hevm or: How I Learned to Stop Worrying and Love the Symbolic Execution

Hi everyone, I'm Mathis Sos and I'll be talking about HEVM and symbolic execution that we built together with Lexi, myself and Zoe. We're part of the Argo Collective. That is a recently spun out collective from the Ethereum Foundation. If you want a bit more about the Argo Collective, you can watch our talk that was given yesterday. So first of all, what is this talk going to look like?

So first, I'm going to talk a little bit about what it means to symbolically execute. Then I'm going to give a bit of an overview of HEVM. Then I'll explain how HEVM can be used to secure down some of your work that you have done, hopefully. And then finally, I'm going to conclude this talk. So first of all, what is symbolic execution?

So let's say that your code looks like this. If you try to do fuzzing on this code, it will likely not find the fault that is marked by assert false, which could be, for example, something that drains your contract or locks your funds or some kind of negative event. So you can keep fuzzing this forever, essentially, and nothing will happen. But if you run symbolic execution on this, it will immediately hit the assert false and will give you the solution, the two integers that you need to pass in to trigger the failure. integers that you need to pass in to trigger the failure.

So this is a good sort of litmus test of what symbolic execution can do in comparison to fuzzing. Of course, it can do more, but this is a good example where fuzzing will not help you very much, and symbolic execution will definitely help you. So let's get a little bit more into the details. So here we have, I used traditional assembly. I'm old school.

I could have used EVM assembly, but it's more or less the same. So what we're going to do here is I'm going to showcase a very simple straight line program where we do a move and an add with two registers. So here we have concrete execution on the top. And what you have is concrete values like 1 and 2. And then the MOV will move the value 2 to the A register.

And then it will add 4 to this value. And then the final register state will be 6 and 2. Now, when it comes to symbolic execution what it will do is it will instead of initializing it with concrete values like 1 and 2 it will initialize it with a variable like v1 and v2 and then we'll try to execute these instructions but over these variables rather than the concrete values and what that will do is that as you can see step by step we we have the state evolve and eventually it will end up with V2 plus 4 on the A register and V2 on the B register. So, of course, if I substitute the concrete values into that, we'll end up exactly where we were with concrete execution. But what this means is that I can mathematically express what is the state for any input value, right?

And, okay, so that sounds interesting. Where does this get hard? Because this seems relatively straightforward. So it gets kind of hard is when branching happens. So here is a program where we have a branch.

And with concrete execution execution it's relatively straightforward we have both registers set as one then we're gonna check whether they are equal they are happen to be equal and if they are true then we're gonna add five to the to the register a and so the the final state is six and one right so this is quite clear but when it comes to symbolic execution we we don't know of of course, what the value of A and B is. We represent them as these symbolic variables, V1 and V2, and we need to check for both potential execution paths. In this case, when V1 is equal to V2 and when V1 is not equal to V2. And we'll end up with two different states, potentially. In this case, we do actually end up in two different symbolic states.

In one case, V1 is incremented by 5, and in the other case, V1 is incremented by 4. Of course, again, if I substitute the concrete values in, then I'll get exactly the concrete execution. However, what this means is that now we branch. So now we have two states, and if there's another branch, then this can become, of course, exponentially large number of exponential large number of potential end states. If there's a loop, of course, that can be, if it's infinite loop, it's not a bounded loop, then you can have issues with this thing never terminating because we don't actually know you know if ever the loop condition is is reached and so we can potentially run forever so I'm just gonna talk a little bit about what other similar execution systems are out there before I jump into HCVM.

First of all, there's more or less two types within this ecosystem as far as I understand. One of them is you have a static code analysis engine, and now you want to validate whether some of the things that it spits out are potentially false positives. And in this case, if the symbolic execution engine is not complete or doesn't understand everything, it's kind of fine because what you will do is you will just simply spit out the potential false positive and let the user deal with it. And that's fine. But in our case, we actually don't use the static code analysis engine as a precursor to HEVM, so we actually have to deal with everything that the EVM has to offer.

And so it's a bit more complicated, and it's also more complete, of course. So these purely symbolic execution framework-based systems, there are a number. There's Sertor Approver, which is based on this backwards exploration and weakest precondition computation. There's ETHBMC, which is, of course, as the name suggests, a bounded model checker type system. Then there's Halmosh.

It's written in Python. And then there's KEVM, which is based on the K framework and allows you to break out into K in case you need to prove some things. For example, loop termination or invariance and things like that. So just a bit of an overview of HEVM. So it started a long time ago as part of the DAPTools project.

It implements the EVM semantics both concretely and symbolically, and actually Echidna fuzzer, if you know about it, it uses HEVM underneath for the concrete execution semantics. It is possible to execute any call from any potential state in the EVM. So it understands all of the EVM in terms of, like, for example, calling out to an RPC, to an archive node, to fetch state, et cetera. It runs, it basically computes a query to an SMT solver, runs the SMT solver to get the response to the query, and then interprets this response and displays it back to the user in a fashion that is more user-friendly than some SMT output. We'll see that in a moment.

