Ethereum Foundation DevCon 6 - Developer Infrastructure Track, 16 Oct 2022

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Building an End-to-End EVM Symbolic Execution Engine in Solidity by Leo Alt | Devcon Bogotá

Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/building-an-end-to-end-evm-symbolic-execution-engine-in-solidity/

Symbolic execution is a widely used approach to formally verify/analyze EVM bytecode. But what exactly is it? What are constraints, and solvers?? Why do you need symbols anyway?? In this talk we will go through a symbolic execution engine for EVM bytecode fully written in Solidity, hopefully demonstrating how beautiful and simple these techniques are, and incentivizing developers to contribute to or write their own formal methods tools.

Speaker(s): Leo Alt
Skill level: Advanced
Track: Developer Infrastructure
Keywords: Solidity,Symbolic Execution,Formal Verification

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

A

A

Yes, so this came out of like a fun project. I wanted to write like a full like an end-to-end, um symbolic execution engine in solidity with including the the solver that we usually use in the in the background, and this is actually pretty fun. So I want to share with you what this does um so a few questions for like audience.

A

Adjustment who, yes, who here was at Harry's, talk yesterday about symbolic computation in your okay, who knows what symbolic execution is: okay, nice I am prepared to tell you what it is, though, for the ones who don't know so I'm quickly going to go over some slides and then we're going to move to code. This word or these expressions are thrown around a lot like what symbolic execution, what's constraints, what's: sn2 silver?

A

What's all that stuff and a lot of people know what it is, but if you don't know what it is they kind of like you feel left out, and these words are used very um trivially, even though they're not really they're simple, but not trivial. So first I want to tell you what's not symbolic execution and that's concrete execution. So let's say you have oh yeah last question: who can read assembly like this nice? Okay, that's very good!

A

um So let's say we have this assembly here from evm and we want to run the concrete execution over it. So let's say we have this call data, um it's 12 in hacks, I, don't know what that is, and what is that in decimal, like 20, no 18. yeah, it makes sense. So if you run this program without call data, what do we get? um What's like? There's no return here is: let's just consider the top of the stack as sort of a return.

A

In this case we get a 12 we're going to push zero um and the stock could call data load that position we get to 12 push three multiply. That's going to give us 36 in HEX, we add one. So we get this number top of the stack right. So this concrete execution, you have a program, you have a concrete input and then you execute the program that input you get an output. So now what is symbolic execution?

A

We just said: what's not so t11 actually has a pretty good explanation of what it is, so it turns the program into math and then solves math formulas. That's actually a very precise, although very vague description of what it does. We have the same program here, but now, instead of a concrete, called Data we're going to have a symbolic called Data. What does that mean to be symbolic? Is that you just use a variable instead of concrete number? That's really all you do you look.

A

You keep looking at variables, so our entire call data is going to be CD. Now it's just a variable. The top of our stack is going to be a variable called top. That's all we're doing so here we're going to collect constraints which are things that must be true when we run the program. So when we run call data load of zero, we're basically doing CD of zero right and then we can also call it X.

A

We can call it side, we can call it whatever it's just a symbol um and it happens that that thing must be greater equals zero, because we're trading we're dealing dealing with evm words and they're unsigned right. The second part is that we are assigning that to X. We just make a variable out of out of that when we do the call data load next thing, we have this multiplication. We can make another variable for it called Y, which is now x times three.

A

Finally, for this ad, we can make another variable for it called top and then which we just did the previous top of the stack which is y plus one.

A

um So you see that for every operation we add a new variable, we add a new symbol that represents that expression and we collect all these Expressions. So we end up with what we call these constraints, and this is what is our symbolic encoding? So we take the program in evm, bytecode and assembly. Here we transform it into a set of constraints and that's our symbolic encoding, they're different. There are many many different ways to write these constraints from a program, which means we have different ways to symbolically encode your program.

A

Why do we want to do this, so we obviously walking code is going to turn into a system of linear inequalities, so this was our set of constraints. That's going to turn into the system of linear inequalities. There are equalities here, but they can be very quickly translated into inequalities, um so we just keep them as they call it for Simplicity, and why do we do this?

A

The reason why we do this because we know how to solve these things with algorithms that you might have seen in high school or University, or you still will see it when you finish high school and what can we do with it? We can, for example, did the same thing we did before. We can give a concrete call data in this case the same called Data as we we had before and run it symbolically. What does that mean?

