Formally Verified EVM Golf and Reverse Bug Bounties by Martin Lundfall, Lev Livnev (Devcon5)

[Applause] all right welcome everyone we're about to kick off we're going to be conducting today for your very eyes a competition in golf around the Gulf you might say that will also be form of the red pipe so we're rewriting smart contracts and I never like what you prefer and you'll submit submit your effects to our CI server which will run a suite of formal verification proofs against that white coat and if you do manage to pass perspex we have approval incorrect contracts then there's a competition for making the most gas efficient that's a contract and in particular we'll be doing it today with an ESD twenty cents this is the month where the most straightforward specification of course there's some caveats on what the specification actually looks like were made a little bit of an opinionated choice here we'll go over that at their time so when I said that we'll be doing a competition actually met we'll be doing two competitions at the same time namely there's this Ian golf competition that I just described hoo-wee correct coz 20 permutation but there is actually a second contest going on behind the scenes and if you're feeling like the first one might not be too much of a challenge for you were here thinking that formal education is just a sham then you can participate in the second competition which asks you to submit bytecode that has some sort of bug in it but it still passive suspects somehow if you believe that the specs and the methods that we have created with the formal verification process that has been set up then you can try to fool it and you can try to submit might go that fast those effects butter otherwise faulty in some way I mean this hard to define one there's no longer expect to talk about but I'm sure we'll be able to figure something out so you'll be able to compete in both of these competitions and we'll get to the details first I'm not going to be talking too much about the theory behind what we're doing today because we need to have time to actually do some hacking but let me just mention that the proving methods that were using here for this workshop we're gonna be using the catering work and we'll be writing our specs without looking at her specs written in the act smart contracts specification language we'll get it okay so let's get deeper into the specification I'll come over to God soon so sometimes people say that NERC 20 yearsI 20 specification as evidence or sort of Express panel it's really not it's more of an interface that really just tells you what the methods should look like in your contract and doesn't actually say anything about the behavior of course I mean we have some intuition around what this should be but there's actually a whole range of different types of behavior of difference here see 20 tokens and it gets kind of annoying when you start dealing with them and then you have to check whether this particular is a 20 you actually did return a boolean at the end of its transfer function anymore what's happening in the case where you're sending to the 0 is not like this so in order to actually have a specification we need to make a choice on all these decisions and neighbors have our choices but before I do that I'm going to show you the language in which we're presenting these choices so this is our specification formats that we have developed in order to be literate language that should be intuitively makes sense users you know common mathematical works and we have created it in such a way that from a small specification like we should be able to generate a suite of reachability claims so proof obligations essentially that you can port to right now okay but there are more back ends and we're planning and so let me show you how this works we have on the left hand side we have the specification in the active language and on the right hand side we have a simple transfer so what we do is well actually let me go back and just say the main claim of a specification is in this storage header so under the storage header we're saying how the balances of the people involved are being updated so we're saying that whatever their initial balances word from Bella to above they're going to be updated with a corresponding value as a [Music] as a result of calling the transfer function okay but this doesn't always happen because there are some scenarios where you do call the transfer function and your balances aren't updated namely if you don't have enough money to send or if there's an overflow when you're trying to add the value to of the receiver and so this should be reflected in the spec and here it is we see that they're actually four conditions associated with this out and the first three are associated with and if and only if Petter resists iff and that means that in the two specs that are going to be generated or the to reach ability claims are to proof obligations that are going to be generated from this act we are going to assume all of the conditions in the pit of the earth header to be true in the past case than to be false in the fail case so what the nature of that claim is is is that it amounts to saying that only if in the case where we are still within the range of a UN 256-bit word then these storage updates should be performed and when any of these conditions are not met then we should be in the field case in the fail case asserts that everything must reverse no storage updates are to be performed but there's another type of condition that we can make in an act and that's the if better then the indenter that the conditions in the if that are assumed in both the fail in the past cases so obviously this restricts the nature of your claim to make sense slightly weaker by assuming additional assumptions and so if you have and it better like this you must have a corresponding next suspect but assumes the negation of that so in this particular SPECT were saying that the caller ID should be different from from the two meaning of the sender should be different from the receiver because we had to treat this case somewhat differently I mean we actually that would only be referring to a single entry and the storage rather than two separate votes so we need to write that SPECT a little bit differently and so then during the course of this competition will be making we have a suite of these specs that will go over soon enough and they will generate these proof obligations your byte code will be associated with a proof obligation and the proof will be run on our CI machine and after they have been run if all of your specs are passing you follow that proof obligations have been proven and then there we will be taking the execution traces so the method by which we're proving things is through a symbolic execution and that gives you a complete exploration of the possible things that could happen through the execution of this method and through this execution trace we were able to walk down all the branches and the final result and guests the final gastrous also the final gas consumed by this method in each match and when we do this gas extraction we take the maximum values of the worst case scenario call this function and this is going to be your value that you're completely so we get a small expression like this if you know your idiom then you know that whenever you do this story to update what actually determines the cost of that has to do with whether the storage that you're obtaining was 0 or where they are putting it to 0 as so we'll see conditions on this board where they are the most general but of course you can take the worst case scenario this and this is what we'll be using ok so with that let me just say how this will all go down as I said all groups will be running on our service you don't actually needs to do much yourself of course if you just if you can come and chance we can talk about it but for the purposes of this competition the only thing that you need to do is to write an implementation get the bytecode of that implementation the runtime bytecode and make a PR to a repo that will be showing you soon and everything that is provably correct will be analyzed forecast okay so I think it's time to go over the specs they can be found at this repo which is the repo will be working with inside Catoctin two-column / backward slash yearsI 20 - golf and there's as i mentioned there were some opinionated choices we made while making a spec well the first one the most important monster listed on this page will not be caring about logs so you can forget about logs for your implementation for the purposes of this contest everything must revert if all value is greater than zero so this is following the convention of both my parents limiting and well this is this is actually true within for the minor caveat the stores will give you know the way that the EVM deals with a storage under the hood is a simple key value mapping of introduced to integers and so in order to translate the so the variables that are being used in near surprising like balances in total supply and allowances you need to place these at a particular location these these into transit your mapping in the UM and there's a convention for how you do this and the most crucial thing to know here is how do you make sure that you need to encode basically the balances on the now aids in a particular way and this is a particular hashing scheme that salinity uses in order to make sure that whatever you look up the palace of a particular address you won't have any collisions with any other address of the balance of memory so we we go over those details if you want to but you can actually also use the library Convention which is extremely similar a big hashes the arguments in the same way but only in a reverse order but if you're using solidity or vigor to write your contacts this will be of course done for you and supplying all opinionated choice if the allowance of a particular person with respect to some executors is the max possible event then transfer from should not decrease the allowance of spending okay and of all the submissions are due it's 125 let's go over the space hey sure yeah so I'll demo it down the specs for you and also have a CI server works and covering detail everything you need to know today [Music] [Music] can you see this is the size okay a little bit thick so first the first I want to show you the structure of this this repo has everyone been able to find it first of all so we're looking for looking for this repo and it hasn't and I'm gonna show you first just the structure of this so we've got going here a Romanian configuration finally you don't need to worry about and the most important stuff is in this source directory and here firstly we have our specs which is expected of me and this is the different aspects of Martin was right - this is red there's a part-time files it's got these aspects that will be tangled tangled out of it you do not need to edit this because this is the part that's that's this part this one is given to you for a but you do need to read these if you want to write limitations over actually that will actually passed it makes written understand all the nuances hopefully not too many nuances as there are some so partners really covered how these specs book but I'll make you just pick another one and quickly don't bring any other features but you know the idea is you want to you want to leave these and these interface lines correspond to the familiar DRC 20 interfaces and we use the we use the solidity where you know detering contract ABI for competing you know need to face selectors from the from the call data which is I guess you know assume but basically what that means is that if you're writing the theoretical total supply function that means that the force four bytes the call data activity the shot three of this string has to be something like this so just keep that in mind in case you're in case you're wondering how however a powder like this of course if you're ready and solidity of my for this visit done for you so I think hopefully these are these are pretty readable the best way to address any any difficulties would be when we get to the practical part if you raise your hand or just say something and we can discuss discuss with me these specimens unclear but I mean it you know I don't either these are pretty readable so you can see for example the convention with the return with the return values is here in this last night at the bottom means you return alive in this things success so now I want to show you actually how to run how to run this with your own 0 implementation so if you go back to this you go message source directory you'll see some other files and the most important one for you to edit is this file in runtime which contains the runtime byte code of your your submission we see there's already one in here which is which is the sample one has provided this is coming from a basic solidity implementation the source of which is it's in the it's in the rebuilding that they their injury so we go on below yeah it's okay so this is like the par that you can compare yourself against a beggar and it also assist you if you find some expert to rethink things have to read this way to you get a handle on what's going on yes so to be clear this this solidity that's in the in the root of this git repo passes the specs so your your your thing needs to be behavioral equivalent to this stuff this is one way to check and except for the constructor which we will not be verifying you don't need to you know you need to worry about how to have this contracts deployed to where a transitional process to play out right so going back to this what you need to do is put your put your bank code into into this pot so you can even doing this fund and up with your during fight card into it and I think you're actually Lancet because if you you know as you'll see in the repo to this pimping me there remain this repo here's how you do that with so steep say I'll see with all studies associate to Dante you'll tend to do up in stimul and have the effect good and these are the instructions before survivor and maybe you have your own funny tools that you want to try so it actually makes a lot of this header but it's not necessary so you know simply having me the hex in here as a ski is how house house I'll see you out there so now I will show you how this gets how does gets processed so it's kind of happened when you when you submit a poor west where you've ended this in runtime the file is our our CI server will automatically pick up the floor but and it's going to run the K framework groomer using the specs generated from the Riviera language against your guest or effective and then after that execution is done you know here's an example where this guy running when his execution is done a successful proof all of the all the specs eligibility things were successfully perfect you will it will actually do a as a symbolic analysis of the the gas with all of all these execution traces and a little calculate the product is run seventy the maximum caskets and then there would be a report produced so here once you wonder we can track your progress you can go to adapt on CI slash GRC 20 - golf they're here for every for every law request this repo there will be a hat which is your entry as you can see here they're the last one was in 1042 and if you know if you look on the right-hand side you'll see that there are 16 aspects in total and 16 of them were where accepted being that this is a correct implementation has been formed an air pipe and now if you click on this link well you'll be able to see an overview of coloring past but also very importantly you'll see next to every extra every passing behavior you'll see here on the on the right you'll see gas and gas analysis so I want to show you these so gas is a bit technical that this is the decay term the new extracted from the smoking execution that represents the state of the gas at the end of the end of every execution to this dysfunction the reason this has been complicated because there's going to be branching it here it's going to depend on the state state of the data but that's not a little bit hard to read the thing that the submission will look at other the contest will look at this gas analysis if you click that link you'll see that we have can you guys do this so basically what this is what this is showing is that this balance of that this balance of munch is actually consumed rather than 30 gasps and in every in every case this could actually a very simple example but now if we move on to something a little bit more complicated like its transfer function we look at the cast analysis for that it's a little bit more so the more complicated secure you see the first thing is the tree so that's actually the gas but all the cases conditional on the starting balance the ending balance and then we also compute the minimum and the maximum gas use the year you're here contest entering is going to be the maximum capacity and we will completely ignore what happens in cases where you are where were your executions supposed to revert so if someone is over over under flowing or they're not approved or something like that the old character man Cassidy's because given the internet and error and we're not going to try to save any gas so you can do whatever you want in those cases provided River so I think this probably gives you everything you need to to get started so we're encouraging as far as soon as possible because it will take you know people think about 15 to 20 minutes for these of these executions to run the CI and we can run a human parallel of course but to increase the chances of your submission I know the workshop please please submit it as soon as possible and don't worry about getting absolutely the best implementation view you can because I think simply getting something that's make some improvements over its validity learn any give you a good shot and the goal is to have fun learn something and of course you know we can continue playing for the next couple of weeks or months if you want to continue to you enough to get it down so just just things workflow completely clear what you need to do I mean is quickly make a submission to this thing to show you so Karen in the twenty golf repo and let's say I want to make a make an optimization to the banker and in particular I'm going to use a tool then use a tool it's very nice called STD which which stands for salinity and has diplom and what's really nice about this and actually comes with the unit systems and it's literally actually uses this to be implemented compiler optimizations detectives would compile into this just state-of-the-art way to to work with about to my plankton and my trip the syntax below that arcade so push if you have purchased error in the EVM what that does is zero on the stock that that cost you three guys but in this particular case mr. Berg we're in this non payable regime where he not supposed to set any value in otherwise it's gonna refer to comparison mention of the most describe the the call value is gonna be zero but they call value off coded only cost two yes we can actually every time we need Chris zero which would be quite a few times because that's quite a useful number we can actually replace every parent smoker serial code which I'm going to look up here in life though she she is is actually 34 in hex so if we do this to the incident inspector that should actually implement this this one pretty sophisticated compiler optimization so now you'll see that we've actually got to change my credit in some in some way and I can actually unlikely to commit this and and make pluralism [Music] so now you just go up here and now of course you'll make arrests when you're in for Kirk or whatever so one side once I click create fuller bunch here it's going to hopefully be picked up by the CI straightaway and then we can start verifying see how much gas we save from implementing this salinity enhanced diplomat optimization great it's already running and if I go if I go to this website which again is adapt up CI / GRC 20 - Gulf which is a nice dashboard for viewing these these builds you'll see that there's a new one there's a new one at the top you see step running sixteen so none of them have been accepted yet and take a little while form the verification is expensive and then you'll see these you'll see these gas analyses coming in as these isomers happen in the next you know two minutes probably the first one will come in and also coming in so you can see how are you doing and you know hopefully it'll take under an hour around 15 minutes to complete all of them and then this will be the first be the first admission I challenge you to see if you can you can beat this one using using any tools of your choice you know even if easy way places starting to apply some of these manual kinds of bike code optimizations you can also try running so I'll see with the optimized flag because the included mission was not compiled with that so that's already gave me some pretty good savings and then of course an Iranian Roy yeah or whatever whatever you like probably give you good time to start start working and please this is a workshop the idea is you're supposed to ask questions and we might help you understand spec language or or this is toiling so please please don't hesitate to uh to to engage with us and your neighbors are there any immediate questions yes yeah the dispatching all that is included none of the deployments is included so you know the length of my code doesn't matter but everything that happens from PC counter1 until they return is [Music] [Music] yeah so exactly like storage be anything but I mean the storage locations that you'll likely be working with are the ones that come from the mapping of balances and allowances so yeah started that there's one really important thing I missed which is to do with storage think thanks for bringing that up so I mean one of the ways that it generally to try off with my storage is by like packing packing things together to try to use that store justify regardless of whether that would be a good idea for any answer Pony token then that isn't really compatible with our with our approach here because what we're formally verifying who actually needs to specify exactly where the where the storage lives firstly and secondly the semantics of your your contract you change and you start to reduce the the size of the the integers that you're using because you really don't start to overflow in situations where otherwise wouldn't have so that that's not really going to work and in particular you actually need to look at one more file in this repo potentially depending on how long how crazy or your purchase which is the storage but if these business story specification and you're just using solidify furtive only need to do is follow the the border of the stores layout that that we gave is an example which is balances total supply and loans and so as long as the variables are good parent they'll be put in the right but formally what's actually going on if you're using more of a level approach then it's it's actually mapped out in this file so I mean I hope that probably if you're going to do something like this video already know how solidity places instance variables otherwise it's going to be a few things to it but you know for simple for simple variables that are not things like like the total supply they're just going into the swap number and the corresponds to the starting from zero the order that the variable is declared so total supply of example it visits top one so you know if you want to if you want to store the total supply you just do s store one into the supply well-well-well mappings like balances and then to deep mappings like like allowances are a bit more complicated they're computed using hashes and invective and conventions as Martin said there's a living Piper and they hash things in the opposite order and by default this files can be configured to use the solidity order so there's always my sense of solidity here if I wanted to use my for instead what I would do is I would um you need to actually replace this with with VIPRE and then we're gonna hash things in the opposite order no you know for the details of how to how it's actually hacked I think the best thing would be that if you're interested in experimenting with this is the you raise your hand one of us will come come and show you to make sure that it's correct just because maybe even most people aren't interested in that it's not worth it spending five minutes explaining it right now allowances like yeah I think these were their over source destination so donor and spender is also correct okay so then let's get started if you have a question please please please raise your hand or justice [Music] [Music] effective of contractors later [Music] just just one interesting fun interesting piece of information so this one that I tried with with with instead to replace six zero zero zero with with 34 and actually uh yeah I can actually corrupted something and the formal verification just came back negative very bad very bad results don't try this one you will be wasting wasting a time so honest as I don't think it's a success for a performer patient may be a bad day for no one actually just just one well the way we set it up is the first failure causes at all that all the stops are don't waste time so take the transfer front function they have nothing actually very quickly again if that's your kind because a cup of tea you know another thing in to investigate would be to figure out why it's optimization is on stage maybe how to make it stay [Music] [Music] [Music] [Music] [Music] we I only took this small break to get this supposed to take much I can ask for someone to cover I should jokes la-di-da I could search for my username Archer [Music] the party okay [Music] [Applause] [Music] [Music] like knowing that I said I forget [Music] [Music] [Music] [Music] [Music] mr. practice currently death [Music] Jesus [Music] [Music] [Music] [Music] my segment I know [Music] any questions or yes [Music] Eliott never easy our neighbors now the most unstable [Music] [Music] sir ooh [Music] [Music] [Music] you jump robust and stay out so I just read one time yes it is president [Music] [Music] [Music] [Music] yeah we're gonna do submissions which is sliding around with the optimizers flag which comes in Clarkson and exactly the same amount of gas is going without [Music] I mean the very last night [Music] [Music] [Music] yes argit at birth [Applause]