HEVM, a smart contract verification tool | Mate Soos (October 2023)

hi everyone um I'm M I work at the foundation and I work onm uh that is a smart contact verification tool that I will be talking about today um just in general I'm going to try to call this structure so I'm just going to give a bit of an overview what BBM is um how to actually use it and in case you want to contribute uh to the tool and I'll try to contribute or uh I'll try to um wrap it up at the end to you know see how you can make use of this tool in your own workflows so just a little bit of a recap uh testing usually follow is is a discipline and usually follows a testing strategy that you should have for your own tools this of course is true for almost everything you build but especially in in space s uh let's say risky as uh building tools that potentially can have billions of of Eur uh you better have some form of testing strategy and that testing strategy usually encompasses something within this this uh test What's called the test triangle which is usually you know starts from the very bottom with unit tests like very small unit tests all the way to the almost to the top it's this user acceptance testing which is almost like the end API testing that you would do and then on top of that Ty you pay testing company or yourself also do some kind of exploratory testing right so this is how a testing strategy could look like there's of course other parts and bent pieces but anyway that's a testing strategy that you could have and many large organizations would normally have um and um as part of these tests usually you have different kinds of tests like does it actually work at all like does the API like work the way that I expect it to work but you would normally also have something called negative tests and positive tests and in the for for example a negative test would be that you um you check against the system going into a known bad State and a positive test would be that you check that the um the uh the the system performs as expected and holds the invariance that you expected to hold so um you can do this kind of testing and uh HDM would try to help with some of this um in the following way so but the way hbm works is that it has uh a concrete semantic execution of evm bite code that is to say that you can you can handcraft your evm bite code and execute it you can also take something off of the blockchain that you don't know the solidity uh code for it you only know the ebm B code that actually gets executed and you can take that and execute it concretely within hbm so just like get or you can execute it symbolically and the way the symbolic execution works is that you it takes um uh um some kind of input as a known bad state or an invariant that you want to check against um examines all the execution paths that can be taken within this within this execution find the set of requirements to satisfy or invalidate your invariance or satisfy the known bad uh States and then runs an external tool to try to figure out ways to satisfy these requirements and eventually I print to you um a set of inputs that will trigger those uh known bad States or invalidate your invariance that you want to have so let me show you an example because I think that might be a bit easier um here's for example uh and I'm going to use solidity because I guess that's kind of easier for people to read than EDM bite code so here is a simple the code uh obviously what you do is you put into a something that is really large and it will overflow and therefore B will actually not be larger than a because it becomes zero right so this is a very classical thing of course you see you can see the unchecked there because I want this to be unchecked otherwise solidity will actually put a check around this and this will never hold so H in this case will trally find the uh the the the case where a is all the FFF and uh we'll actually output you a a call that is to say will tell you that you need to call this function uh with a equals to this large number and this would trigger the known bad state so this is this known B state that you want don't want to happen so let's say that you would say okay well that's quite easy because I can trigger that with a fuzzer like I guess do you know does anybody like hands up if you know what a fuzzer is okay so that's quite a lot of people so the others who are not familiar with the fuzzer the fuzzer what it does is that it puts in basically random values into the um in this case the function parameters so A and B for example and tries to put in a lot of different random numbers and see if you can trigger any of the assert false fails that are in this case right there now the problem with something like that is that you would have to like try a lot of different numbers to figure out that those two numbers actually trigger this and so this is kind of like trying to find a needle in a Hast there if your program can be can be forced to fail quite easily or can be easily faulted with like special numbers that are known for example the z f f FF is a very ZX FF is a very welln sort of problematic number um then you will have a trouble trying to find these kind of faults whereas symbolic execution will immediately find this this problem no no with within a second and you can run this on a fuzzer and I'm pretty sure none of the fuzzer will actually figure this thing out um of course I could use much more complicated mathematics here and hbm will just do the trick anywhere so this is kind of the difference between Sim execution and fuzzing there's more to it of course but the bottom line is that the um the the symbolic execution will be sort of slow and smart whereas the fuzzing will be fast and kind of dumb it will run the concrete semantics it's quite easy to do you can just run Gap if you really want it to and it will uh run it really really fast and try it with many different values and then hopefully it triggers the fault and now you discover that there's a problem but if it doesn't then you are stuck because it will never prove to you that there is no such input whereas hm will actually compute that there is no such input or if there is it will actually give you a counter example that is to say a way to call this function um right so now that was the known bug and then how to do invariance so an invariant in your code is for example you want to make sure that the total balance of all your tokens is X and you assume you basically put this require at the beginning of each of your functions for example in this case you put a require there and say well I require that the invariant holds at the beginning of this function let's say a transfer function and you require that the the invariant hold at the end as well but instead of require you put an assert so now in case at the end of your function invariant doesn't hold then this tool can actually find a way to execute your your function such that the invariant holds at the beginning but doesn't hold at the end so something went wrong within your within your system right and this can be very helpful in case you know your invariance of course you need to write your invariance this thing doesn't know what is your invariance it doesn't understand that for example maybe your invariant is not that all tokens must the total sum of all tokens must be the same fixed value but instead it must be to like always is decreasing so now you have to describe that as an invariant instead of you know it needs to be a fixed value right um the other thing that the hbm can also do which is quite nice is that sometimes you'll see that people ride custom evm by code just because they want to make sure that their gas costs are as low as possible or maybe other reasons one of them would be that you want to minimize your gas costs and what that means is that sometimes there's a very simple function that you could use which is on the left but it uses a lot of gas and there is one that you came up with which seems to use a lot less gas and does seems to do the same exact thing now HDM can actually validate that it does exactly the same thing so the tool will behave in all potential cases the same way so this is called equivalence checking and it can give you assurance that your handwritten you know master code that you wrote on the ey is actually the same as the thing that you can actually review and understand better on the left right so this can help you gain Assurance right so all testing is basically just trying to gain assurance that the system does what you expect it to do it's up to you to Define what the expectation is of course but uh hbm can help you do that so there are some as with every other tool hbm has its only set of mations one of them can be that for example Loop can be Loops can be challenging so if you have a loop in your code then remember that this is symbolic execution which means that it tries to do every single potential Branch it doesn't just try one branch as the concrete execution will do right the concrete execution substitutes the concrete values that it guesses runs it and says well it didn't seem to have done anything wrong let's try another concrete R in this case that's not that's not what we're doing right what we're doing is that we try every single potential way of executing the system and if there's an infinite Loop then it will we will actually Loop infinitely uh which means that we'll never terminate which me quite bad so instead what we do is that we actually limit ourselves to a number of Loop iterations and we'll warn the user that this is all we could do because we can't run infinitely um and so that Loops can be challenging we actually have an option for that but still it can especially Loops within Loops etc etc um recursion which is just another way of doing Loops basically can be a bit of a problem especially if you call yourself right that's basically just another loop um complicated mathematical uh uh Expressions can be a challenge uh because in complete execution if it's just an exponentiation it's an exponentiation you can actually sometimes use the uh the builtin assembly instructions into the CPU to do quite fast in our case we actually have to symbolically describe the uh the exponentiation which can be quite complicated um and um you could um we while in concrete case in concrete execution it doesn't quite help for example that you put requires at the beginning all your functions describing the known things that that you know are correct right now about the program but for us if you actually describe those things then we can limit the number of branches that we need to go through right so if you know some kind of invariant always holds at the beginning of the program and you add that as a require then we will actually run faster because we don't have to run those those branches so we can prune branches away which is it's not really a limitation but it's something to look out for when you're writing your code and finally HDM itself is not verified code so while it does some verification and uses some tools that do verification the the transformation that we do and the interpretations that we do of your B code is not actually verified so there could be a bug in hbm and we could potentially say that you know we have found no bug in your code but actually we made a mistake so that's always a possibility so let's let's just talk a little bit about how the system actually works um so right so the way this actually works is that we um we we do an interpretation of the by code a line by line interpretation just like you would do with a conrete execution system except that instead of describing a single execution through this uh set of instructions we describe a mathematical equation for every single like we we build up a mathematical equation that step by step gets of course larger and larger as we keep on interpreting and in case there is a branch like a jump instruction a conditional jump instruction then we Branch we actually start we do two right so we start writing um effectively the the the equation gets doubled and we we execute both branches and then make a gigantic Global um equation at the end about expression let's put it that way not an equation and that gigantic um expression at the end will need to be uh checked for all their potential final States whether any of them validates the um the um the invariance or triggers any of the um bad states that you were uh interested in checking for so for example here's a relatively simple function uh the one that we have seen before we trying to uh see if I can add one to a value and make it smaller than the initial value right and there is indeed one like this the 0x that value and um in this particular case the um the final uh the final uh expression that will come out for us is this one at the bottom which basically just says if I add to variable A1 then it will be less than equal to variable a right so it's relatively easily readable this is effectively a mathematical equation if you think about it just from high school and um most uh I mean in this particular case we know that this is within a modular arithmetic and so this will be possible of course this will not be possible in the in the case of infinite integers but this is not infinite diges this is the ebm so we have 256 bit semantics and this will roll around and what we do is once we have created this expression as you see at the bottom is it will now translate this to something called an SM SMP L an SNP is a set of theories and in this particular case we use the the theory of bit vectors which means that um we uh use an external tool for example Z3 if you have ever heard of this uh tool um to uh try to solve this equation so basically we have the equation that you see at the top and we don't try to solve this equation instead we give this to an external tool and ask this external tool is there a solution to this equation and the external tool actually gives the answer at the bottom as you can see it's exactly the counter example that we were looking for and now we'll parse this uh count for example um for the user and give the the the offending a call as a as an output so that you can actually um test it yourself like you can you can write the test case and show someone that hey you know there is actually a bug in this in this system either because in this case you enter a known wrong state or because you can invalidate the invariant you know the invariant propell at the beginning of the function and no longer BS at the end of the function so therefore uh there's a way to to invalidate your assumptions about about the system so this is kind of just to understand how HDM works like more like internal and how it could be used from the perspective of um of U fing strategy uh sorry a testing strategy and with that this is basically a form it's not really a puzzer it's a ho but normally it would be used in conjunction with the and now I just want to show you how to do this like actually by hand so how do you actually do this well uh you can um you can get you can Foundry I guess you know what Foundry is um many people use it for uh for for building a and and and and and and uh well creating um projects on projects on top of eum then there is uh of course hbm itself and you would also need a version of Z 3 in this case and basically you add this uh function with a prove underscore in front of it and then Forge build an HPM test and that's it it will forche build will of course build or your or your files or your solid defies and HDM test will find these Json files for them all up check where any of them has a pro in front of it and then try to find a way to uh to to count account for example basically to to trigger this search failure and we also have a a repository for benchmarks where uh in case you have found something that you know for example hbm struggled with or hbm had some bugs um or if you have found that another tool in this case hmos did perform better than HDM then you can contribute back to us um to uh so that we can actually improve uh the performance of of of hbm for the particular cases that you have found that it wasn't doing very well um this Ben Mark repositor is actually maintained not only by us but also by the halmos team so that's another tool that we can try to use that has a very similar interface uh for for uh users and finally in case you have found uh hbm to be maybe not as good as you would have liked it to be although I really hope that it will be as good as you would have liked it to be I think it's actually very exciting uh as a as a tool uh on its own but of course nothing is perfect then here you'll find um ways to contribute um maybe I just want to show you at the very bottom like what are the kind of things that is possible to do in case you want to improve the performance of HDM it's not as complicated as it seems for example this is nothing but a a rewrite rule so it will say that if you add zero to a number then of course it will be the original number so in this case we're adding a and b and if B is zero then it's just a and if a is zero then it's just B and otherwise it's a plus b these kind of rules are sound quite simple but they they help simplify the equ the equation down the expression down that we uh that we talked about and then can significantly improve the performance of the tool so these kind of relatively simple so I guess most people would see this to be quite of elementary mathematics and these kind of Elementary mathematical rules can actually improve the performance of the tools so if you have ideas they're very much welcome okay I'm going to try to wrap up quite quick um so I mean as a as a conclusion I think I I just want to say that HDM of course is not a standard tool that now you have run your your problem like your your your um your uh contract through HDM and now finally it is complet completely secure that's not how it works hm is part of your stress testing strategy so there should be a lot of unique tests and and and and integration tests and end user tests and exploratory testing and then as part some as part of some of that there should be some fast testing and as part of that there should be some um proving that some of those fast tests can actually not be triggered neither by fuzzing nor by uh symbolic execution and so therefore hbm should be a tool that can help basically give you more confidence in the correctness of your um of your system one thing that I think is quite interesting with an htbm is that because it forces your hand to both think of the kind of invariance you would like to have and to think about all the bad States you want don't want the system to end up in it should help you think more from a higher level about the kind of things that your system should be doing and should not be doing rather than individual function calls individual overflows Etc so if you think of HDM as this kind of tool that can help you uh create a higher level understanding of what your your contract or your your system should be doing then it has already helped um hopefully it can do more but that's maybe a change of perspective that it can sort of force uh people to have I think that's all for the moment but you'll have probably questions thank you for the presentation interesting and I have a question um Ian you mentioned that you are able to build like equation from the code right so these are linear or nonlinear equation good question so um it depends on what's inside your uh code so in case your code for example I mean this code here uh this code here this cre add will only have a linear arithmetic in there right because it only has an an an addition a multiple addition in here but in case your tool has a multip multiplication in it or exponentiation in it then we're talking about nonlinear arithmetic and that will be quite complicated um yeah so it will become quite complicated of course it's still modular whatever and in paper it's all doable but um practically speaking it gets much harder and you will see these kind of tools um struggle quite a bit it also depends on the type of uh solver you use eventually because we support many different solvers to run your your problem on I'm just trying to find so here this& expression that I show in the middle this can be parsed up by up to five different tools that comes off top of my head and they will happily try to solve it so some of them will perform better and others will perform worse but um it mostly depends on the kind of code you're writing I mean if the code is mostly about um logic like branching logic of like how you know if this happens if that happen then that's there's no you know there's not even arithmetic in there right it's just an if and S but if your code suddenly becomes something quite complicated like some economic incentive that you know we're going to give 0.05% of this to that now percent is a multiplication right so now we're in yeah okay now the question because was not this question my question is I mean if you have this linear system of equation that is describing your codes are you able to like investigate this the state Matrix so for example trying to find out value vur to try to explore the property of the codes like exploring linear algebra uh basic features so I mean how in the physics you equation to describe a system right and then you analyze the state Matrix to investigate the property of the system in this case if you are able to build a system of equation describing the code is it possible or makes no sense no so what we actually do is that we describe for each end State okay so the you know program starts in terminates right I think if it doesn't terate I think we can just forget about it for the moment because we're going to run out of gas at one point so you know it terminates at one point so it has an end in a beginning so this beginning in end is one is one of these fairies that will end up and this describes completely what happens within this execution Trace right and so then we can ask queries whether this you know execution State validates one of your invariants well invalidates one of your invariant so we only ask that now there could be other questions asked for example can you compute an invariant that holds for every single execution right there would be another question to be asked uh but we don't do that but that would be an interesting problem but I would say that's more like more towards research I mean this is also quite researchy but that's even more like sort of even more Uncharted Territory but it would be interesting to see if you can basically you you give me your contract and I tell you these are thear that hold about your contract that would be maybe interesting because then you know the programmer could say okay well this invariant I want and I didn't expect that in variant and then you can try to you know that they might find some issues with that um you can also flip this around of course and say okay how are what are the different kinds of ways you can uh execute your program and given these uh this symbolic interpretation you could potentially create a set of test suits out of nowhere that actually runs all the different ways you can execute this thing so I tell you I give you a a test suit given the code which is quite powerful if you think about it uh but we don't do that either it's interesting and maybe one day I guess but it's not the goal right okay thank you very much yeah thanks for the presentation um can can you talk a bit about I mean it's probably difficult but can you talk a bit about the the limitations of of hvm so how how large what is the size of a contract system you can analyze what is the I mean yeah of course it depends on whether it's linear or not I guess but I don't know can you give some examples that's actually a good question um we do actually have um a bunch of interesting examples um that we have collected as part of um these kind of like coding challenges and uh tricky like Capture the Flag uh programs that that tend to be kind of tricky but small um that we can definitely work with and the underlying idea has been used on things like Unis swap so it's not like something completely unheard of although it wasn't HDM at the time that was used to verify parts of Unis swap but um in theory it's capable of verifying large systems such as Unis swap as far as I'm concerned I think it should be capable of doing that but it might need some help so you might need to simplify some parts of your of your of your program such that this actually terminates um but we are actually probably should do a bit more on on um applying to real world examples um yeah I think that's something that we probably should do a bit more of but it's definitely possible to do it and the underlying idea has been used in in very fine large systems but this particular implementation yeah it might struggle with something it might do way better than you expect I think if it's if it's logic of the system that you're trying to verify then it will do extremely well because the logic is just it's just branching left and right if you're trying to start verifying some complicated mathematics uh some incentive then you're you you there could be issues where where nonlinearity will just blow up the problem into something that will never get like never terminate but I think some of that can be escaped by saying well you know I'm really interested in the logic of the program and not so interested in the z05 or whatever multiplication that is in this in this in this line of code and you sort of simplify that a way and then you might then hbm hopefully should be able to uh to verify the correctness at least of the what's called normally in the banking space this would be called the business logic right the the way the system should be executing in terms of of the branching not in terms of the actual values that come out it I don't know if I answer the question but uh yes I think there's one in the back me so languages like property based testing is popular is it is it fair to say languages yoube yes that is that is that is very very fair to say yes correct indeed but this actually so property based testing is a form of fuzzing right so you have this kind of property and it fuzzes that for that property and if you can invalidate that property with one particle execution out of two power of a thousand it will likely not find it whereas this will actually find it either it doesn't terminate or it finds it so those are the two options so in that sense is stronger than the standard property based testing if I understand correctly So within that space this would be stronger but it's also weaker in the sense that it might not terminate whereas the you know the property is lesting what it does is that it substitutes concrete you know concrete values into into um into the into values that that you expect you ask it to substitute into and then executes the concrete semantics so it will always terminate it will just not find necessarily all the counter examples right yeah and and and that's and the stronger property is because you're you're using an Ser gu right exactly yes I mean inv validate the property using the S&P sare but the thing is that the property itself needs to be you know described in a in an expression which is which requires an interpretation of the semantics into a symbolic uh expression and then the symbolic expression needs to be somehow eventually described into this SMP which you mentioned so this this kind of these two steps are the key steps but I mean they also themselves break down into substeps for example simplification of the expression and filtering of the expression etc etc so there are some interesting like in between but that's correct yes