Security Summit 🦺 Formal Verification with DeFi

[Music] I'm Samir from Satora and today I want to talk about formal verification and its application in defi along with what we do at Satora to allow you to verify your smart formally verify your smart contracts so formal verification is an old computer science approach where you have a program and you have your specification and you're basically checking your program against your specification making sure that it is following the properties that you have laid out before and uh you know these tools they either give you like a bug a counter example showing you exactly how your protocol violates those properties or it gives you basically an effective proof of how your protocol is like successful on all the properties that you have laid out before so the first question that we can ask is like why do we need for formal verification in this domain of defi in particular and uh here I've listed like a couple of bugs from 2022 2023 Oiler Finance urine finance and as you can see all of these hacks have led to millions of dollars in losses so one thing that is very interesting about this domain of defi is that the bugs have a very high impact you can have millions of dollars in losses and uh you know these funds are usually very hard to recover so here safety critical code becomes very important like even small bugs are uh can lead to some huge vulnerabilities and you know can drain the protocols out of their funds so code is code safety is very critical and as you have seen billions of dollars are at stake so you need something more than just testing fuzzing and auditing safety guarantees and this is where formal verification can shine it can give you these strong security guarantees that you need to you know make these billion doll protocols robust uh another interesting thing to note is that traditionally formal verification has been very uh hard to scale because the code bases traditionally have been massive with a lot of uh lot of files and data structures so but this is not the case with defi here the smart contracts are very modular and they're isolated in the sense that uh you know they're they're they're captivated they're just captivating one idea so it's very it's easier to deploy a formal verification uh in the domain of D5 and it's easier to like make use of it uh in this domain but uh interesting thing to note is that even though the code is small and modular bugs are still very hard to find in D5 with just testing fuzzing and auditing approaches and that is primarily because like the bugs that actually lead to millions of dollars in hacks occur in rare scenarios the they are very strategic bugs they only occur like tricky edge cases uh and this is another place where actually formal verification can Shine the most as compared to testing fuzzing and auditing alone because formal verification allows you to explore this whole landscape of possibilities and helps you find the bugs in those rare scenarios that cannot be looked by with just the help of like testing or fuzzing uh and as we all know even though like the code on the blockchain is immutable the code is constantly updated because uh you know teams are adding Buck fixes and new improvements so it becomes imperative to make sure that all of these new changes are constantly getting uh uh secure for your with your properties like we need those strong security guarantees for every major update or every even minor update as well uh in this example of Oiler Finance which is an interesting example where they had verified they had formally verified their original code base securing it safely however it was like a small change in a new PR that actually led to a bug uh which led to $200 million in loss and unfortunately this new PR was not formally verified and kind of like uh tells tells you about the importance of formal doing formal verification regularly and repeatedly in uh regular development cycle so hopefully now that I've convinced you like why formal verification is essential in this domain of defi uh let's talk about like what other tools are available in the market that can help you get some more security guarantees so first and foremost comes testing and fuzzing approaches where you have Rand random testing on many inputs and some of the examples of these kind of tools are like akinna and Forge so they're very easy to use they find a lot of bugs but they they are the hard to find logical coin cases are not possible using testing and fing approaches like uh you know protocols that are dependent that have many dependencies or they call one another testing and fuzzing approaches are limited in their security guarantees when it comes to such protocols uh then you have the static analysis approaches static analysis tools like uh Slither check marks Vera code where you analyze the source code to find for patterns that could be exploited for hacks and uh what these static analysis tools do is they perform an over approximation of the source code like they over approximate the behavior of the underlying source code so what can happen however is that they can lead to many false positives and negatives so they can show you issues that are maybe not real bugs to begin with so that is an issue with the static analysis tools by themselves the third approach we have is that of like automatic formal verification ation which we also employ at Satora that you have your specification your logical uh formal verification and you reduce that into an equivalent mathematical formula a logical constraint and then you just pass it on to third party uh constraint solvers like sz3 CVC 5 and they give you either an effective proof showing you how exactly your protocol is uh verifying the uh specification or they give you a bug uh showing you how exactly where exactly in the protocol uh a property is being violated of course these automatic verification tools are computationally expensive and they take a long time sometime they sometimes do take a long time to run fully and find a bug but uh as we'll see later the computationally expensive part is not the hardest part about formal verification and uh last but not the least we have proof assistance where you first write the specification and then you derive a correct code out of that specification so the code will be correct by Design and tools like the K framework and help you uh design such uh secure smart contracts however the problem with such proof assistance is that they involve laborious efforts they're very hard to use they're not plug- Inplay approaches and they're just hard to scale in general uh looking at the all these tools in a more pictorial representation you can see that testic and fuzzing can find many many bugs they're very useful uh and then you have the Satur approver the formal verification automatic formal verification tool which can find even more bugs and in fact the Satur approver can find all the bugs as per your specification so formal verification is as good as your specification if your program if the properties that you have written the specification you have written is like strong and covers all aspects of the protocol then the prover will find those uh bugs related to those uh areas as well and then you also have the St static analysis tools which finds some bugs misses some bugs but then again reports some issues which are not real bugs to begin with so we can also look at these tools in the scale of security versus automation so security is like how much secure how strong of a security guarantee does the tool provide how strong uh how how strongly can I say that my code is safe versus automation of how easy is it to use how easy is it to scale uh how can new developers just come and start using it all together so here we see that you have some tools like K and Co which are like which provide very high security guarantees very strong robustness but they are very hard to use and uh very hard to scale like new programmers have to have spend a lot of months beforehand to actually learn the tool themselves to then you make use of them in uh doing smart contract security and then on the other hand you have your fuzzing and static analysis tools like slyther and a kidna which are very easy to use plug-and play approach but they don't really provide a strong security guarantees so this is where uh Satur tries to come in and comes at that like sweet spot of having having uh if not as expressible as COA then equally as expressible in describing properties about a system and of course we try to be like as easy to use but not easier but not easier to uh as your testing and fuzzing uh Frameworks so this is where we try to come in and make formal verification more approachable to new developers and Veterans alike so at soral we try to build uh uh tools that can help you verify your smart contract formally verify your smart contracts uh we have the Satur approver that performs the automatic formal verification at the bite code level and then we also have tools like Gambit that can help you uh check the strength of your specification a specification is just like a list of properties and so you want to make sure that that list of properties itself is uh strong and this tool can help uh by mutating the source code and then make sure making sure that your specification is uh catching the bugs in the mutated source code so this list of properties the specification is actually written in this uh language that we have developed internally called CVL which is like a declarative language expressing what exactly a contract should do at any point in time uh we'll see an example uh in the slides as well of or CVL yep so here's a very simple example of a very simple contract uh where you have a very simple function f and all we really care about this function is that it should never return a zero so let's compare how we'll do a testing fuzzing and sat and formal verification framework so for testing you will first instantiate your contract your setting a to three and then you'll just check for random arbitrary values f of0 is not equal to z f of one not equal to z f of 17 not equal to Z great so for fuzzing you'll do something similar you'll instantiate your contract again with the specific value of a and then for all the random values of like 10,000 100,000 you'll make sure that F does not return a zero great however so there are two things to note in both of these testing and fuzzing Frameworks a the value of a has been specified like nowhere do we say that okay a can be an arbit value and B like you're still checking for only a limited number of inputs X ranging from 017 or like 10,000 100,000 values so this is where Sora and formal verification can shine where it does not it you don't need to restrict your program in those manner like you see this rule in that you write in a CVL a declarative format you say that okay let's consider X which is an arbitrary U 256 variable and we want to make sure that FX is not equal to zero we don't have any restrictions on X we don't have any restrictions on a what this tool does is like it it explores all these possibilities magically and tries to come up with the specific values of X and A that can actually lead to a violation of the uh smart contract so this is a very simple example but this goes to show that the strength of formal verification for proving uh cool properties about your programs and you can like uh extend this to your complex smart contract such as er c20s er 721s and other like uh pool contracts that allow you to write more complex properties about them so here's like a brief overview of like the internal magic that is happening inside the tool so you have uh your solidity file getting compiled to the evm bite code using a solidity compiler and then it gets decompiled to an intermediate representation called Tac and parall you have a formal verification spec which is written in CVL as we see as we have seen and that two gets compiled to a this intermediate representation tag so both of these things are combined together into a huge blob of TAC which goes through a bunch of like simplifications optimizations and uh other things and then get passed on to a a very long mathematical formula a constraint equation that gets passed then passed on to like a third party smt solvers like Z3 and CVC 5 that either give you a bug showing you how your protocol is violating the specification or the or says that there is no bug so you're basically getting a proof that hey your protocol is uh verifying is completely valid as per the specification of course there is an issue where your where the tool times out and this is because uh smt solving is like a computationally hard problem and to there can be cases where the tool times out and does not report either of the two cases and this is what we do at Satora we try to minimize timeouts we try to uh make sure that the uh the tool can generate an outcome in all most possible cases so a question that we often get asked is that where does formal verification fit in the development cycle of a developer and and the answer to this is that uh we we try to push a verification driven development approach for formal verification we want you to think of formal verification in the same way as you take think of testing in physic you have your for testing you write your function you write some unit test for that particular function before moving on to a new function in a similar manner you write your uh function in a inside your protocol in fact even before writing a function you think about the property for that function you write the invariant for that function and then you come up with that function and then you make sure using the prover that the function actually adheres to the in variance that you have specified in the specification if not you can go back maybe change the function or maybe change the design of the property itself make it stronger uh but if it is verified great you can do your development forward so formal verification is not something that should like only be left till the end of a development cycle it should be deployed continuously throughout the development process so as to make sure that you're developing a sound and robust system to begin another question that gets asked often is that does formal verification replace auditing like manual auditing and the answer to that is of course no it's uh formal verification auditing testing fuzzing all go hand inand to improve the overall security of your contracts they there nothing is like a silver bullet that can uh help you secure your contracts uh from all these hacks so you know you have you design your dab and then you write your code for it but parallell uh you also write a verification like in your CVL like you formalize that verification and requirements uh using like a formal language and then you test your code against that specification making sure that your code follows those properties but more importantly you also check the specification itself making sure that it is actually the properties that you want or you can make use of tools like Gambit Etc where uh you check the specification by mutating the source code and introducing bugs in the source code itself then you get a bunch of verification reports and at the end of the day of course a human has to look at those reports to make sure that the code is following the properties the properties are what you expect it to be uh and you know the whole system is working as expected before you can deploy and publish the protocol uh now many people think that formal verification can only prove an absence of bugs however I think the biggest value of formal verification is in is in finding those tricky Edge case bugs that are very hard to find using testing fuzzing and auditing Frameworks uh even in the case of like Hardware uh analyses the biggest value of formication has been finding some rare to find Ed Case bugs and uh as I mentioned before the hardest problem for formal verification is not the computationally expense extensive part yes it just true that it exists but in practice we see that the a hardware problem is for people to write good specifications about their system it's this the system design is a harder problem because uh it requires like a bunch of uh analysis a deep understanding of the system and we have seen many of times where our the specification falls short of covering every aspect of the system and as I've alluded to before formal verification is not a silver bullet it's uh not going to replace auditing testing and fuzzing but you have to think of formal verification as an additional aspect that you can utilize to enhance the overall safety profile of your uh code base uh it increases like everything combined together should make your system more robust to against Hax and um as we saw in the last slide formal verification is not something that should only be thought of as like a last step uh one one last time deal one once you have done the development it should be thought of at the beginning in fact even before you start writing code so that you can so that it can help you design uh Better Properties about the system and at the same time like uh write better implementation fall adhering to those properties so uh all in all formal verification can be a very useful tool that you can uh employ in Your Arsenal to secure your s smart contracts against bugs and hacks and yeah uh thank you everyone for giving me the time