2

See question. Is the SMT Checker in solidity a form of symbolic execution?

1 Answer 1

2

Yes. It is.

Symbolic Execution Primer

Symbolic Execution is a means of analyzing a program to determine what inputs cause each part of a program to execute. It will convert the program to a symbolic expression (hence its name) to figure this out.

Aka, it will attempt to convert your program to a set of logical expressions. Aka aka: Make your code math.

This is also known as "path exploration" because getting this set of logical expressions will give you a formula that relates to conditionals, or "find it's path".

Example

For example, take this function:

function f(uint256 y) public {
  uint256 z = y * 2;
  if (z == 12) {
    revert();
  } 
}

If we wanted to prove there is an input for function f such that it would never revert, we'd convert this to a mathematical expression, like such:

z == 12 && // if z == 12, the program reverts
y >= 0 && y < type(uint256).max && // y is a uint256, so it must be within the uint256 range
z >= 0 && z < type(uint256).max && // z is also a uint256
z == y * 2; // our math

In this example, we have a set of 4 boolean expressions.

SAT Solver

We can then take this set of logical expressions and dump them into a SAT Solver (A SAT Solver is not symbolic execution, but right now is a popular next step). Which for now, you can think of as a black box that takes boolean expressions and tries to find an example that "satisfies" the set. For our example above, we are looking for a input y that enables the rest of the booleans to be true.

To dump this into a SAT solver, we need to convert our math to CNF form which might look something like this:

(z <= 12 OR y < 0 OR z < 0) AND (z >= 12 OR y < 0 OR z < 0) AND (z <= 12 OR y < 0 OR z > 2y) AND (z >= 12 OR y < 0 OR z > 2y) AND (z <= 12 OR y >= 0 OR z < 0) AND (z >= 12 OR y >= 0 OR z < 0) AND (z <= 12 OR y >= 0 OR z > 2y) AND (z >= 12 OR y >= 0 OR z > 2y)

Our SAT solver will then attempt to find a contradiction in our set of booleans, by randomly setting booleans to true / false, and seeing if the rest of the equation holds.

It's different from a fuzzer, as a fuzzer tries inputs for y. Whereas a SAT Solver will try different inputs for the booleans.

Solidity SMT Checker

The solidity SMT Checker attempts to do this conversion of code -> math itself based on your assert and require statements and then runs it through a SAT solver, and therefore is a form of symbolic execution.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.