-
Notifications
You must be signed in to change notification settings - Fork 1
symbolic_execution
Symbolic Execution is a program analysis technique that translates a program into a model of a program. In contrast to real programs that can only operate "concrete" data (ie, all variables must have actual values like 1 or "foo") the symbolic models produced by Manticore can operate on "symbolic" data. Think of symbolic variables the same way you would variables from algebra.
Consider the following simple function:
function f(uint a) public returns(uint){
return a*3;
}
When this program is being executed, the Ethereum virtual machine only understands the current opcode and the contents of memory. If you execute this function with the value of 4 you will get 12 back but no other information is recoverable about the relationships between inputs and outputs.
When the symbolic execution engine is "executing" this program it doesn't actually calculate the result of any operation. Instead it is building expressions that capture the relationships between inputs and outputs. In when executing this example Manticore will create a symbolic variable a and a symbolic variable that represents the result of the function (a*3). If the result of the function is used later on it will retain information about its origin unlike in EVM.
The way Manticore generates models for EVM is by translating the program instruction by instruction into a representation called smtlibv2. The execution of conditional branches can be very challenging to represent with symbolic execution. The way Manticore gets around this limitation is by forking whenever it encounters a conditional branch and continuing the translation on both forks of the program. This strategy has downsides, it can lead to scenarios where manticore takes a prohibitively long time to complete analysis. The good news is that most smart contracts are written in such a way that code patterns that trip up Manticore don't often get expressed.
Models are comprised of smtlibv2 code. Manticore translates EVM into smtlibv2 in such a way that captures all of the effects and side effects of the instructions. Manticore can then use a solver to generate facts about a program trace. One fact that manticore can generate is the inputs to a contract that make it take a given path through the program. To learn more about the specifics of how smtlibv2 works take a look at the document on z3.