Formal Verification for Solidity

[Music] so I guess we all agree that uh it's really really hard to write 100% uh correct code regardless of whether this is a smart cont contract or any other piece of code and but what does it actually mean to write correct code what what is the word correct mean and uh I think the the best explanation is that uh code is correct when it does exactly the same thing as the the programmer intended it to do so the the mental model of the programmer about smart contract or about the the program is the same as the what the the actual machine does with the program and for ethereum uh this extends even more because we do not only want uh the the expectations of the programmer to match the actual program but we also want to match uh want to match the expectations of the user to match the the actual execution of of the program and so how do we get to that point uh and there are of course several uh well established techniques and one of them is to to to uh yeah write use testing unit tests um and that that's quite easy easy to do you just think about uh a certain input and make up your mind about what you're expected to happen and then run the program and see whether that actually happened and that's good to to check whether uh desired behavior is actually there but it fails to show that under desired behavior is absent so you cannot use unit testing to show that it's impossible to uh withdraw money from your smart contract by a malicious actor and the reason is because you would have to check all possible ways to call the contract and that's an uh infinite number uh and yeah testing can only do uh Finly many cases uh let's let's so yeah and but there's a solution to that and it comes in the form of formal verification and let's take a look at an example there so this is an this is an easy token contract which has a balances mapping and uh a function that allows transferring uh yeah balances from one account to the other account there is a tiny error in there and not sure if you see that and I would argue that so yeah testing can detect that error but most people probably won't think of this specific input that is required to trigger the test or trigger the trigger the failure so uh yeah what's the problem here it looks correct but uh it probably also will work correctly for most of the token contracts out there but what it fails to test is whether there's an overflow in the in the in the two Fields so if uh if the amount you want to transfer and the amount that is already there in the Target account sums over 2 to the 256 then we get an overflow there and uh the the mechanics don't work correctly [Music] um yes so uh and formal verification allows us to ask questions like uh is the sum of all balances unchanged by the transfer function considering all possible states of the contract and all possible possible inputs to the function next so how does it work in general um so you you provide formal statements formal mathematical statements about the the behavior of a contract and then you use mathematical proofs to show that uh the code satisfies these statements you can do that manually but since we live in 2016 there are there are of course automated provs to help you there and find the the mathematical proofs um but so one thing I want to stress here is that formal verification is not a silver bullet the reason is that um so the the source code so a programming language is already a formal description of a program so and adding adding formal statements in another language uh or completely formalizing the behavior of a smart contract will not really help because as I said in the beginning it's all about the mental model of the humans so um the the key goal in using formal verification is to reduce the complexity of the smart contract we use source code uh to describe how an algorithm works and how a smart contract works and then we use formal verification to describe what it does and the idea is that this what it does is easier to understand then how it does it and another another great uh thing about formal verification is that we can ask questions about the behavior of the program so it's not only about formalizing it in in a kind of a specification but we can also just add to that and ask questions like is the sum of all balances fixed and if there is some way to modify the balances so that the sum is not fixed between two calls then uh the system will tell us or uh yeah we can also ask questions like will I smart contract get stuck so is there any way to uh to send messages to the smart contract to call functions in a way that at some point it's not possible to move forward in the in the states of the smart contract or it's not possible to to get the money out at all anymore so uh yeah form verification is coming to ethereum there are already uh a lot of research papers on that topic um and the reason for that is that blockchains are actually a paradise of Home verification because uh yeah the the model is that simple but uh U later will tell you more about that um okay and formal verification tools also exist for kind of a common languages like C and Java and Adda and uh these there are and the way it works for these tools for pharmacy for Kato and for spark is that you write your your program in the the ordinary language you're used to like like C and then you annotate this uh source code with uh formal statements so like solve balances is a is fixed between two function calls and then there are tools which compile both the source code and these annotations into to a language that can work with the annotations this is often Y3 uh and more recently we have fstar and then um automated provs are used to verify these formal statement on the translation of the source code let's take a look at an example so this is this is from a c and you see that no no pointer um so you see that there at the top there is a block of comment with these formal statements and then at the bottom you have regular C code and uh you also have comment inside the C code where you can refer to uh the state of the program at that point so yeah let's not get into detail there and uh yeah now uich will take over here it is here he is and uh so uichi is uh a formal verification engineer who recently started at the etherum foundation and he will focus on uh extending the formal verification uh features of solidity hard yes uh so Christian started this solidity to Y3 translator um that's similar that flami but for the smart for our smart contract language solidity I extended the framework so that it can deal with the arrays and it can deal with the simple token contract with just one transfer function um the contract itself is easy um it has a transfer function uh you can specify the from address to address and the value and some balances are changed um this is the same thing as Christian showed before um it has the same problem with the buffer over no integer overflow um the tool correctly complains if I don't specify that the total balance is less than a certain big number otherwise the to complains next slide please um when the smart contract has a problem we see a window like this um this is Y3 GUI Y3 is a front end for dozens of automatic and manual theorem provs and on the left side you see lots of conditions desired conditions like no integer overflows no buffer overflows and so on you see many green chicks the green chicks are on the verified conditions and Y3 can automatically verify most of the properties but you also see some blue question marks the blue question marks are on unverified conditions uh wisely still doesn't know if these blue questioned properties hold or not um when you click on one of these question marks on the right pan you see a yellow highlight on the suspicious piece of code um the code is a translation of the solidity contract into Y3 yml language that's a language for Y3 and here the highlighted line is uh subtraction um so in this case this might underflow um and when you see such a problem you can either modify your pro program or annotate your program more and more um annotation is like putting assertions in the program and if you put enough assumtions to um satisfy the automatic provs the automatic provs will say green check but in many cases you just find problems in your specification so it's about adjusting your own mental model next slide please um so before finding slm I was looking for a place where formal verification actually makes sense um before the I joined the research institute my job was to spread the formal methods into the industry but I didn't have any access to any company's source code so it was hard for me to do that so I joined a company that hired former verification Engineers that was a US company I had eight colleagues writing proofs were a wonderful environment but I I was not happy because our proofs were not about the real thing um the fundamental problem is the real CPUs come with documentation 2,000 pages long and nobody has ever translate translated the whole thing into any theor and provs so that was a huge problem we couldn't solve um I found eum I saw the eum virtual machine I saw the yellow paper the specification uh it has only 32 pages long and I I thought I can actually translate this thing into a theorum Pro and I can write proofs about smart contracts I was doing that and I was posting the partial results on vit and Christian found me and I ended up here um so the V machine is wonderful because it has a small specification and this small specification really matches the reality because all clients try really hard to match this specification otherwise one of these clients would behave differently from others and that's the worst thing they want so they really want to be conformant to the specification and a small definition that that matches reality is the fundamental necessity for formal verification engineer I found it in E next slide please um we have some future steps um so when I'm extending the solidity wi3 framework um there are some immediate problems like or we don't have the Cora instruction yet in the ation or we cannot deal with mapping to mapping in Y3 in a short and elegant way um because of this we are thinking of moving to F star fstar is something similar to Y3 but it has more advanced features um I want to thank Microsoft for open sourcing F star and also G3 smt solers and we extensively use it um thank you very much um but feature wise um we have more problems to solve than just verifying uh one solidity contract um I think we are moving to many small contracts than one monolithic big contract so we have to be able to reason about multiple cooperating cond contract [Music] and and then just reasoning about solidity code is not enough because what runs on the blockchain is not a solidity code but a compiled B code and sometimes the compiler has a bug so somehow we have to know how the bite code behaves whether it's evm or the evm 2 the second one um so somehow we have to do that but um that's easier than most CPU architectures out there so I think this is a solvable problem um the next one is uh multi transaction conditions So currently the precondition post condition in variance on the contracts uh just on one cord um it can already deal with the re entrance but uh from the first call to the last return and that's the range of verification we need to extend that um and then yes and combination with offchain protocol um this is harder because the moment we get off the blockchain um people's behavior or yeah are not constrained by clear rules so what's good for people is not very well defined but somehow we have to Def Define a game where it's in the players's interest to be to coordinate with the rules um and the formal methods can help here because it can explore all possibilities of interaction um the last point is rather practical um so you saw some blue question marks but just a question mark is sometimes not enough for me to understand the problem so it would help if we can see counter examples like with this input with this state this is broken and then um it's more easily understood um but I see I believe many more formal verification researchers are coming to the verification of vum smart contracts because of the reason I mentioned thism virtual machine is V Paradise for formal verification engineer thank you very much thank you [Music] Yi and