libTriton  version 0.4 build 1355
Dynamic Symbolic Execution

Table of Contents

[internal] All information about the dynamic symbolic execution engine.

Description


Triton contains an internal Dynamic Symbolic Execution (DSE) engine. This engine maintains a symbolic states of registers and part of memory at each program point.

The symbolic engine maintains:

During the execution, according to the instruction semantics, the table of symbolic registers states is updated at each instruction executed. This table is modeled by a correspondence of \( \langle rid \rightarrow \varphi_x \rangle \) for each register where \( rid \in N \) represents the unique register's reference and \( \varphi_{x \in N} \) represents the unique symbolic expression's reference and the link to its SMT graph. In other words, at each program point, all registers points on its symbolic expression which represents the last semantics of the assignment.

Step Register Instruction Set of symbolic expressions
init eax = UNSET None \( \bot \)
1 eax = \( \varphi_1 \) mov eax, 0 \( \{\varphi_1 = 0\} \)
2 eax = \( \varphi_2 \) inc eax \( \{\varphi_1 = 0, \varphi_2 = \varphi_1 + 1\} \)
3 eax = \( \varphi_3 \) add eax, 5 \( \{\varphi_1 = 0, \varphi_2 = \varphi_1 + 1, \varphi_3 = \varphi_2 + 5\} \)

Like with registers, Triton maintains a symbolic states of part of memory. This is modeled by a correspondence of \( \langle addr \rightarrow \varphi_x \rangle \) for each address where \( addr \in N \) represents the address of the memory and \( \varphi_{x \in N} \) represents the unique symbolic expression's reference.

Step Register Memory Instruction Set of Symbolic Expressions
1 eax = \( \varphi_1 \) n/a mov eax, 0 \( \{\varphi_1 = 0\} \)
2 n/a sp = \( \varphi_2 \) push eax \( \{\varphi_1 = 0, \varphi_2 = \varphi_1\} \)
... ... ... ... ...
10 ebx = \( \varphi_3 \) n/a pop ebx \( \{\varphi_1 = 0, \varphi_2 = \varphi_1, \varphi_3 = \varphi_2\} \)

Based on this process, we know that \( ebx = eax = 0 \).

There also exists an important point, if there is no previous symbolic reference of a register or part of memory when the instruction is processed, Triton builds the expression with the concretization of the value and assigns the expression to a new symbolic reference. This allows us to start the analysis everywhere.