Add a synthesizer engine (#1074)

src/examples/python/synthetizing_obfuscated_expressions.py → src/examples/python/synthesizing_obfuscated_expressions.py

@@ -1,9 +1,9 @@
 #!/usr/bin/env python3
 ## -*- coding: utf-8 -*-
 ##
-## Example of synthetizing obfuscated expressions.
+## Example of synthesizing obfuscated expressions.
 ##
-## $ time python3 ./synthetizing_obfuscated_expressions.py
+## $ time python3 ./synthesizing_obfuscated_expressions.py
 ## In: (((((SymVar_0 | SymVar_1) + SymVar_1) & 0xff) - ((~(SymVar_0) & 0xff) & SymVar_1)) & 0xff)
 ## Out: ((SymVar_0 + SymVar_1) & 0xff)
 ##
@@ -28,7 +28,7 @@
 ## In: (((0xed * ((((((((0x2d * ((((((((((((((((((0x3a * (((((((((((0x56 * ((((((((((((0xed * ((((0xe5 * Sy ...
 ## Out: (SymVar_0 ^ 0x5c)
 ##
-## python3 ./synthetizing_obfuscated_expressions.py  0.12s user 0.01s system 99% cpu 0.125 total
+## python3 ./synthesizing_obfuscated_expressions.py  0.12s user 0.01s system 99% cpu 0.125 total
 ##
 
 from __future__ import print_function
@@ -39,106 +39,6 @@
 from triton import *
 
 
-# Oracles table, each entry is structured as follow (x value, y value, result).
-# More entries there are, more precise is the result for example checkout
-# this table [0] or generate your own table with [1].
-#
-# [0] http://shell-storm.org/repo/Notepad/synthesis_tables.py
-# [1] http://shell-storm.org/repo/Notepad/gen_synthesis_tables.py
-
-oracles_table = [
-    {
-        'oracles'   : [(0, 0, 0), (0, 1, 1), (1, 0, 1), (1, 1, 2)],
-        'synthesis' : 'x + y'
-    },
-    {
-        'oracles'   : [(0, 0, 0), (0, 1, -1), (1, 0, 1), (1, 1, 0)],
-        'synthesis' : 'x - y'
-    },
-    {
-        'oracles'   : [(0, 0, 0), (0, 1, 1), (1, 0, 1), (1, 1, 0)],
-        'synthesis' : 'x ^ y'
-    },
-    {
-        'oracles'   : [(0, 0, 0), (0, 1, 1), (1, 0, 1), (1, 1, 1)],
-        'synthesis' : 'x | y'
-    },
-    {
-        'oracles'   : [(0, 0, 0), (0, 1, 0), (1, 0, 0), (1, 1, 1)],
-        'synthesis' : 'x & y'
-    },
-]
-
-
-sizes_table = {
-    8:  ctypes.c_uint8,
-    16: ctypes.c_uint16,
-    32: ctypes.c_uint32,
-    64: ctypes.c_uint64,
-}
-
-
-# Two vars synthetizing
-def two_vars_synthetizing(ctx, expr, x, y):
-    for entry in oracles_table:
-        valid = True
-
-        for oracle in entry['oracles']:
-            ctx.setConcreteVariableValue(x.getSymbolicVariable(), sizes_table[x.getBitvectorSize()](oracle[0]).value)
-            ctx.setConcreteVariableValue(y.getSymbolicVariable(), sizes_table[y.getBitvectorSize()](oracle[1]).value)
-            if expr.evaluate() != sizes_table[y.getBitvectorSize()](oracle[2]).value:
-                valid = False
-                break
-
-        if valid is True:
-            return eval(entry['synthesis'])
-
-    return expr
-
-
-# Constant synthetizing
-def constant_synthetizing(ctx, expr, x):
-    ast = ctx.getAstContext()
-    c   = ast.variable(ctx.newSymbolicVariable(x.getBitvectorSize()))
-
-    synth = [
-        (x & c, 'x & c'),
-        (x * c, 'x * c'),
-        (x ^ c, 'x ^ c'),
-        (x + c, 'x + c'),
-        (x - c, 'x - c'),
-        (c - x, 'c - x'),
-    ]
-
-    for op, s in synth:
-        m = ctx.getModel(ast.forall([x], expr == op))
-        if m:
-            c = m[c.getSymbolicVariable().getId()].getValue()
-            return eval(s)
-
-    return expr
-
-
-def synthetize(ctx, expr):
-    ast       = ctx.getAstContext()
-    variables = ast.search(expr, AST_NODE.VARIABLE)
-
-    # There is no variable in the expression
-    if len(variables) == 0:
-        return expr
-
-    elif len(variables) == 1:
-        x = variables[0]
-        return constant_synthetizing(ctx, expr, x)
-
-    elif len(variables) == 2:
-        x = variables[0]
-        y = variables[1]
-        return two_vars_synthetizing(ctx, expr, x, y)
-
-    return expr
-
-
 # The following function returns an MBA-obfuscated expression found by
 # Mougey et al. while analyzing an obfuscated program. I took this
 # representation from the Ninon Eyrolle's thesis. The MBA performs
@@ -190,7 +90,7 @@ def main():
 
     for expr in obf_exprs:
         (print('In: %s' %(expr)) if len(str(expr)) < 100 else print('In: %s ...' %(str(expr)[0:100])))
-        expr = synthetize(ctx, expr)
+        expr = ctx.synthesize(expr, constant=True)
         print('Out: %s' %(expr))
         print()
 

src/libtriton/CMakeLists.txt

@@ -50,6 +50,9 @@ set(LIBTRITON_SOURCE_FILES
     engines/symbolic/symbolicExpression.cpp
     engines/symbolic/symbolicSimplification.cpp
     engines/symbolic/symbolicVariable.cpp
+    engines/synthesis/oracleTable.cpp
+    engines/synthesis/synthesisResult.cpp
+    engines/synthesis/synthesizer.cpp
     engines/taint/taintEngine.cpp
     modes/modes.cpp
     utils/coreUtils.cpp
@@ -94,6 +97,7 @@ set(LIBTRITON_HEADER_FILES
     includes/triton/modes.hpp
     includes/triton/modesEnums.hpp
     includes/triton/operandWrapper.hpp
+    includes/triton/oracleEntry.hpp
     includes/triton/pathConstraint.hpp
     includes/triton/pathManager.hpp
     includes/triton/register.hpp
@@ -108,6 +112,8 @@ set(LIBTRITON_HEADER_FILES
     includes/triton/symbolicExpression.hpp
     includes/triton/symbolicSimplification.hpp
     includes/triton/symbolicVariable.hpp
+    includes/triton/synthesisResult.hpp
+    includes/triton/synthesizer.hpp
     includes/triton/taintEngine.hpp
     includes/triton/tritonToBitwuzlaAst.hpp
     includes/triton/tritonToZ3Ast.hpp

src/libtriton/api/api.cpp

@@ -1316,4 +1316,14 @@ namespace triton {
     return this->taint->taintAssignment(regDst, regSrc);
   }
 
+
+
+  /* Synthesizer engine API ============================================================================= */
+
+  triton::engines::synthesis::SynthesisResult API::synthesize(const triton::ast::SharedAbstractNode& node, bool constant) {
+    this->checkSymbolic();
+    triton::engines::synthesis::Synthesizer synth(this->symbolic);
+    return synth.synthesize(node, constant);
+  }
+
 }; /* triton namespace */