# hevm or: How I Learned to Stop Worrying and Love the Symbolic Execution by Mate Soos | Devcon SEA

- Speakers: [Mate Soos](https://streameth.org/speakers/mate-soos)
- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2025-10-09
- Duration: 26:28
- Topics: Science & Technology
- Watch: https://streameth.org/watch/yt-o89CWZc2i1w
- YouTube: https://www.youtube.com/watch?v=o89CWZc2i1w

## Description

hevm is a symbolic execution engine for the EVM that can prove safety properties for EVM bytecode or verify semantic equivalence between two bytecode objects. It exposes a user-friendly API in Solidity that allows you to define symbolic tests using almost exactly the same syntax as usual unit tests.

In this talk, we'll present hevm, what it's useful for, and when and how to use it to help secure your digital contracts.

Speaker(s): Mate Soos
Skill level: Intermediate
Track: Security
Keywords: Security, Fuzzing, EVM

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

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.

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon SEA was held in Bangkok, Thailand on Nov 12 - Nov 15, 2024.
Devcon is organized and presented by the Ethereum Foundation. To find out more, please visit https://ethereum.foundation/

## Transcript

[Music] hi everyone uh I'm Matthew sa and I'll be talking about hm and symbolic execution uh that we built together with Lexi myself and Zoe uh we are part of the uh Argo Collective uh that is a recently spun out uh Collective from the Ean Foundation um if you want a bit more about the Argo Collective you can watch our uh 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 hvm then I'll explain how hvm can be used uh within uh you know to to secure down some of your um work that you have done hopefully and then finally uh I'm going to conclude this talk so uh first of all what is symbolic execution so let's say that your code looks like this um if you try to do fuzzing on this code it will likely not find theault that is uh marked by assert false which could be for example something that drains your contract or locks your funds or some kind of negative event um so if you you can keep fuzzing this forever essentially and um nothing will happen but if you uh run symbolic execution on this it will immediately hit the the assert false and will give you the solution the the the two integers that you need to pass in to um to trigger the the failure so this is a good sort of litmus test of what uh symbolic execution can do in comparison to to fuzzing of course it can do more but this is a good example where where fuzzing will 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 uh traditional assembly I'm I'm I'm old school uh I could have used evm assembly but it's more or less the same so what we're going to do here is uh I'm going to Showcase a very simple uh straight line program where we do a mo and and a move and an ad uh with two registers so here we have uh concrete execution on the on the top and what you have is um concrete value like one and two and then the Mau will move the the value two to um to to the a register and then it will add uh four to this value and then the final register state will be six and two now um when it comes to symbolic execution what it will do is uh it will instead of initializing it with concrete values like one and two 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 um we have the state evolve and eventually it will end up with v2+ 4 on the on the ax a register and V2 on the on the B register so of course if I substitute the the concrete values into into that will end up exactly where we were um with concrete execution but what this means is that I can um mathematically Express uh what is the state for any input value right um and okay 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 um a a program where we have a branch and uh with concrete execution it's relatively straightforward we have both uh registers set as one then we're going to check whether they are equal they are happen to be equal and if they are true then we're going to add five to the uh to the register a and so the the the the final uh state is six and one right so this is quite clear but when it comes to U symbolic execution we don't know of course what the value of a and b is uh we represent them as these symbolic variables V1 and V2 and we need to check for both potential uh execution paths in this case when uh V1 is equal to V2 and when V 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 B1 uh has is incremented by five and in in um in uh in the other case B1 is incremented by four of course again if I substitute the con 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 if there's another Branch then this can become of course exponentially large number of um exponentially large number of of of potential end States um if there's a loop of course that can be if it's infinite Loop there 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 if ever the loop uh condition is is reached and so we can potentially Run Forever um so I'm just going to talk a little bit about what other uh symbol execution uh systems are out there uh before I jump into hvm um first of all there's there's more or less two typ types within uh this ecosystem as far as I understand one of them is um you have a static code analysis engine and now you want to validate whether some of the things that it spits out are uh 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'll do is you'll just simply uh spit out the the potential false positive and let the user deal with it um and that's fine but in our case we actually don't use the static code analysis engine as a as a as a precursor to hvm so we actually have to deal with everything that uh the evm has to offer um and U so it's a bit more complicated and it's also more complete of course uh so these purely symbolic execution uh framework based systems there is uh there are number uh this seror approver which is based on this uh backwards exploration and and weakest precondition computation there's ebmc which is of course as the name suggests abound in mulch ER type system then there is halmos it's written in Python and then there then there's kevm which is based on the K framework and allows you to break out into into K in case uh you need to prove some things for example Loop termination or invariance and things like that um so just a bit of an overview of hvm so it started a long time ago as part of the D tools project um it implements the evm semantics um both concretely and symb and actually a kidna fuzer if you know about it it uses hvm underneath uh for the concrete execution semantics um it uh it it um is um possible to execute uh any any um uh call from any potential state in the the evm so it understands um a lot of like all of the evm in terms of like for example calling out for to an RPC to a to an an AR arive node to fetch State uh Etc um it runs it basically computes a a query to an smt solver runs the smt uh uh runs the smt solver to to get the the response to the query and then interprets this uh response and uh sends it back to the displays it back to the user in a in in a in a fashion that is um more user friendly than some smt uh output we'll we'll see that in a moment um so there two ways of using hvm one of them is uh for counter example generation and one of them is equivalence checking so let's talk a little bit about this uh counter example generation for um um in this case and and some kind of post condition that typically is written for example in in in Forge test case as a Forge test case um so here we have solidity Viper whatever language you prefer or even just pure evm bite code and that gets interpreted uh by the by the internal um um symbolic execution engine inside uh um symbolic interpreter inside uh htbm to produce an intermediate representation and then this intermediate representation together with the post condition that you put down uh gets compiled into a logical formula that gets sent out to the smt solver and smt solver is what's called a sub model the solver so it understands for example bit Vector arithmetic which is which is quite useful because of course there's these 256 bit bit vectors or variables in in in evm that evm operates on and then either it proves the property um finds a counter example or times out of course that's always a potential possibility um when it comes to uh ex um symbolic execution for equivalence checking we do something very similar but what we do uh eventually is that um we try to compare the two executions against each other so you have uh bite code a and by code B let's say that M code B is like a refactored by code 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 prove that it is equivalent find the counter example so some input or in state that where the two contracts actually uh disagree or of course there's always the potential for timeout and um let's go a little bit deeper into this kind of symbolic execution engine uh inside inside hvm so it operates on bite code which means that we're not tied to any particular uh um uh compiler we're not even tied to something like Ule for example um understands all of the evm stack call frame Stack Storage call data everything um can as I mentioned it can actually run at any point in the blockchain history um and it is fasted against the concrete execution semantics of gath in this case um as mentioned like it has issues with uh loops and recursions because of uh this issue that unterminated Loops we don't know when to stop um it has some issues related to symbolic uh offsize and and memory copy this is purely due to smt limitations and um doesn't currently deal with symbolic gas so it basically ignores gas when it comes to a symbolic execution um in concrete execution of course it understands gas and we'll deal with it and so achidna will be running correctly in that sense um 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 bite code then it will um um 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 cat shck and arrays and and maps and things like that that are quite specific when it comes to uh to How uh the evm handles uh arrays and maps and things like that so especially katak which is very complicated to uh to put to exactly represent in in smt and 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 um and then we gather all the all the results from the asmt solvers and then get the counter examples extract them and and rep and map them back to the query that was originally dispatched and see how how we can display that to the user in a way that they will be able to run this and and 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 um so that's kind of the the high Lev of the internals um 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 uh box in the previous box that you um that I showed so here's a simple function right uh this will overflow uh if if uh the variable that you push put in is large enough in particular exactly equal to 2^ 256 minus one and uh B will actually not be larger than a in this particular case I'm sure you have um played around with this uh it's a very trivial uh overflow issue and this gets compiled into this intermediate representation where we have a proposition that a must be uh um smaller than the A+ one right 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 um and uh it can be quite um like understandable to a human how the internal representation um Maps back to the original code in this case it's quite quite clear um okay so I'm going to talk a little bit about uh about uh how to actually run this tool and what kind of results you can expect so in this particular case we have uh Forge standard test that we're going to 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 uh Z3 which is one of the um smt solvers that we we uh we support and you need uh hvm binary that you can just download from the repository and uh 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 uh the EST and uh run hvm test and it will parse everything up and do its magic and eventually give you a counter example which is what you expect so um this um is sort of the the base way of using it um and it is as clean and tidy as it looks on the on the on the output I did not actually change that or edit it or didn't even even the the the spacing is is how it is so it's quite visually uh representative of what are you going to test and what are the counter examples that come out if there's more than Comm one counter example there's going to be more than one listed there so how does HM equivalence work uh here I'm just going to show um sort of a a contracted uh thing uh it's a very complicated uh code that was um someone tried to uh 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 is uh two codes and we want to know if they're equivalent um uh you see that it emits a warning that we cannot actually explore the whole thing in this particular case due to a a call into Unown code obviously we don't know what's going to happen there uh like what is going to get executed um but beyond that it says okay well anyway I powered through like I'm going to ignore these bits and pieces we have um 1.7 million end states that we need to check for equivalence and then it says okay well I tried my very best there's 93 of them uh I couldn't do because of of uh this memory uh that was a memory copy that is that is symbolic I couldn't do two because of timeout this actually had a 15-second timeout for each uh each query and eventually I couldn't find any discrepancies given these warnings and and and uh things that I couldn't actually explore uh and if you have a look this actually ran for like 34 minutes and 45,000 seconds so obviously it was like uh a multicore machine that did this um so it doesn't like give up and like error exit or something like that it actually gives you a meaningful output and of course this did actually check 1.5 7 million end States so it didn't uh it didn't do nothing even though of course you can't completely trust this because uh there are some parts that were not explored as as displayed um right so I'm just going to give you a bit of a references and and and pro tips of how you might want to use uh hvm so first of all of course there's the hvm reposit there's also a very extensive user guide we have worked quite a bit on it uh lately and uh it really does give uh a rundown uh step by step how to um the kind of outputs you can expect Etc so it also explains for example some of these warnings that here are of course quite thirst because we don't want to overwhelm the user in the in this with the output um just few Pro tips regarding using hbm so I would uh recommend for example using it for equivalence testing the uh the the one that I showed you was specifically done by one of the compiler teams um who wanted to check if their optimization or new idea uh actually doesn't break uh the the the what the contract is expected to do that the compiled contract is expected to do um so it's quite useful in case you want to refactor or if you want to do some gas optimized codes it can be useful um if you write a lot of tests and eventually your your tests are going to be your specification and that can be quite nice as a driver for uh for maybe thinking about your contract in terms of like what it's supposed to do rather than what the code says it's doing um and of course um I encourage you to do uh test positive tests negative tests and invariant tests um U for example like a positive test is what we expect for example somebody types in I mean in a normal situation not in a in a in in this one that positive test would be you type in the password uh and the password is correct and you're logged in if you type in the wrong password you're not logged in an invariant pass an invariant in this case would be for example in the space of a blockchain would be that uh after transfer the sum of balances is the same right um and even if EV just a note so even if hbm test gives you warnings and and and and shows you that some of the things it couldn't do it doesn't mean that it's us in any way shape or form you're not supposed to uh like complete coverage is kind of a myth or something we want to get to but it's very very difficult and what you normally get is a certain level of certainty and uh hvm can help you improve this and and Elevate uh your level of of assurance of your contracts correctness and at the end of the day that's what we're aiming for of course it'd be very nice to have it all the way but this is uh this I think is also very helpful um especially because um it's more complete than just a fast test so limitations I think I've explained this before so there's issues with loops there is issues with recursion um and there are some issues with complicated mathematical expressions like exponentiation modular division things like that um purely because it's complicated on a 256bit variable um for future work we're planning to help uh fix some of the hopefully fix some of the issues regarding recursion and loops with some form of CHC and um potentially hopefully we'll help some some some better uh jump D handling but also maybe EF will help with that um so in case you want to there is of course the the um the QR code and uh check it out have a look see what you can do it should just work out of the box with your currently running tests thank you that was an excellent presentation can you come a bit forward oh yeah sure okay so let's start with the questions uh is uh acvm better than other tools such as ctor or halmos in terms of uh compatibility with Foundry easiness to use Etc so I guess it's a more devx question okay um I would not compare it necessarily to Cur Cur has its own verification language it's a multi-million dollar company um it's a different ball game Al together um um I would I mean but nevertheless actually hbm does very well even though I would say from the perspective of what it's supposed to aim to do is slightly different of course uh we don't have a specific I mean not a specification language per se we have these uh test cases which eventually become your specification um regarding halmos I mean I really like halmos uh so I I think um it's always fun to have more than one uh tool available for doing whatever you want to do not only because you know if one of them doesn't work then you can try the other but also because the two two two from a development perspective of the tool itself um of course it's nice to see what harash is doing and we copy something from them and then they copy something from us and that's a what's called cross pollination and this this is very normal in any field including scientific Fields so compare I I I I don't know I I'm not a big fan of this kind of competition mindset I think it's nice to coexist and and work together and I'd like to do that with both Cur and H yeah uh so the next question is uh if we should avoid Loops in code or in more General how can we write code in a more verification friendly way yeah good question uh yes no Loops please I mean in in in in general not a good idea to have unbounded loops because it can run forever it will eat your gas um you can hardly reason about it in in a you know from from like what is it actually going to do um so I think it's not a great idea to have uh unbounded loops and you should minimize the number of Loops you have in general in your code um I mean that also goes for recursion for the same reasons um um yeah I mean you can there are ways of K like K evm uh can can break out and and you can try to write some in variants and things like that um hopefully we'll be able to do something like that maybe with some with uh including the loops into I our ir and and maybe we'll be able to do something with that too that' be very fun and interesting but in general you know you're not only making our life harder you're also making your own life harder so perhaps avoiding it is the best way to go the next question is uh how do you deal with the path explosion problem um we compile 1.7 million queries and run them in 34 minutes that's I that's the best way I can talk about it because enough in the end of the day you know it will happen but uh you power through it I mean um how does c do it they have a a form of servers and then 1.7 million quers get run in 5 minutes instead of 34 minutes I mean you can also do that with hbm it's not a big deal um at one point it's going to be pretty cheap to do that relative to how much money you're going to lose by not having it mhm I guess the next three questions can be maybe answered in one go so oops uh is there any reason to use Z3 over cvc4 CVC 5 do you use multiple SMD solvers yes so actually I don't know if it's publicly at but there will be a very interesting tool in regards you know what is best um from the halmos team I'm very excited for that um I personally of course am a big fan of bwoods law and the team Behind bwoods law I know them and I trust them and I like them um um I also like Z3 I if you know Nikolai um it's he he's a very uh he's very good at what he's doing so I have I I'm still on the side of collaboration and and friendly competition and so anything Works anything as as long as it works I'm happy um so you can use actually any solver you just do minus minus solver and uh do your own thing you can also add your own if you like um you can even add the wrapper and then uh run any smt solver instead of you can even write your own like I think now even STP might work like I used to write STP so uh although I was not very good at it but I did I did I did also contribute to STP so I guess last question how hard are your kak constraints are on the solver um we use un the theory of uninterpreted functions to deal with catak that's the best way I think to deal with this particular issue um I'm not going to go into details because we're running out of time but basically cck is a very complicated function and and representing it exactly is a very bad idea so we and I think many others using uninterpreted the theory of uninterpreted functions to deal with it it has some downsides and it can be problematic but if you do a lot of rewrites on your maps and arrays uh actually they can also completely go away so with a good simplification routine and um and um the best potential way of of doing this kind of uh use of uninterpreted functions to deal with catak I think uh we can get there it can be an issue but I think um with some luck and and with perhaps even better rewrite rules uh it's not such a big issue great let's thank uh mat one more time [Applause]