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

foreign [Music] 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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. 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 so 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 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. 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 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 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 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 no that one wasn't because you need the answer to be minus one-third so it's not going to be possible 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 yeah exactly there's a bunch of soundness stuff you have to add to this okay all right thank you sorry I didn't see but is this code somewhere available to uh yeah this repo github.com um that thing and there's probably bugs in there though so feel free to fix them 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 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 for this tiny program 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 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 there are different 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 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