Formal Verification with the Certora Prover

Transcript

hi I'm Mike George I'm director of product at sartora today I want to tell you a little about the sertora approver afterwards during the demo session we'll be set up over in the front there so you can come ask us questions so what is the Satora approver well it's a tool for finding bugs in smart contracts the way it works is developers specify the intended behavior of their contracts in our domain specific language which we call CVL you can think of specs a little bit like unit test but they're much more powerful in fact I normally wouldn't say infinitely more powerful because it sounds like hyperbole but in this case you would need an infinite number of unit tests to replace a single rule so it's it's Justified and the prover will then take these specifications and the

contract implementations and check that the contracts obey the properties and the nice thing is it checks that they obey the properties in all possible cases so the approval will consider every possible configuration of your storage variables and every possible inputs to the method calls um and this sounds like magic and it kind of is and it builds on Decades of research and formal verification um both from Academy and Industry um so I want to um take a second to tell you how um our formal verification approach is different from fuzzing so it's similar in the in the sense that both take a code and a specification and give you um you know try and find bugs with fuzzing you generate an example you

run the example and if you're lucky it fails and then you've found a bug or a violation if you're unlucky it passes and then you go and generate another example and run that example and so on and eventually you've run lots and lots of tests you get some confidence that you couldn't find a violation and that you know can take a couple of days with the sertora approver we do similar input right you take a code and a specification but instead of running the code we translate it to a logical formula and this logical formula is satisfiable if it's possible to violate the assertion and then we hand this off to a third-party smt solver and there are many of them we actually use several and it can give us one of three answers

it can give us what's called a model which says here are values of variables that will cause this assertion to fail and then we can turn that into a concrete example of a transaction you can do that will violate the properties but it can also give us a proof which then says it is impossible to violate this assertion no matter what value you give in and of course this is an impossible problem to solve in general so we can still time out but our timeouts typically take two hours and then they tell you okay you need to go back and think about we have techniques for simplification that can that can help um let me tell you a little about about our domain-specific language so it's like solidity your your specifications look like straight line code you you know Define some variables call some contract methods you can Define

functions and so on use required to specify the preconditions assert to describe the correct Behavior but it has a lot of other features that are very useful that go beyond what solidity can do so you can reason about arbitrary values I already mentioned this if you just declare a variable and don't Define it the approval will try every possible value and I already mentioned that we try every possible value of storage variables as well we have Syntax for calling an arbitrary method so you can say something like if any method increases an allowance or something then something must be true we have the ability to access the internal state of contracts and to hook on changes to the storage State we have explicit uh concrete concise Syntax for writing and variance

um we can reason about reverting paths so that we can write specifications like this method will never revert unless the following conditions are true and we can even rewind storage to a previous state so we can consider uh different hypothetical situations right so if I run this transaction but then I roll it back and instead run a you know add a permission and then run it again I should get the same answer things like that um I probably don't have time to go through this but let me just quickly show you um what a rule looks like here so this would be a specification for like a erc20 transfer method for example and so this rule looks kind of like straight line code we declare a sender recipient amount we don't actually say what that

sender recipient amount recipient and amount are um uh the as I said already the approval will consider every possible value of those we can then add a requirement that says that the you know message sender for the transfer call um is um is the sender we declared we can record the balances before and after just like you uh would in solidity we have a special math in type here that is a non-overflowing integer but other than that it just looks like a straight line code we call transfer pass in explicitly the environment with the message sender and the block time stamp and so forth and then we write some assertions we assert that afterwards the balance went down by the given amount and sorry the

balance of the sender went down the balance of the recipient went up so this is the an entire specification we can run it through the prover and the approver will say oh actually this is violated and it will give us a concrete example is this off the screen for you guys it is um that's maybe too small but the concrete example here says that the sender and the recipient are the same are the same address and of course if you transfer from one address to itself the balance isn't going to change so we can then um um add a precondition uh add a precondition and once we add that precondition the rule will pass

verification is only as good as the specification we're developing tools to check the specification I'm out of time so come ask us about that later and thank you [Applause]