Symbolic execution for HEVM; hevm symbolic and hevm equivalence

[MrChico]

This draft PR is a WIP extends hevm with symbolic execution capabilities, allowing it to be used as a proving engine for formal verification, as well as admitting more intelligent fuzzing strategies.

It's not particularly close to being ready for merging yet, but I would like to share my progress to get some early feedback and discuss some of my findings so far.
It is now ready for review!

On a high level, here's what's going on:

Most of the magic here comes from the SMT-based verification library sbv, which provides symbolic variants of common basetypes like booleans, words and integers. These variants are strict generalizations of their concrete counterparts and functions over them will just evaluate normally when given concrete arguments. Using these we can generalize various parts of the EVM:

• The EVM stack is changed from a list of words, [Word 256], to a list of symbolic words, [SWord 256], and stack operations are adapted accordingly.
• The buffers memory, returndata and calldata are changed from ByteString to [SWord 8]. This is a (concrete) list of symbolic values, not a symbolic list, which means that while reads and writes can refer to symbolic values, they must always happen at concrete locations. This restriction means that we are unable to deal with dynamic data types for the moment. More on this later.

The main part of symbolic execution is handled by the function symExec, which executes the EVM with symbolic values while keeping track of an accumulated list of constraints (path conditions), until reaching a JUMPI opcode. At this point, it invokes z3 to check which branches are possible, and recurses with the path condition updated accordingly until reaching a list of possible final VM states. The resulting VM states can be checked against a post condition.

EDIT (04/07/2020):

Symbolic execution is now done with the "operational monad pattern" as seen in TTY, VMTests Dev, etc. Similarly to how instances of SLOAD or CALL causes the execution to end with a Query error, JUMPI introduces a new type of query (PleaseAskSMT), which will need to be performed in an IO context. The actual smt query is performed in a new fetcher, which is used in TTY.interpret (which (as before) only keeps track of one VM at a time) and the new SymExec.interpret, which is essentially a function VM -> [VM], but crucially does the necessary lifting in case we encounter any blocking queries.

Some example proofs are given in test.hs.

While defining arbitrary post conditions is probably better handled with something like act, this PR provides an easy way to check for asserts (executions ending with an INVALID opcode (0xfe)) using the cli endpoint hevm symbolic.

Example usage:

echo "pragma solidity >=0.5.15; 
           contract A {
               function factor(uint x, uint y) public pure {
                   require(1 < x && x < 973013 && 1 < y && y < 973013);
                   assert(x*y != 973013);}
}" \
| solc --combined-json=bin-runtime - \
| jq '."contracts"."<stdin>:A"."bin-runtime"' \
| tr -d '"' > fun.txt

hevm symbolic --code $(<fun.txt) --abi $(seth --abi-function-json "factor(uint256,uint256)")
"Assertion violation:"
(1021, 953)

Obvious TODOs

• Allow storage to be symbolic as well.

• Ensure that the conversion did not mess up any of the general state tests. The semantics for concrete execution should remain unchanged after this.

More interesting TODOs:

• EVM words are a little too large for z3 to be good at dealing with them. As a result, it hangs on some simple proofs like this tautological SafeAdd proof. This has also been noted as a problem for @leonardoalt, which recommended to use unbounded integers instead. This would require adapting all arithmetic opcodes to operate modulo 2^256 instead. But there also might be other solvers than z3 that are better at dealing with large bitvectors.

EDIT 08 June:
There is now support for cvc4 as well, which in certain situations deals a lot better with large bitvectors. Large bitvectors seems preferable to modulo integer arithmetic, especially since most contracts use quite a lot of bitvector operations to do masking and other encoding gymnastics.

• It should be possible to generalize byte buffers like memory and calldata to deal with symbolic locations. SBV offers two options here, SArray which translates directly to an smt array, and SFunArray, which is "implemented internally, without translating to SMT-Lib functions". I'm guessing the latter option is preferable.

