Symbolic Rust EVM

[gakonst]

Motivation

Fuzzing is great but it does not cover all potential code paths, it just sprays and prays randomly right now

Solution

Create a Rust Symbolic EVM which we ideally implement the Evm trait for so that it can be used seamlessly in forge.

Other Context

Symbolic evms impls:

• https://github.com/palkeo/pakala/blob/fce61037e511321cfd97b8adf88f5d3b74781099/pakala/sm.py
• https://github.com/dapphub/dapptools/blob/beaaeb6a6ad1cde22989bd088b10bdd06718b73f/src/hevm/src/EVM/Symbolic.hs
• https://github.com/ConsenSys/mythril/tree/2518cc8b656bb0d21a80058c3f7f1def13da8db7/mythril/laser/ethereum
• https://github.com/trailofbits/manticore/blob/b4d129f8b1fd07501ffe096a835366b110470b4d/examples/evm/minimal.py

Blogs

• https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
• https://forum.openzeppelin.com/t/symbolic-execution/2158

[transmissions11]

can get the best of both worlds with symbolic seed fuzzing:

[drawnwren]

Does anyone have good resources for building a performant symbolic execution engine? I am thinking of giving it a shot, but would like a better grasp of best practices + theory.

edit: The manticore paper is good and here's a good explanation of symbolic state merging.

[Silur]

let's suppose the SEVM is done, what solver shall we use to exhaust the symbolic states?

[grandizzy]

let's suppose the SEVM is done, what solver shall we use to exhaust the symbolic states?

I think for the starters should be z3 (https://github.com/prove-rs/z3.rs) . Other candidate could be Yices2 (https://github.com/novafacing/yices2-rs)