3

I'd like to see a minimal symbolic execution / formal verification example using the following function:

function f(uint256 a) public returns(uint256){
  a = a + 1;
  return a;
}

What would that look like?

1 Answer 1

2

When we look at this function, we can easily see two paths this function can take.

  1. a < 2^256, a = a + 1, function returns
  2. a == 2^256, a = a + 1 overflows, function reverts

We can turn these into a set of boolean expressions. Then, input those into a SAT Solver with some "question" added to it. We can see what this code would look like in SMT-LIB format to input to something like the z3 SMT Solvet.

; Declare a symbolic integer variable 'a' as a 256-bit integer
(declare-const a (_ BitVec 256))

; Create a context for Path 1
(push)

; Add assertions for Path 1
; assert a is not equal to `uint256.max`
(assert (distinct a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
(check-sat)

; Remove the context for Path 1
(pop)

; Create a context for Path 2
(push)

; Add assertions for Path 2
; assert a is equal to `uint256.max`
(assert (= a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
; bvult is "bit vector unsigned less than", so we are checking that a + 1 is less than a
(assert (bvult (bvadd a (_ bv1 256)) a))

; Check if Path 2 is satisfiable
(check-sat)

The (check-sat) line is sort of the "question" we are asking. We are saying "is there a variable a such that all the booleans in this list are true?"

If the property of our smart contract was "f should never revert" we could see Path 2 holds that "question".

This line:

(assert (bvult (bvadd a (_ bv1 256)) a))

Is a boolean saying essentially (a + 1 > a). Since we have included it, you could argue the question we are asking our theorem solver is "with these constraints, could function f ever revert?"

The output of this in z3 would be the following:

sat

Meaning, that yes, the function f could revert.

The hard part of all this, is converting your solidity -> SMT-LIB for a solver solver to digest. Tools like manticore can do this, but will give you the SMT-LIB for the entire contract. ChatGPT can also help create these conversions. It can be really tricky to get this conversion correct though.

Your Answer

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

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