EDIT 08 June:
I have generalized calldata slightly with a slight of hand: calldata is now a tuple (SWord 32, [SWord 8]), where the first argument is understood as the calldata length. Since EVM just returns zeros when reading out of bounds calldata, this allows us to fully abstract calldata without having to deal with arrays.

• The Show instance for symbolic values, is quite boring as it just displays <symbolic> for symbolic variables. For a more insightful hevm --debug experience, we might want to accompany symbolic words with a pretty-print string, at least when function ABIs are available. Opcodes would need be adapted to update the pretty-print string as well as updating the values.

EDIT 13 July:
Basic scaffolding for displaying symbolic values with a richer AST is given, but the full implementation is decided to be out of scope of this first PR.

• Quite understandably, the current execution strategy fails miserably when dealing with loops whose condition depends on a symbolic value. Depending on the setting, one could go in several directions to account for this:

1. Keep track of which pc values have been visited, and restrict the number of times we are allowed to return to a particular pc value, aka "bounded model checking".
2. Maintain a set of "trusted specs", i.e. VM -> VM functions that can only be applied under certain conditions. These "trusted specs" can themselves be proven by symbolic execution and coinduction.
3. Try to infer loop invariants automagically using some CHC style solution or whatever Data.SBV.Tools.Induction uses. I'm doubtful this would work, but it's worth exploring.

EDIT 08 June:

1. is now implemented, and the number of times revisiting the same branching point is allowed can be configured using the flag --max-iterations.
   2 can be done once better act integration is here, and 3 remains interesting to explore in the future.

This type of symbolic execution would probably be able to generate a lot more interesting test cases for tools like Echidna. Do you guys (@japesinator, @incertia) have any specific requests for functions that would allow you to incorporate this into your workflow?

What are the effects on performance for concrete execution? Hopefully it does not change drastically, but I think a slight performance decrease would still be acceptable.

EDIT: July 13
Performance is actually better on this PR than on master, see the measurements done by @xwvvvvwx further down this thread.

[leonardoalt]

It should be possible to generalize byte buffers like memory and calldata to deal with symbolic locations. SBV offers two options here, SArray which translates directly to an smt array, and SFunArray, which is "implemented internally, without translating to SMT-Lib functions". I'm guessing the latter option is preferable.

@MrChico What's SFunArray? If it's not too hard to implement, maybe give SMT arrays a try as well at some point. It is one of the most studied/implemented SMT theories, so I wouldn't be surprised if it's performance is good.

Try to infer loop invariants automagically using some CHC style solution

I'd be interested in trying something like that

[MrChico]

@leonardoalt What's SFunArray?

From what I understand, when using SFunArray, sbv handles the "internals" of the array structure manually – it maintains symbolic variables for all used keys and values, and translates reads and writes to big nested ite expressions over these. It also does caching, apparently.
As a result, one cannot compare two SFunArrays.

It seems appropriate for memory and storage, where we care mainly about the values at specific keys, rather than the structure as a whole.
For buffers like returndata and calldata where we want to make claims about the entire structure, maybe SMT arrays are more appropriate

[MrChico]

Also implements #305 as of 3575269, allowing previewing of transactions or debugging of past transactions.

[MrChico]

Incidentally also solves #273

[livnev]

Also implements #305 as of 3575269, allowing previewing of transactions or debugging of past transactions.

Wow amazing!

[MrChico]

I now consider this effort feature complete for a first release. I'll be adding some more tests and docs (check out the readme and please let me know whats unclear!) as well as writing a blog post over the next couple of days, but that shouldnt be blocking review.

I'd be happy for experiments all over, but in particular the equivalence checking and the symbolic execution against remote state (using rpc) would benefit from some extra hands trying things out

Concrete execution and all old cli endpoints should remain their current functionality (modulo some minor improvements), so please lmk if you find any regressions here. That said, many library functions have changed type signature though so this is a very breaking release

Finally, I suggest we should not squash these commits when merging as that would make the git history fairly opaque.