So there are two ways of using HEVM. One of them is for counter-example example generation and one of them is equivalence checking. So let's talk a little bit about this counter example generation for in this case and some kind of post condition that typically is written for example in FORGE test case as a FORGE test case. So here we have Solidity, Viper, whatever language you prefer, or even just pure EVM bytecode, and that gets interpreted by the internal symbolic execution engine inside, symbolic interpreter inside HEVM to produce an intermediate representation. And then this intermediate representation, together with the post post condition that you put down gets compiled into a logical formula that gets sent out to the SMT solver and SMT solver is what's called a site model theory solver so it understands for example bit vector arithmetic which is quite useful because of course there's these 256 bit bit vectors or variables in EVM that EVM operates on.

And then either it proves the property, finds a counterexample, or times out, of course. That's always a potential possibility. When it comes to symbolic execution for equivalence checking, we do something very similar. But what we do eventually is that we try to compare the two executions against each other. So you have bytecode A and bytecode B.

Let's say that bytecode B is like a refactored bytecode or something that is gas optimized, and you want to make sure that it's doing the same thing as the original one. And now what this will do is that it will try to act to prove that it is equivalent, find the counter example, so some input or in state where the two contracts actually disagree, or of course, there's always the potential for timeout. And let's go a little bit deeper into this kind of symbolic execution engine inside HEVM. So it operates on bytecode, which means that we're not tied to any particular compiler we're not even tied to something like you will for example understands all of the EVM stack call frame stack storage call data everything can as I mentioned it can actually run at any point in the blockchain history and it is fast against the concrete execution semantics of GATH in this case. As mentioned, like it has issues with loops and recursions because of this issue that unterminated loops, we don't know when to stop.

It has some issues related to symbolic off-size and memory copy. This is purely due to SMT limitations and doesn't currently deal with symbolic gas, so it basically ignores gas when it comes to symbolic execution. In concrete execution, of course, it understands gas and will deal with it, and so Echidna will be running correctly in that sense. So just a bit of the internals. Maybe this is a little too small, but basically what it does is that it takes in as an input the EVM bytecode.

Then it will step-by-step execute it and branch, if necessary, to build an intermediate representation. And then this intermediate representation is simplified in a generic way. And there are some specific simplifications related to catch-hawk and arrays and maps and things like that that are quite specific when it comes to to how the EVM handles arrays and maps and things like that so especially catch-hook which is very complicated to put into exactly represent in in SMT eventually what happens is that this IR gets compiled into a bunch of SMT queries, and these SMT queries get dispatched to the SMT solver or solvers, and then we gather all the results from the SMT solvers and then get the counterexamples, extract them, and map them back to the query that was originally dispatched and see how we can display that to the user in a way that they will be able to run this and actually trigger the fault. Because at the end of the day, it's annoying to get something like, hey, your problem is faulty. That's not going to help the user.

But the user really wants some kind of counter example so they can actually run it and see how it is wrong. And then, of course, they can fix it or hopefully fix it. So that's kind of the high level of the internals. So let's talk a little bit about this intermediate representation. I'm not going to go into the details, but that's kind of at the middle of this whole box, in the previous box that I showed.

So here's a simple function, right? that I showed. So here's a simple function, right? This will overflow if the variable that you put in is large enough, in particular exactly equal to 2 to the power of 256 minus 1, and b will actually not be larger than a in this particular case. I'm sure you have played around with this.

It's a very trivial overflow issue. And this gets compiled into this intermediate representation where we have a proposition that a must be smaller than the a plus 1. So I mean, it's very simplistic in this space. But the point was to make it kind of readable and also human readable. This can also be compiled into a graph, as you might imagine, and it can be quite understandable to a human how the internal representation maps back to the original code.

In this case, it's quite clear. Okay, so I'm going to talk a little bit about uh about how to actually run this tool and what kind of results you can expect so in this particular case we have a forge standard test that we're gonna import our contract is um is a test and then we add prove underscore in front of it you will need forge you will need Z3, which is one of the SMT solvers that we support, and you need HEVM binary that you can just download from the repository. And you put down this test, and this test will, of course, fail, again, due to overflow. And the way you run it is very, very simple. You just build with the ESC and run HVM test.

And it will parse everything up and do its magic and eventually give you a counterexample, which is what you expect. So this is sort of the base way of using it. And it is as clean and tidy as it looks on the output. I did not actually change that or edit it or even the spacing is how it is. So it's quite visually representative of what are you going to test and what are the counterexamples that come out.

If there's more than one counterexample, there's going to be more than one listed there. So how does HEVM equivalence work? Here I'm just going to show sort of a contracted thing. It's a very complicated code that was someone tried to use. And here I just want to show some of the edge cases, but also that we do power through the edge cases as well.

So in this case, there's two codes, and we want to know if they're equivalent. You see that it emits a warning that we cannot actually explore the whole thing in this particular case due to a call into unknown code. Obviously, we don't know what's going to happen there, like what is going to get executed. But beyond that, it says, OK, well, anyway, I power through. I'm going to ignore these bits and pieces.

We have 1.7 million end states that we need to check for equivalence. And then it says, OK, well, I tried my very best. There's 93 of them I couldn't do because of this memory that was a memory copy that is symbolic. I couldn't do two because of timeout.

This actually had a 15 second timeout for each query. And eventually I couldn't find any discrepancies given these warnings and things that I couldn't actually explore. And if you have a look, this actually ran for like 34 minutes and 45,000 seconds, so obviously it was like