A

We're gonna, in this case a simple substitution: does it we can substitute CD by visitorical data, which then substitute CD of 0 by 12 and so on, and we get at the top is going to be this number when we solve that with gal, Jordan, illumination or Gauss elimination or there's tons of ways of solving it. A simple substitution here will: do it not only gives us the value for top. It gives us values for every single variable in this system.

A

We could have read it that it before with the concrete execution, so the cool things we can do with this. We can ask many many things, so you can ask, for example, can top be greater than 10 000.. How do we ask that we simply add a constraint that represents that statement in this language, so can top be greater than 10? 000 basically gives us this constraint here and then, but here's the answer.

A

It is possible, in which case such a solver, such a math solver, will tell us that the system is satisfiable, meaning that there is evaluation for every single variable in the system. That makes this the the the set of constraints satisfiable.

A

It is possible that all the constraints are true at the same time, and it also gives us what we call a model, which is the actual values that make the whole the whole set of constraints valid and similarity before we have a value for top and- and we also have values for every single variable that appears in the in the system.

A

We can also ask n top be zero. What do you think so? We can represent it for this constraints, pretty simple by the way where all these variables are on the integers there's no reals or rationals here, everything's integers. um In this case this oversized the system is unsatisfiable. It's inconsistent, there's, there's no way all these constraints can be true. At the same time, they may be true in separation, but they will never be true um at the same time, what we want to do is basically do exactly that in solidity.

A

So, but what exactly do we want to do? You can do several things you can try to prove that a certain assertion is true. You can prove that a certain thing always happens or never happens, kind of things for our use case, we're going to try to find unreachable branches. So here's a piece of solidity we're going to analyze the VM byte code, but this is just to show an example. So we have this functional, X and integer X and first we require that X has to be last or equal 10..

A

Then we have the branches as if x, slash or equal 50 does something and then the rest does return is false. So this Branch here, basically the false branch of the f.

A

It's unreachable right because ax we know that X is less or equal 10 from the beginning of the function, which means it's always less or equal 50., meaning that it will always enter the if and it will never come to this part of the of the code. So if you take the true Branch, this is reachable because these constraints are together, but these are not right. So if x has to be less or equal 10, it cannot be greater than 50.. So this branch is unreachable. We can remove the whole thing.

A

Well, not the whole thing, just the the bottom. The cool thing about trying to do that stuff is that we need very little support from the evm.

A

Of course, if you want to write, if you want to write a symbolic education engineer to write an interpreter in the first place right, you need an NVM interpreter, but we don't want to deal with every object because it gets really big, really complicated and we don't want to do things like call, create and storage and all these complicated stuff, which of course, you could and a lot of tools do that. We don't want to do that in solidity. The cool thing again about this encoding.

A

We we only have to care about the stack operations um control flow, so it jumps and opcodes that stop the execution and relation upgrades, and so basically we're going to Care, mostly about as I, saw before ifs with relation operators inside so less than greater than and the negation of these, so that you can get less than or equal and greater than or equal.

A

The symbolic encoding we're going to use is also pretty simple so for every evm expression that we saw before we're going to transform it into math constraint of the form, a minus, B, less or equal K, where A and B are going to be variables and K is going to be a constant. So this is also what Harry was talking about yesterday in in his talk, and we got things like like this: for example, whoever was in Harry's talking together. Is this uh system satisfiable yeah?

A

So if you sum everything on both sides, then you get basically zero. Last Oracle minus two, which is a contradiction, so this system is impossible to be satisfiable.

A

um The reason why we like this encoding is because we can use a difference, logic, solver and again, as Harry explained yesterday, a difference logic solver is very simple: to write. What does it do? It basically takes these constraints, these math constraints, and it tells you whether it's possible or not, that these things are satisfiable at the same time, and if it is possible, it's going to give you values for the variables that make it satisfiable.

A

Otherwise, it just says it's not possible at all for these things to be satisfiable together, um the solver is much simpler than the things you need like ILP or smt, when you need to solve with linear combinations or even non-linear expressions and the sorts of things that you end up with when you start encoding, arithmetic expressions and other things and as also higher explained yesterday. This runs in employ normal time on the graph generated from the constraints using the volume four graph algorithm not going to go much into that.

