Advanced Fuzzing Pipelines

[d-xo]

Just noting some ideas that @msooseth and I discussed for nice fuzzing pipelines that we could write if had an Expr -> EVM compiler.

Compiling an Expr End into EVM bytecode should be fairly simple, especially if we produce yul instead of bytecode directly. Each ITE can be an if-then-else block, and translating return / revert leaves into return / revert statements in yul shouldn't be too hard.

Concrete Evaulation vs Geth

1. Generate a random Expr End
2. Compile that into evm
3. Execute both against some concrete input value and compare the result

This would test our smt encoding to make sure that it matches the concrete semantics (we could use the concrete semantics from hevm or from geth).

Symbolic Exec vs Equivalence Checker

1. Generate random bytecode
2. Symbolically exec to produce an Expr
3. Compile the Expr into EVM
4. Run the equivalence checker against both

This would test the symbolic execution engine (and Expr -> EVM compiler) against the equivalence checker.

[d-xo]

Actually for the first case we don't even need an Expr -> EVM compiler, we can just generate random bytecode, produce an Expr from it, and then compare both against some concrete value.

[msooseth]

Notes to self:

Fuzz input generators: https://github.com/MariusVanDerWijden/tx-fuzz https://github.com/MariusVanDerWijden/FuzzyVM

Runners: https://github.com/holiman/goevmlab

Branch: fuzz-msoos2

Check accuracy through geth:

• Run geth in --dev mode and use geth attach JSON RPC: https://ethereum.org/en/developers/docs/apis/json-rpc/
• eth namespace in JSON-RPC: https://geth.ethereum.org/docs/interacting-with-geth/rpc/ns-eth
• eth.call method of geth in JSON-RPC mode (https://www.quicknode.com/docs/ethereum/eth_call) can set state (including injecting a contract), execute code, and get the return value. It does NOT persist state, which is good. Then we can check it against what HEVM did.
• notes about it here: https://hackmd.io/Fkh-_l6-T-q1znP44twuMQ

Catch errors with:

• https://hackage.haskell.org/package/ChasingBottoms

Fuzzing tools:

• We can do coverage-guided fuzzing of hevm-ci itself via LLVM compile (GHC supports this)

Tracing:

• tracing visualization goevmlab: https://github.com/holiman/goevmlab
• tracing explained: https://www.youtube.com/watch?v=b8RdmGsilfU
• We can use the trace-based comparison of fuzzyvm, by re-adding https://github.com/dapphub/dapptools/blob/master/src/hevm/src/EVM/Dev.hs#L151 back to HEVM (Tracing tool: https://github.com/ApeWorX/evm-trace)
• We can also pass a tracer CODE that will act on the trace(!)

[msooseth]

This has been implemented in Tracing.hs, closing.