EthCC 2: Dr Petar Tsankov

all right so the microscope all right I think we're all sets hi everyone my name is Patterson cough I am going to talk to you about functional correctness of smart contracts and how to certify this so we have already seen several talks related to finding exploits and detecting generic vulnerabilities in smart contracts here I want to explain what's the difference between looking for genetic vulnerabilities versus certifying custom functional correctness of smart contracts also we have seen techniques based on static analysis symbolic execution so we're going to clarify what the guarantees of these are and in terms of you know the guarantees provided to end-users so the team working on the things that I will be talking about on the left you see the research team were based at ETH Zurich and we are focused on interdisciplinary research where we combine symbolic reasoning techniques from program analysis as well as data driven techniques from machine learning to build useful security systems for different domains such as blockchain security but also some other domains and then on the right you see the chain security team which is a spinoff from the AI Center so there are we focusing exactly on blockchain security and bringing all these products and tools to the to the end user all right so I like to make this comparison here because there's actually something that comes in common when you think about smart contracts airplanes spacecrafts and so on so all these pieces are things that really have safety critical piece of software that must not fail once you go and deploy this thing all right and however there's a very important difference when we think about how what steps we do to make sure that no bugs are cure after deployment so namely if you look at how Boeing and NASA are deploying their software before you know you deploy it for example some controller on an airplane you would formally verify and certify that this controller is working correctly once you deploy it on on the airplane the problem is that only a handful of projects have so far actually have been formally verified for when we think about traditional smart contracts and this is a challenge so because the vast majority of the smart contracts were basically using most people using best effort techniques to ensure that no bugs would a cure once you deploy on the blockchain so that's clearly it's it's a challenge and the consequences can not be surprising that there will be a lot of embarrassing hacks and problems that will get missed out unless you do a proper development and all security auditing process before you know to make sure that all bugs are caught before deployment so our mission at jcq it is to change this so we want to bring formal security guarantees for for smart contracts and doctrine projects so essentially we want to take all the well-established traditional methods that we know that our capable and work very well for certifying critical safety critical software such as those deployed used by NASA Boeing and so forth and use those techniques to provide high-end guarantees also for projects that are building on smart contracts so more technically what this means is that we are doing some mathematical modeling to capture all possible behaviors of a smart contract so this allows us them to prove that the contract would behave correctly with respect to form of the foreign defined specification that contract and Wow something to mention here that form of reification is not something new in the space of contracts so there have been few projects that have been formally verified but the challenge is that the current technique that are being used to formally verify a contract or they really require a lot of manual expertise or they're very time-consuming and that's why not you know most products are not going this way because it's a really expensive process to go through and the way we want to change this is by building a lot of automation which can reduce this cost of doing form of verification for code for contracts by at least one order of magnitude and this way you could you know let's everybody benefit from this technology that's the goal alright so to solve this we have bill take a verified form of verify for each idiom contracts and this verifier is capable to certify custom functional specifications so I want to explain what what this means now but before giving you more detail on how you use such a system and and how it works and why is it challenging to build it I want to go a bit more into detail to explain why is it hard to certify such custom specifications for for smart contracts and against something I want to know I want to open a note here that I'm not talking about finding generic vulnerabilities like Korean currency transaction you're doing buffer overflows so these are basically known things that are bet and you have to check before you deploy but here I'm talking about checking whether the contract correctly implements the exact business logic that the developer has in mind okay so I'm going to give you an example of what this process looks like so to certify functional correctness you start well with a smart contract so you would have for example you would have a cloud set of smart contracts and let's say we have an escrow smart contract that's is supposed to keep all the funds that are being invested by the users then the next step is that there will be a bunch of different requirements that we would have to certify that are correctly implemented in this by the smart contracts so just to give you some examples for example we want to make sure that investors cannot claim refunds after the goal the cloud service reached so if the cross flow is if the crowd sale is successful no refunds should take place okay another example is we would want to ensure that the sum of all the deposits that are stored in this escrow contract always equals the balance of the escrow contract so intuitively this means that the escrow actually keeps the funds that are being invested by the users during the crowd sale and again these are not generic property these are specific to the particular use case and smart contractor your building right next to certify these requirements so they're roughly speaking this is between two steps so the first step is to formalize what these high-level english requirements mean at the level of the code so that means that we would take such an informal requirement and then we would formally write it in the form of a formal property so you don't have to worry about how you specify these property this is the actual syntax that we use we used in the varix form of verifier but the key point is that you precisely define at the law of the contract what what does it mean whether in a given state a property holds or not okay so that's step one once we resolve this then the next challenge is to actually check that this property holds for all possible states that your contract can reach and just thinking about this problem you would have to go through the following process so you would first look at the initial state which is the state your contracts are in after deployment after initially deploying your contracts and then once you deploy then users can start sending transactions to that contract and then there are many different transactions that they can send so each of those transactions it would change the state of your contract to another state so you would have to consider also whether the property also holds in those new in these new states that your contract can reach and it doesn't stop here because you know users a second user who's done a transaction then a third users would send a transaction and overall there will be you know unbounded sequence of transactions that your contract would run and the fundamental challenge is the following so first they're invisibly many transactions for us to brute-force so we cannot enumerate all the transactions and run them and see see if if if a property gets violated and the second challenge is that we don't really have a bound on the number of transactions that your contract would receive once you deploy it so this is this is really the fundamental challenge that that would have to solve and Wow there it's challenging so there are many different methods and techniques that can be used to to check to discover violations or to prove that the contract works correctly so I'm gonna give that overview on what these are so many review is not not as your price that's actually what more projects are currently doing you know panel review involves checking reading having an expert breathe breathe through the code and check if there could be a sequence of transactions that would result in breaking a particular property of your smart contract and the downsides of this is they're also well-known because you have to rely on the expertise on the expertise of this of the person who is checking it's time-consuming and especially if you think about functional requirements these are you know if you think in the context of a very large product it can be quite difficult for a person to grasp the really the edge cases of such projects so to do better there the next level would be to employ some kind of some form of automated testing and we have seen several techniques here today about this some of you have probably heard about techniques such as fuzziness or symbolic execution so let me actually show you what the guarantee is these would provide if you apply them to your projects so let's look at fuzzing classic we'll do the following it will start from the initial state and then essentially the father would generate a bunch of random transactions it would execute them on your account or on your contract and then this would result in Singh observing few additional states and then these are the blue check boxes here that you see on the slides however all these red boxes are the things that your are all these days that you would not see because your father did not generate a sequence of transactions to get there and there could be states that are pretty tricky to reach in practice so there would be such red boxes if you apply any kind of fuzzing techniques and so these are basically the blind spots that you would see if you want to that where box could could remain unless you cover those states and there have been many many tools that have been deployed that employ this kind of technique it's a very well-established technique for for software correctness in general then we also talked about how you apply symbolic execution to find bugs symbolic execution provides a different guarantee it's not like fuzzy here's the difference well symbolic execution is very good at handling the breadth of many different transactions so what you could do is you could encode all the possible transactions that you could run in a given depth and then this could give you a guarantee that for example once I deployed the initial state for whatever sequence of three transactions you send to the contract that you would not see any violations of the property so this is something you can guarantee with symbolic execution what you cannot guarantee is that if you have an arbitrary large sequence of transactions that that you would not have vulnerabilities there and this is simply because if you unroll this this large number of transactions the constraints that we just saw in the previous talk that would be so complicated that no SMT solver would help you in solving those so this is the fundamental challenge and limitation of these kind of techniques and again there has been many many different tools that have been deployed including the one we saw in the previous talk that employs this kind of technique and the goal is that you could it is you so because you could first you find interesting exploits and vulnerabilities in the first you know the basically which are few transactions long alright so these are I classify all many are we doing automated testing so these are bug finding techniques that they did not guarantee that you don't have issues but they are useful to find issues formal verification is kind of a switch because this is the point where you actually would can get a guarantee that your contract would work correctly for the lifetime of the contract alright so the goal here is that you would actually check compute some representation of all the possible states your contract can reach and certify that all the properties that you have in mind all the requirements would hold for the lifetime of the smart contract so that's what we're targeting so this is what verax does and now I'm going to explain to you you know this is great but it's not easy to build such a system so let me tell you what are kind of the key inside that we had when building the system and also what what is our experience in adopting such a form of verification approach when we when we check when we are in smart contracts all right so at the boundary level so this is how you use such a system so you start with the smart contracts the code of those contracts then we have some very high level requirements that you would want to certify and again this is not a generic vulnerability this is a custom requirement defined for the particular use case of this contract then as a first step this is a manual step where somebody has to on either a developer or an auditor would have to formally write this property in a language so I'll give a little bit more information about what this language is and what its capabilities are but the point is that we can formalize the requirement then the second step is automated so you can provide the COS code of the contract together with the formal property to the form of verifier and then this very fun would either tell you to tell you that the property holds and the guarantee that you get here is that once you deploy for any sequence of transactions you would never violate this requirement or it might tell you that the property may not hold and in addition it can output some abstract trace of how you may actually violate the property for example it can output some sequence of transactions that if you run them with some particular values you could you could reach a violation for specific requirements so that's at a very high level how you would use such a system so again the formalization of the property would be menu this is something auditors would do and the checking part which is the difficult part and this is delegated to this verifier which can give you this guarantee that's the property holds all right so I mentioned that we would have to formalize these requirements and something that was very important for us is to come up with something as a language specification language is easy to use by you know auditors and developers and here I have some examples of common properties that's come up when you add it or or verify smart contracts so some examples are well very often you want to check the access control well access control is implemented correctly for example that certain functions like deposit are only called by by an owner these are things you may express in this language very often you also want to check very specific state-based properties for example after a certain time so in this example after one week after the refund time has started then no refunds can be made right so you can formulate such things you could very off contracts have non-trivial state machines so if you think of a crowd sale you would have for example presale main sell and then you would either lock into a successful phase or a refund phase so here for example you may formulate that the refund and the finalized phases are kind of disjoint so if you reach refund stage you would never be able to in the future reach a finalized State and vice versa so basically there very often you want to check that this state machine is correctly implemented in the contract very often also we encounter invariants over aggregates like mappings and erase because he's you know in so easy for example you don't have a way to iterate over the keys of a mapping so often you have auxiliary fields like total supply to capture the total the sum of the balances in the contract so you can also verify that those in these invariants holds and if you think of large projects you also very often have invariants over multiple contracts and not only over a single one these are also things that very commonly pop up so the foundation of this language this is it's an extension of our solidity with some quantifiers but it has a very solid formal foundation so this is based on linear temporal logic which has been studied in decades in and you know we very well know what are the complexities and expressiveness of these of these techniques the second challenge that we had to so address is basically how do you deal with this unbounded state space of the small of the smart contracts and here we employ two main ideas the first one is to leverage a symbolic execution to precisely reason about how individual transactions work so this you can do because it is scalable enough to reason about depth one meaning a single transaction and then the second idea we combine is to leverage program abstraction to bound the size of the state space so this is something that would allow us to make this task of verification computationally feasible so this is definitely is not something that can be explained here in five minutes but feel free to ask me afterwards if you're curious how you can combine these two techniques and there are many many other challenges you have to if you want to build us do they sound symbolic the very fire there are many subtleties that are specific to to solidity and ethereal for example hash-based the locations you have to reason about gas mechanics if you want to verify you know you you have to all these features that are specific you have to handle them in a sound way if you want to have at the ends a sound as product your form of very far can guarantee the property so I have listed some of some of the common pitfalls that we have observed in existing symbolic execution engine so they typically there will be some variations of those word that would not be handled with fully sounded so to speak alright and in terms of impact so we have in what what the system achieves is really fast and scalable formal verification for contracts we have done a number of case studies with on the research side as well as with with concrete clients and we see several important benefits in this place if several important benefits that you get if you adopt such a verification approach the main one that I would say is the the mentality switch that we're not longer talking about book finding and best efforts we're actually talking about I certify that this works and this is something you can put in on say an audit report and give a guarantee to the end-users and that's useful because ultimately the end user wants to see what does this contract do and this is what you want to put in the audit and other benefits are more practically useful because for example very often contracts to implement common functionality so you could for example define a library of different specifications for tokens and cross-sells and then reuse those across different audits of similar contracts recertification is also cheap because once you can formalize the properties if some of them were violated because there was a bug once the code fix comes from a plant you could rerun the system and check if this this fixed actually address the the the particular problem that was found by by the verifier all right so how do you get access to this well we're going to release a demo of the system that you can play with including like play with the specification language to see what the capabilities are we're going to put this upload this in the next few days at vertex dossier for now you can go there and put your email and we'll notify you when when we upload the foods MO and if you're interested to use this as a service for example to integrate it within your development process or protocol just send us an email and we can chat so do I have maybe one two more minutes I'm gonna make one more quick announcement not related to form of reification so yesterday actually we released the first framework for automated testing of Civility compilers and we're now looking for people to join us and help us further develop this framework it is also it has been the development this is fully funded by the Athenian foundation so this system is basically capable to generate thousands of different semantically equivalent contracts and then run them and check if the compiler messed up in one of those cases so you can find more detail about here I mentioned so this system already found few bugs some of you may be recognized some of those bugs and those have been addressed in in in the in the latest version of the compiler if you want to find out more so this is where the code it's publicly available and we have the discord channel where you can join and you know just talk to us and see if you want to contribute in some form so with that I conclude I hope I convinced you that what's what's what certification of contract means why is it important and what are the different methods and guarantees you can get if you want to do this and yeah thank you a lot I'm happy to take a few questions if they're staying [Applause]