A

If you want to learn more about that, please re-watch um Harris talk and this algorithm is super simple. This is basically almost the whole thing, and most of it is comments. um So now all we need to do is put it all together. So this is the whole project, so these are two tests files, one for the solver itself, just like you need to test for the solver and one for the symbol, execution engine, and then you have all those files for the um for the whole engine.

A

So what we want to do is like write, an interpreter. How do we write interpreter? We need so by the way. Please, if you have questions just like try to you, can ask questions right now, just to make sure we we go and um in a good flow.

A

um Actually, it's not here so usually when you write this interpreter for evm, you have this context. What is the context? You have the code that are executing you have the program counter like what which upgrade? Are you executing right? Now? We have a stack in our case. It's going to be a symbolic stack.

A

um Don't worry about that now we have a path which, basically, it's a it's- a path of all the program like of the program counters that were visited in the in the jumps and we're going to use this to detect, loops and exit, because we don't want to encode loops. We have um an array of constraints. This is what I showed before like. When you see the require, it says, require a class or equal 10. We go into that Branch.

A

So we keep that constraint because that thing needs to be true for the rest of the execution, um and this counter variable is just a um accounted to help create new variables. So when we were creating new variables for the Expressions, X, Y and Z, and so on here we're going to be expression, one expression, two expression, three and so on, and they need to be different in the branches that we execute.

A

So that's it. We have the context um ignore the rest. For now, let's jump right into the execution engine, so we have this. Recursive function called run from which takes our context. So here you see it's basically gonna Traverse. All the up codes select the opcode.

A

This is just a check um that we just exit early in Loops. We it becomes an under proximation, but we don't want to do loops.

A

We extend the path with the Disney opcode, and here is the part that the first part of the what I mentioned with The Interpreter. We need to care about Stack Up codes because they're going to add some numbers and a bunch of different things, jump locations, jump destinations that we will need when, when building our constraints, so this just does the usual um stack handling. So if it's a swap you're gonna go into the stack and swap the numbers, if it's a dupe you're going to duplicate whatever it needs to duplicate it.

A

If it's a push, you just push that number into the stack here. The only thing we do is apply a function on the stack arguments, which is so, for example, if you have an ad we're not going to encode the ad precisely here, but we do need to consume the stack slots and put a new return value there right. So this basically just uses these handlers. We have internally it's like a bunch of function, pointers um to if you have an ad.

A

So this is generic for, like all the all the up girls, we don't care about. It takes the number of arguments this op code takes pops. All of them from the stack creates a new work. What we call symbolic variable so like a new expression, 13 or whatever here, and puts that expression on the stack um and we don't really have. We don't really care what it looks.

A

um What it looks like right now, we don't really care what kind of constraints we have over it and and here's a part of the that we actually care about the where we do the check. So if we have a jump every time we see a conditional jump, we take the the argument of that jump. We take the condition that makes it jump and we ask the solver: is it possible that we can't jump to that location, because this is before we had this?

A

This required an if right, so we have require access or uh X Plus, then or equal to 10.. So we have that saved. X must be less or equal to 10., and then we see, if x, greater than 50, and then we ask. Is it possible, though that is that X is greater than 50.. So at this point, that's when we um we have all the math things encoded already in here as you'll see this make symbol. This is like internal helpers, not important right now, so here's where we do the check.

A

So we check if the op code is relational, so if you have a less than or greater than or if it's an e0, because if, if we needed a greater or equal, we don't have greater or equal in the VM, so we need to do is zero um less than right so and similarly for um less than or equal. So if it's one of these, we basically take the the condition which is here. We transform it into an DL expression, difference, logic, expression um and basically call this over.

A

So we have this check here, which will take all the constraints and we'll call this little DL server. That I mentioned, um which- and this is the check we call this over and if the server says unsut, then we say this branch is unreachable. Why unsat? Because if the branches, if the branch conditions are unsatisfiable together, it means that um the silver will say unsatisfiable right, and this means that that part is not reachable because there's something in in the middle that is not allowing that will not make the code.

A

The code, the code path, is basically going to be inconsistent um and what the silver looks like is yeah. This is the entire silver, so you take the constraints. So here you just build the graph, so this is built in the graph here. You just need to know how many variables you have.

A

