# Certora: Keeping your code secure forever: Move Fast and Break Nothing by Mooly Sagiv

- Speakers: [Mooly Sagiv](https://streameth.org/speakers/mooly-sagiv)
- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 27:01
- Topics: blockchain, smart contracts, distributed ledger, ethereum, ethereum solidity, solidity, solidity summit, language design
- Watch: https://streameth.org/watch/yt-5XIWAB4NElU
- YouTube: https://www.youtube.com/watch?v=5XIWAB4NElU

## Description

We will describe a platform for formally verifying smart contract correctness that can be integrated in CI/CD. Smart contracts and their invariants are converted into SMT formulas and the SMT solvers automatically identify vulnerabilities or generate mathematical proofs of correctness. We describe our experience applying this technology in the development phase and present bugs found and smart contracts verified.  Our hope is that this SaaS technology can speed up the development process. The secret sauce for integrating in the CI/CD is that the invariants are reusable across different versions of the code, and targeting the low level EVM bytecode. This raises various technical challenges both at the conceptual level of the specification and at the technical level.

## Transcript

thank you very much fancy and thank you akush for the first talk actually made my life much easier so i want to also make your life easier for the people in the room we actually uh have also a formal verifier and actually you can try it as we speak now it's a it's actually implemented and hosted in amazon so what you can do at the moment if you are not our customer we don't let you change your code but you you can change your spec and you are you are i encourage you to actually try that it's actually a beautiful demo which was put by anastasia enrique from our team and actually this actually shows you that you can actually it says actually failed to access my camera but you can you can see me right fancy yes we can see you fine and here you find and see the slides all good wonderful so what we are very happy in this space and we we hope this will continue we are finding terrible bugs in this space and terrible bugs in smart contract and actually i'll give you a little bit hint of how we are doing it so uh wait a second this doesn't move now so who are we so we are we are actually a team which is located in in seattle and in berlin in tel aviv uh shelly grossman uh james wilcox john thomann novit door and alexander nuts was actually here in berlin leo oppenheim was a secure security expert or pistoner and anastasia fedotto and thomas bravandi and what we are trying to do we are trying to formally prove like the previous talks that the code specify a satisfied specification but as i said we are equally interested to actually find bugs and actually that's the biggest value of our technology as part of the ci cd it's actually find box and just to mention we had the previous talk interactive therapy these are very powerful tools they are agnostic to the programming language they have even completeness and the previous talk we had also by by christian and we hear tomorrow about smt check here this work at the solidity level also the sulci verifier and the very solved by microsoft so what's interesting about our tool it operates directly in the evm code we think that this is very good and in fact this i'll show you and the second thing that we do in satori and i'll talk about it in the second part of the talk that we are actually implementing clever static analysis that actually can recover interesting information about the evm code and this actually improved the utility of the smt so we see these as two complementary technologies that work well together so what do we build we built this product that we call continuous code verification it's very similar and you see it in the demo it's very similar to what anku shows in one way in the sense that you give the customer a code but we actually write in a different file we write the specification we write a property that says what are the invariant what are the rules that must be obeyed and then we feed it to the essay to the to the tool which is hosted on the web it actually either can give you a format proof or it can actually give you a test case and that's actually a very valuable a test case that you show you input that violate the specification so the interesting thing about that that we think that specifications are hard but once you write the specification once when you move when you upgrade your contract or you move to another version of the contract we can check that your code satisfies the specification and we have already done it with few customers which integrate our tool into the ci cd so there are unique aspects of that so one of the things that we say that we decouple the specification from the from the code so we don't write these loop environment in the code we write them outside the code and we write them in high level in the sense that we want to make sure that we guarantee certain properties that outside users care about like for example inverted operation the bound that's applied it will show you later maybe you want your transfer to be additive in the sense that if i if i s transfers to d and and it turns it first it transfers x and then it transfers y then if it transfers x plus y it should be the same and interestingly we can check this property and either prove them or even more interesting find bugs and the other aspect that is unique about our approach is that we tackle the low level evm program so this has some pleasant benefits so basically we want to make sure that you don't need to change the spec when you change your code and in fact in some cases we show that we can use the same spec for different project and and another thing which is interesting because we operate on the low level card we can catch more errors so this means that we can actually catch arrows that are not actually caught on the source code and we verify the actual program which is being executed so for example if the solidity compiler generate a loop if the generated compiler generate and it in fact it does if the consolidated compiler generate tricky memory operations we can actually check them so we see ourselves as a checker that can be executed outside the comp up after the compiler so i'll give you a very very simple example and this is example which is in the demo but there are other examples which are more tricky so this is a very very simple property that any erc token should be uh uh should should satisfy and this is actually given by shamiq islam which is the head of security at coinbase so when they list tokens they want to make sure that nobody should be able to mean unbounded number of tokens so formally it's some kind of an environment that says that the mean the number of minted tokens is less than the predefined amount so let's see of a very nice team which is the maker dao and this is a team which implement an inverse auction so what is an inverse auction you start by some kind of a beat which is high and then you have different different guys alice bead and bobby and since bulk beat was very the smallest one then at the auction at time after the closing time uh basically the the number of bits basically bob will get the bid and the total number will increase by bob speed and this is a very nice behavior but what happened we ran out the tool and we ran actually the test version of the of the make of the maker we just ran it through this abandoned minting supply and basically what it happens it found out that if you have mallory and mallory beats very very close to the max so and in this uh and and and and nobody else beat it so so after the build expiry time at the close operation basically the total supply is increased by milo repeats and this is actually something that you can execute now with our code we can check it you can write this back and check it and in fact it's one of the examples on the demo so this is exactly what will happen in the demo it will run on h function and you see it actually it operates on the evm codes you see some some some data about the evm and what it tells you it tells you that all the functions satisfy this rule but the clause can violate it and it gives you the test case in fact it gives you the test case that actually show you that it has this violation and once you fix the code it will actually show you that that it's actually correct so how does it work well how does the satoru approval architecture work so what happened is that we have the first part is something which is very unique in this space we have a decompiler we have something that takes the smart evm card and perform clever analysis and actually it would perform more this is actually what john has implemented in in the seattle office etc we are actually getting this high-level intermediate representation think of something like yule and maybe more that you can actually extract automatically from the evm code this will fit to what we call verification condition generator so verification condition is not like the vc that you think it's what's called the vc informal method which is basically a method that converts into a formula like within aqua stock and this takes the rules which are from outside and it takes the intermediate representation and from both of them it generates these constraints it just generates this verification condition and we fit them to existing constraint solver we are not we're operating directly on the smt level so we can feed it to different constraints over the whole public domain and great and and complementary and these constraints holder either can give you a test case which actually show you the actual violation or it can actually give you a formal proof of the rules that hold on on all inputs so this is a very very simplistic example i'm only showing you that kind of a pseudocode you see this transfer function and you see some rules that says that the balance before is equal to the balance after and you see that they are this constraint for each each statement in the code we generate a mathematical constraint which emulates the semantic of that and we also take the invariant of the rule and which we generate it into a into a an equation that says that you want the sat solver you want the smt the model con to find a solution to these set of constraints and each of the solution to this set of constraints it's represented back okay so basically you feed it to a constraint solver and the constraint solver actually gave you a simple but interesting bug that if you're transferring from from an alice to itself then in fact this environment can be broken so it gives you some kind of an edge case and once you fix it it can give you a proof so i want to talk to you about the evm which is the interesting part of this talk which is sort of what we do technically so i took a very very simple example it's the bank example which is also available in the demo and it's a very very simple think about it like erc or maybe even simpler than erc there are functions like deposit transfer and user and remember you see in aqueous talk that basically he is handling the solidity but we are not taking the solids we are taking the evm and this has some very interesting consequences so what's going on in the evm so the evm you basically have a flat memory so basically all the local variables and fields are all actually heated and the operations are low level operations so even if you select a field it becomes a bitwise operation that we know as smt solver that's very very difficult so you make the task of the solver very difficult and even whereas the the the control flow and the procedure and the procedure are really hidden and even the arguments are hidden so this makes the life of the verification or even somebody was investing investigating this code manually very very difficult this is just to show you what happened is actually it's an output of our tool so this is one of the stages of this decompiler and you i'm sure you don't understand what's going on here right so basically what happened is that these are nodes that represent the evm instruction you can't read it and so do i but each of these it represents some kind of execution of the evm and there is an error if one instruction can be followed by another instruction so you see that these are and one thing that you can see here which is kind of weird that in the evm it's all kind of of spaghetti which actually the even the procedure structure is lost so for example here is this deposit if you believe me and i will not be able to prove but this is the deposit part so this is a part of the evm which is a deposit here is the result so they are very very tricky so reading this code or running static analysis or formal verification of this is very very tricky and even if you take this small function this transfer which is part of the bank and you even look at that at the solidity level it's very very clear but look at this instruction so basically the access to funds funds message center as part of the required this looks very very simple in solidity but guess this is how it's generated in the evm they are in fact 21 instruction you should ask christian later but there are 21 instructions here and this 21 instruction they manipulate the memory and the stack in in a tricky way so what actually is going on this font's message center is actually mapped as a as a hashing function which is actually you can cut the message sender and the slot of the fund and this is executed by means of increasing and decreasing the stack so you see the first instruction it puts zero in the stack the second instruction duplicate now we put message send there now you you do you you put this uh value cleaning you put another zero you put the value cleaning again you put this duplicate you put this uh a 20 here so now it's 32 you put this ad you put the swap you do this store level and and now there's this 32 you add this the 32 to get 764. you put this zero i'm sure you lost me by now there is this hashing thing now there's zero there's drop there's less load eventually trust me or trust christian it actually gives you the right solution but if you want to read it to run formal verification here it's very very tricky there are a lot of things here which makes smt even harder than it usually is and smt is a very very hard problem so this makes the life of people hard and this is actually where static adapters would be used okay so what do we do so besides using smt techniques which are wonderful we're also using other wonderful techniques and developing our own which are called abstract interpretation so there is a well understood theory that says how do you automatically find environment about your program and we do that at the low level program but you can actually execute these kind of things as a high level program and these they prove some kind of absence silent overflow for example we can actually implement something similar to safe mass but not dynamic we can actually automatically find something that was similar to aqua stock without even calling the smt and give you this gives you some kind of a sound and potentially incomplete reasoning but it's not so bad for us we can because we can actually run the smt and from a computational uh point of view it's actually sidestep the problem of undecidability so what's going on under the hood of this tool it actually does this sidestepping of undecidability improves properties of your program by doing this abstract interpretation so what's going on you take the state you take the set of state and you over approximate the next state and then you over approximate the next state and so on and so forth until you reach what we call a fixed point a point where the analysis stop changing and at that point if we actually separate the good state from the bad state we will automatically be able to find invariant about your program and this happens if your program explores some kind of locality property and if they don't then in fact this will give you a false alarm but so for us it's not so bad because we have the smt checker that we can run in order to check whether these are right or wrong so what we do in this space we are developing this framework that you can think about it like evm like llvm or suit so these are things that develop academic research project university of urbana champaign and also in mcgill university suit is for java llvm is for c so we are trying to do something similar for evm and we are exploring the properties which are unique in this space and i'll be happy to to say more or you can contact john so we are doing memory analysis we are doing unused allocation bound checking we are doing all kinds of analysis and actually it's it's we are an intermediate step and we are doing more and more one thing which is interesting that during this process we are finding actually bugs in the solidity compiler we just found one and also that we can actually reconstruct a lot of the high level information from the evm and this could be useful by itself so for example here i didn't show you all the code but you see that actually these are the 21 instruction and you see that the static analysis actually was able to eliminate the stack so you see there's no more memory here and in fact you see that we are able to recover almost the information of the source and this is useful whether you are doing static analysis or not so basically this makes the analysis simpler i can show you many many examples that smt timeout and it this will terminate in a few seconds and what it does conceptually it separates the low level operations which are executed in a byte code from the high level operation that we are proving and it will allow us to prove stronger in variant and actually it makes it more the bugs that we are producing are more understandable so the compiler of course has many usages beside formal verification this is known of course in the community program understanding slicing auditing for upgradable contract we can check interesting properties and other things um so that's one thing so i'm almost close to my to the end of my talk and i want to somehow say something about more high level and leave a level for other discussion so we are this space i've been uh working on this space for 30 years now so there are actually many interesting technique in this space and somehow i like to think about them as how expressive they are and how automatic they are and this is the very of course i should say this is a bit subjective but there have been academic articles trying to compare them so we heard this morning about tools like k or or tla plus they are proof assistant they are very good but they they require lubricant effort i'm just pointing out an academic effort what we did something for academically in the context of iv where we try to compare how much effort are in these interactive to improve and it's a very very big effort and it's even worse in the sense that once you change your code a little bit you have to redo it on the other hand there are a lot of beautiful techniques that develop by many people including myself uh standing canals and they are very automatic but they are limited and what sato is trying to do satori is actually trying to be in the middle somehow we hope and of course this is something that has to be judged but we hope to be maybe not as automatic as interactive but is automatic enough to to enable you to show everything that you want and even more importantly when you change the code find the box and also we wanted to be uh uh uh automatic uh powerful so we want to actually achieve both of them i wanna maybe just sort of to for you for curiosity verdi is a very nice project by james wilcox who is our city always in seattle and basically he proved properties of consensus in and it every lines of cod every line of the of the consensus protocol he had to write 10 lines of so that's very tricky iron fleet is a project which actually used daphne or or boogie and in fact it's actually also difficult and what we are trying to do we are trying to make it very very small and i think we have numbers that show that we actually have very very small lines of at least academically for these protocols and in satoru we are trying to be even more automatic and sometimes we sacrifice precision but other things but and also we are leveraging a lot of interesting properties about this domain so we are doing something which is very very specific for smart contracts so this is my last slide uh i want to make some we want to make formal verification standard for software development and the interesting thing is that we think that this domain and i i'm of course academic but now i'm taking a leave because i'm thinking that this is a very interesting domain for this uh our technology and in particular we're interested to explore the connection between proof automation and automatic bug finding we think that actually there are actually two side of the same coin so we don't want to separately look for proof and and for bugs we want to actually connect them together and the other thing that we are trying to do i haven't been able to show you but you can see our our our specified language we have quantifiers we have hyper properties we are doing a lot of things that make actually verification at the high level are good and we love to collaborate with the general foundation anybody else and it's the third thing is that we operate in the evm level thank you very much thank you thank you for your talk awesome all right we have a couple of minutes left again for questions um first the questions in the room then the questions in the chat um leo you want to say something yeah uh thanks molly for the talk i think it's a very nice and special challenge to talk about in high level and variants on the evm level um and related to that i took a very brief look um at the display at the spec language i just mentioned and i was wondering how do you deal or how do you specify or what how do you manage loop invariants in the context of uh in the evm context beautiful question so that's actually something we ask you it's very difficult for us at the moment we have a mechanism for that i think we discuss with you we have a mechanism for that what we are doing and which they are hoping in certain cases we can infer them automatically but if not we have to say something which is specific to the code for us usually what happens usually for example if you have a procedure you have play and post condition then it's make it easier because we can specify that at the procedure boundary but you're absolutely right there are certain cases that actually the the source level is is something that is better but remember where we want to be we want to be for people who change their card and the problem with looping variant is not just a one-time fee you change your card and every as you know every little change of your card you change your environment so we so we so it's true actually we are at the moment we want to infer so if you write for example in our specified language you see there is this notion of said invariant but what does environment it's a global environment so basically what it does it checks that before and every every procedure which it checks them at the procedural boundary but if you want to do them at the loop boundary you actually have to either infer them or do some other thing our tool by the way also also has the possibility of doing bound and model checking so you can actually say uh explore a fixed bound of the loop another thing and we also another thing that we are doing with the static analysis we're unfair actually interesting looping variant and i love to elaborate about it so we can infer quantified environment we can infer many things which are very hard for smt because this is actually my research as you probably know yeah thanks yeah we talked about it some time ago and yeah i was just wondering um yeah how it looks right now because it is a very hard problem and yeah i i personally haven't gotten very far and that's something we're trying to figure how to specify for for act for example on a lower level yeah yeah so we should definitely talk about that we actually have coming uh code will probably contribute open source that does an interesting thing that needs this loop environment so i would love to talk to you and of course i will attend your session tomorrow to to understand where what what you are heading to cool thanks okay we have one more question in the room from app um we can't hear you in case you're trying to speak sorry can you hear me now yes now we can hear you perfectly okay perfect uh so my question is regarding the fixed point analysis uh basically uh the uh smart contracts even the simple one have uh concrete domain of them is invisible to this uh to find a fixed point uh so what are you using it for as your abstract domain when you're looking for fixed yes yes so this is actually a question to john but he's sleeping so i'll try to do a good job so he's is adding more and more things as we speak i think the interesting thing uh so you're from this domain i just don't know how technical to get back to you it's uh one thing that pointer analysis in this domain so we talked about it that there are things that lvm and others but this isn't we everybody said a lot of bad things about solidity and evm but we can say a lot of good things it's much easier for for static analysis than many of this domain in particular memory allocation actually there are no the allocation so basically we have points to analyze but it's very simple and we love to to to say what we are doing we have interval analysis we are adding and we're adding more as we speak then i think about it we're working with customers and we see the customer code and see what is needed for this code and we have the smt always as a backup so basically you run the smt if the smt does a good job we don't have to do anything but in in many cases when the smt fails then we actually have to to develop more clever abstract domains and we are thinking of adding more abstract domains to that we have basically that kind of a framework that we add more and more abstract domains