Move Fast and Break Nothing Michael George

hi my name is mike george i'm the head of product at certora and uh today i want to talk to you about our technology for verifying um smart contracts um and uh and hardening them um so what we do at zortoro we have a tool called the stator approver and it um checks your program against the specification and tells you whether your smart contract does what it's expected to or not so our tool takes in your evm byte code as well as a specification that's written in our custom specification language and the specification says here's here are properties the contract should have you know the contract should be solvent for example or the you know certain method should not revert and our approver takes in these two things the smart contract the evm byte code and the specification and it outputs one of two things if you've done a good job on your contract it'll output a yes saying yes under all circumstances your contract does satisfy the property that you've set and if it turns out that actually you have a bug in your code the approver will output a no and not only will it tell you no your program does not meet its specification but it will also give you a specific example here is a state that your contract can be in uh here is a method that you can call on your contract here are arguments for this method and if you call these arguments if you call this method with these arguments in this state then this will violate your property okay so i want to explain i want to show you a little bit how how you would use the prover and to do that i want to walk you through a bug that sertora found in sushi's trident protocol and this was a bug that actually would allow you to completely drain a liquidity pool so it's quite an important bug and i want to show you how we think about verifying contracts so let me first tell you about the contract example so it's a constant product pool which is a liquidity pool it holds two types of token i've called them token a and token b here in reserve and it allows you to swap one kind of token for the other okay so let's say buffyguay comes along here and says i want to buy 10 b tokens we have to figure out what the price of those b tokens is in a tokens because they're swapping so if they want 10b tokens they need some a tokens and the way we figure out that price that's where the constant product of the constant product pool comes in so after this transaction there will be 10 b tokens in reserve because 10 of them went to buffing way and to keep the product constant that means there needs to be 10 uh a tokens afterwards as well and that means that uh buffingway needs to spend five a tokens to bring the number of a tokens up to ten okay so that's how the constant product pool works this has the effect of making uh rarer things more valuable okay and of course i want to show you one other thing you can do with a constant product pool which is maybe buffy way doesn't want to trade maybe they want to actually invest in the pool and the reason they would want to do that is they get some liquidity tokens right and so uh in the pool originally other investors held 10 of these liquidity tokens um when buffyweight invests they're going to get two liquidity tokens and afterwards the reason i show this is this the product here isn't actually constant right if you invest both sides of the equation go up and so the product is going to go up but also the number of lp tokens in the pool goes up and um i just want to point out to make the math work out the number of lp tokens squared should be the same as the product so before it was 10 uh times 10 is 100 after it was 12 times 12 144 okay all right now in my former life i was a teacher and so i can't resist putting a quiz in the middle of my talk so if i ask you to describe a key property of constant product pools what a lot of my students would say is the product is constant and that's a good a good answer and of course we know the product of the reserves is constant depending on the size of the pool all right so if we think now about a spurt contract that's trying to implement this constant product pool we might have an interface it might have different ways to get the amounts of reserves the total supply of lp tokens different ways to swap buying a or buying b you can mint and burn that would be adding or removing liquidity from the pool and the thing that we care about again is the product of the reserves is constant and with this interface we can actually write down an expression for that the reserve a times reserve b is going to be equal to the total supply times the total supply that's what i told you on the previous slide so now i want to think about how would we actually check if we have a smart contract how would we check that it has this property this is like the defining property of a constant product pool so one thing we might do and one way that a lot of smart contract developers find bugs is they think really hard or they hire auditors who are very good at looking at solidity code or byte code and finding finding mistakes in it right and in this particular case i've shown you a little bit of the uh of the trident pool code that in fact the bug is somewhere in this method uh i'm not going to ask you to even try and read it you won't find the but maybe you will if you're really good you probably won't find the bug right away um but the point is this is just a piece of the code there's about 550 lines of solidity code that contains this particular bug auditing is a manual process you never know if you're done if you've missed something and so that's that's difficult it's important it's useful and actually i should mention the bug i'm talking about was found independently by an auditor so it's not impossible um but it's difficult so another thing that developers often do and is a really important tool is testing so what you might do again if this invariant this key invariant is what you want to check you might write some test code right and at the end you're going to you're going to do some things right you're going to set up your pool you're going to call some method on your contract and then at the end you're going to check exactly the property you want to check right so reserve a times reserve b is the total supply squared right but the question here is if i want to write a good test suite what am i going to put here right so i've written good comments right i'm going to set up a pool i'm going to call a method but what method am i going to call well i probably want to call all the methods that do you know various things swap and burn and mint and so forth but even then i'm going to have to call them with arguments how much am i going to have to swap how much am i going to have to burn i can get to the point where i have 100 coverage but maybe there's a bug that's caused by some overflow or something like that so even if i have 100 test coverage i may miss a bug just using testing and more than that it's not just the method you're calling or the arguments you're passing the actual state of the contract before you um before you actually execute the method that matters a lot too maybe the bug only shows up if the if the pool is currently empty or maybe only shows up if the pool is right above its you know minimum lp supply or you know who knows right so once you start thinking about okay let me list out all of these scenarios i care about and then start writing your testing you're going to have a lot of testing and again it's manual uh it becomes a more automated but still manual process right and to figure out good cases you're actually back to looking at your 550 lines of code to figure out what are the different paths you care about so let me tell you how we would do this with the sertor approver so as i told you the satoru approver takes in the specification what should your contract do as well as your contract and it checks to see what it does so with the sertor approver the way we would check this invariant is we would write the following specification invariant constant product that's a name i came up with the product of the reserves is the total supply squared and that's it that's the specification now it actually turns out we did some of this verification we ran the tool there are some cases with some round off error where this is actually not quite true it's true like within epsilon but we can also have a simpler invariant that should definitely always be true so this invariant this modified invariant just says if either of these is zero uh then the total supply has to be zero so if the reserve a is zero total supply has to be zero reserve b is zero total supply has to be zero right so it's just saying the left hand side is zero means the right hand side has to be zero okay so we can write down uh invariants like this in our specification language and then the approver will check does the contract obey the invariant and it checks it no matter what so it tries every possible method and every possible code path in every method with every possible argument which sounds impossible and it's a little bit magical what actually it does is convert the contract and the specification into a logical formula and then use sat solver to uh to actually show that that formula is does hold but effectively the approver checks that you your contract debates the invariant no matter what and if it doesn't it will provide a counter example it will say here's a state of the contract here's a method you can call here's an argument to the method and if you you know if you execute that then after that method call this invariant will break okay so um i'll even i'll show you a little demo here so let's say i uh go to demo.sertor.com here um so you can actually see here we have a whole bunch of examples where you can see some solidity code you can see specification you can put in your own solidity code if it's small enough it'll it'll just work in the demo site so i'll go to interesting bugs here go to the constant product broken so here we have this is actually a simplified version of the contract because there's some setup we had to do to get to get the the actual contract to work with our tool but this is for demo purposes uh contains the same bug and here this is probably a little small for you to see but that invariant that i showed you is right here that second and very integrity of supply there's a little bit of setup we have to do as well so for example we don't want the prover to give us an example where uh you know you start from this impossible state and then you do this operation we don't care about that so there's a little bit of additional setup but the first order of approximation the invariant looks just like the invariant i showed you on the previous slide and so you can click start verification it takes a couple minutes i mean it's checking a nearly infinite number of oh it doesn't because it's cached but it does take a while but let me just show you the results in my slide so what you would get as output from the approver is all of the methods of the contract are checked and we find that most most of them do actually preserve this invariant but there's this one method called burn single that actually violates the invariant and not only do we know that this burn single method violates the invariant but we get sorry trying to scroll on my screenshot didn't work we also get a call trace and we can see here actually that the burn single function gets called and by drilling down we can see the different arguments we can see the state of the storage of the contract and we can find out exactly what happened and then using that of course then it takes some expertise to say what's the actual bug in the code but knowing there is a bug and you can exploit the bug with this following test case is a really helpful thing to be able to do so that's what i want to show you the sartor approver can check a lot of different things so i showed you an invariant you can also check things you can write down method specifications if you're writing a smart contract you probably put some comments that say you know this method you know transfers 10 x tokens to whatever you can actually write a rule that checks that the method does what you say you can check properties like solvency if you know if i might have to pay out you know x tokens i can guarantee that i actually have x tokens uh allocated to this contract you can check things like permissions that you users can only change their own balances and not the balances of other users or even things like front running you can check properties like if i take this transaction and insert another transaction just before it in the same block the price that i get will be unaffected you can write rules like that and many other things it's a it's a very flexible language so i encourage you to take a look at our demo site demo.sartoria.com or drop us an email and that's that's what i wanted to tell you thank you