um This is still building the graph and then Here We Run The, this single, the single source for this path, algorithm, which is the first part of the solver, which is basically yeah. It's a very basic graph algorithm. Then we did a negative cycle detection and that's really all the silver does. This is and 20 lines of code. It's really simple and um yeah. It's a it's a logic that I really like, because it can do a lot of things while being very, very simple.

A

um The last thing that I want to show is: how do you use this? So here I have this contract unreachable. That has a bunch of functions and that's like some unreachable branches. In each of these functions, all we need to do to test. That is really just this. We call the Sim run function from the library from the symbolic symbolic execution Library, with the runtime code from the contract.

A

That's really all and here's a simpler thing, just like manually, um just a simple test with somebody care that I know what it does and if you run this yeah.

B

A

Here, you'll see that um this is the complicated case with all the solidity high level functions and it's not the best way to report the things, but it reports. It emits an event that says unreachable Branch with the pc255. This tiny example. So it's this is the same as I showed in solidity just like in written quickly in yule, and this is the bytecode that it generates.

A

um Well, that I wrote manually, and um so we can quickly compute This Together keeping track of the stack, and then you see what it what it actually does in execution. So push zero we're going to push zero. Then we just called it a load of zero. It's going to give us some X, then we push 10.

A

We duplicate the X we do less than so. This is going to turn into this. This is the stack by the way and the top is the higher position. So now we push tag 0b and we do the like a conditional jump where the false Branch stops. So we don't care about the first Branch. All we do is just so you're gonna pop um we're gonna pop this first two arguments right because of the jump, but because we go into a branch. This condition must be true for the rest of execution right set of constraints.

A

So we keep going in tag, one jump, Dash dup, we duplicate X. Again we push 50., we do an LT now and which consumes the X, and this becomes top of the stack. Just a symbolic expression like Y equals X length less than fifth less than x, we push 14, and then we jump 2 and then, at this point, when we see the jump, we're going to ask the solver, is it possible that this new condition 50 as an X, is consistent with what we already have X less than 10?

A

And it's always going to say: that's not possible, and at this point here precisely at this jump, I, that's where we basically stop and say this Branch here is: is the true Branch like where you're jumping next is um unsatisfiable, so you can actually remove that entire Branch right but yeah. So there's a lot of code behind that there's a lot of helpers. The main intuition was basically this algorithm of just like run an interpreter caring about if you're killed, not caring about other up codes and yeah I'm happy to take questions.

C

uh Super cool talk: this is wild. You can do this in solidity. I'm wondering about overflow, though, uh because your researching at the beginning was that that one example you showed was impossible, but it is very possible in the presence of overflow.

A

No, that one wasn't because you need the answer to be minus one-third, so it's not going to be possible.

C

um Okay, sure yeah, but it doesn't look like you, handle overflow anymore yeah, no right yeah exactly so. That means that your results are not correct.

A

Yeah exactly there's a bunch of soundness stuff. You have to add to this. Okay, all right. Thank.

B

You sorry I didn't see, but is this code somewhere available to.

A

Yeah, this repo github.com um that thing and there's probably bugs in there, though, so feel free to fix them.

D

um So since you wrote this in solidity I do you have any thoughts on why you would want this to be executed on chain.

A

Not at all, okay should not run this Unchained yeah well, actually, so, if I wait, let me quickly just look how much gas this takes.

A

For this tiny program.

D

You said that for a given program, there's a lot of different encodings you could have. Can you give a few other ideas of other encodings and what would be the trade-offs.

A

Yeah, so this encoding uses um this encoding basically chooses which has a difference logic, because the solver is very simple, so we could write in solidity right, so the the encoding is tailored to become systems of inequalities that look like the constraints that a DL solver would take. But where is it now um in Harris talk actually which I have here?

A

There are different.

A

So if you wanna, if you actually want to encode, add mold div all these kind of things, you will need more complicated constraints like linear combinations, where is it Harry yeah you'll need linear combinations like this, for example, and more complicated constraints and you'll need like a Simplex or integer linear, programming thing or even in non-linear, is over depending, and these things are a lot more complicated. So Simplex is well it's it's an exponential algorithm that kind of happens to run mostly in polynomial time these days, but in all linear, non-linear Earth.

A

If you're trying to solve nonlinear constraints, that's an undetable problem and you're going to have a hard time solving it. So.