Securify: Not Your Grandma’s Smart Contract Verification

thank you corrupted good afternoon everyone and welcome to this talk about sacrify Sakura is a smart contract verification tool which was developed by the people that you can see on this slide it was developed at ETH Zurich which is leading Technical University in Switzerland and you can learn more about sacrified by visiting the various links that will appear in these slides and I will make the slides available afterwards after this talk so first let me let me tell you the reasoning behind Sakura Phi and motivate the creation of Sakura Phi so most of you are aware assume in this room of the various security flaws that have plagued the theorems in the beginning so the most famous one remains the dowel bug which eventually led the developers to do a hard fork of the chain so as to river the state the state change is created by the attackers another more recent security flaw was a multi security bug which resulted in 30 Millions in a theorem robbed by by attackers so let me go into details of this second floss more more precisely so it was a case of in privileged right storage here I have a really simple example of this kind of flaw so just keep in mind for all the examples that are going to come that these are meant only to illustrate the flaws and not are not meant to to have a real logic in themselves so as you see here it's really a toy example so this is a wallet contract which contains the storage viable honor which specify the owner of this wallet and there are two functions this initialization function init wallet which can change the honor and this withdraw function through which the owner can actually withdraw money so you can see here this works so you can see here that there is actually a check to prevent anybody else from from from withdrawing money but the problem in case is that anybody can actually change the the owner viable which is a problem since because it makes the check useless so this is this is in a sense the the mystic peyote bug that is you allow anybody to write to your storage even though you rely on it for crucial operations so of course the exploit in the multi sick party bug was much more complicated because the contract itself was more sophisticated but the basic vulnerability is the same so there are many more security bugs that are possible with the etherium platform one of them is the category of unexpected ether flows for instance when you expect ether to go to your contract but don't provide any means to withdraw it so you end up with locked it ether in your in your contract in secure coding such as the mystic party bug so providing ways to write your storage without checking whether the user should be able to do that or not the use of and safe input whenever you use for instance timestamp or block numbers and pretend that these are random variables and even feed them into cryptographic functions for instance to create a pseudo-random generator then this is bound to failure because these variables can be biased by miners so for instance a miner can decide to not to process your transaction right away and this is going to be delayed by at least one block which gonna result in a higher timestamp reinsured method call so this is basically the DAO bug and manipulating ether flows by a transaction reordering so this is a bit specific to the a theorem platform where all the transaction can African where all the transaction can can be processed concurrently so for the details of this one I have another toy example this token contract where you have two storage variables one is the price of this token and the other is the the owner of this contract and so you can set the price where only the owner can can can change this price and the second one is a cell token where some ether is transferred as you can as you can see here a user can can call this function according to a given price so what happens in practice that a user can read the price variable on the blockchain everything is public and you don't even you don't even need to create a transaction to read the value of this variable but what happens here is that once a user decide to call this function the owner can still call another function so what would happen is that the owner would realize that there is a transaction pending with this this function and then this side okay maybe I want to increase the price or lower the price depending on what he wants to do so the thing is when you have a transaction pending you have no guarantee that it's going to be executed within the context that you that you just read and so in a sense the two operations do not commit and you shouldn't expect them to commit either so how to detect this kind of bugs I'm going to talk about automated security analysis as a way to make sure that these bugs are not implemented in your contracts so if I were to draw a big drawing of all the possible behaviors and I would I would have some something with all the possible behaviors and within them a lot of security bugs that you want to avoid when implementing smart contracts the problem is that you cannot enumerate all possible behaviors for instance if you have an earning an integer argument in your function it's going to be you cannot call this function with all possible integers and just say ok this this trace is faulty so at one point you have to make a trade off and decide how to to find the bad behaviors so the different security analysis approaches that you can have are here represented so the first one would be testing where you actually try to cover one path and from this one path you can extract one trace and try to - - to check whether or not it's faulty and whether or not it corresponds to what you expected dynamic symbolic analysis which is an improvement on basic tasting because you're not able to cover way many more paths so this is a bit testing plus purse if you want and so you have the same kind of guarantees that is testing and dynamic analysis report through bugs that actually exist in your in your codes and say they provide you with traces of what happened and put the can still miss bugs because your evolution of code coverage which is not equal to 100% so this is a problem because you can never be sure unless you have caught you have covered all your on your codes and that is 100% coverage you can never be sure that your code doesn't contain any of these bugs and the last one in the focus of my talk today is automated verification which makes a different trait of that is it can report false alarms but it has no missed bugs so it is a current state of the art for the Ihram platform what do we have what tools do we have and why do i suggest today so on the testing side we have truffle in populous which are respectively JavaScript and Python frameworks and help the developer to to implement that constructs and associated test and deploy them efficiently on the local dead chain and this way that developer can run these traces and check their assertions in an efficient manner on dynamic analysis sad you have a Yenta which was just presented in which allows the developer to cover when many more many more paths in his code execution and on the automate automated verification side we now have sakura Fida i'm presenting today and which as i said makes a different trade-off that is it provides you with strong guarantees at the bug that you are trying to find doesn't exist in your code on the other hand it can also report that the by the bug might exist in your code and then you have to look at it on your own and tell whether or not it's it's here so this is really a different trade-off from the two previous categories so if I were to summarize sakura in a few words I would say that Sakura is fully automated one click for more verification system for a 3m smart contract so I prepared a short demo and so I hope it's gonna work so this is recorded so here you have the interface of Sakura Phi you can see that by default there is some example of solidity code so this is the website itself so here you have a some solidity code that you can input tech so that you can verify it afterwards you can also feed some byte code or you can also input the address of a contract already deployed on a main chain so the thing to keep in mind here is that Sakura actually works on byte code so even if you give solid it could what is this gonna do under the hood is this gonna compile this code and work on the EVM code so now if we look at this simple example of a simple bank you can see here that you have a storage variable balances which contains the balances of the users you have a deposit function which allows a user to the pose to deposit some money and you also withdraw function so there are many things that are wrong with this code and I just want to show one of the code so here you can click formally verify and your you know have a security report with various patterns that are checked or not so the ones that I'm interested in right now is gas dependent reinsurance II so basically basically the DAO bug so if we click on the the matched line to find out where the the faulty code is we're gonna see that here there is actually some ether which is sent and some storage value which is which is set to another value at after the course so this means that the attacker through is fallback function can call this function and this dysfunction is gonna be executed within the same state which is the DAO bug so one one solution for this Posey's bug in this particular example is just to remove this line and put it before which is a quick and dirty solution let's say so if we click formerly verify again we're going to get another security report and in that case you can see that the pattern is not a gun check so you have made sure that your contract is no longer a victim of gas dependent s dependent reenter NC and this is a strong guarantee that is you're 100% sure of that there is no national code coverage here or they said that the code coverage is 100% so another example now is this flow the wallet contract so here you have a storage Bible which is owner which is the owner of the contract so this is example I showed earlier you you can initialize the owner of the contract through the first function in it wallet and the second function allows some transfer of ether if the message sender is the owner so we're not going to try to to get the security report out of this contract so if you remember it's the multi sick party bug so you see different patterns and here the one that I want to focus on is I'm privileged right to storage so I explained it earlier this that you allow anybody to write to your storage without any check so if we click on a match line we're gonna see that the faulty line is where you assign the owner to another viable without any any check so here's a solution that we can that we can use and that work that was actually used in a multi-state party bug was to have a modifier only honor which is gonna make sure that the function will be actually executed only if the if the message sender is the owner so basically having the same check as you had in this function but for the initialization function so here you click formally verify again and if you look at the patterns nights it's safe and so now your contract is guaranteed to be to be deprived of any and privilege destroyed to storage one last example quickly is that of the token with the changing price so this is a the other transaction reordering example that I showed earlier where you have this set price function through which the owner can change the price and you also have this sell token which is meant to be used by the by the user so if you click formally verify you can see here that the that that transaction may affect either amount so this is a case of transaction reordering because the unknown that can be sent depends on on the variable which is not constant so here a quick fix would be to just decide that the price is constant and remove any ability to to change the price in the future so if we click formally verify again we can make sure that this pattern is checked so of course in that precise case it it removes one feature of the of the of the contract that is changing the price so you will need to do a bit more to keep this feature that's it for the demo so now let's talk a bit about what's under the hood of sakura phi so first as I said earlier Sakura fireworks on the EVM code so you can exit the idiom binary that you obtained for instance by combination of the obvious solidity code and using this Sakura is going to obtain an intermediate representation this intermediate representation is only meant to be easier to process by static analysis the static analysis provides you with a set of basic facts about your code for instance you have you you know that this variable is a constant or you know that this variable is a balance and so all these basic facts are the number 0 of your iterations that you can run to have more and more facts so basically you have a set of inference rules that is for instance if a is a constant B is a constant and C depends only on a and B you will know that that C is a constant as well so you can imagine this sort of infants rules that we have in Sakura Phi to obtain more and more useful facts about the code so iterating over this you finally obtain a set of facts which is a fixed point with respect to these inference rules and so from from all these facts you can infer the security report that I showed to you earlier and which so basically you match the facts against patterns security patterns so we have a few now and we hope to increase the number in a coming in the coming months so what is what is important to remember here is that you this is fully automated that is the only thing you do is at the beginning providing the source code of of your contract and then sacrifice is gonna do all this part and provides provide you with the security report and this is easily extensible because you can add new patterns along the way so in our experience so far it was easy and quite quite quick to add new patterns because the the platform provides any sufficient primitives so our hope is that we won't have to modify sacrified that much in the future to provide to provide a new new patterns so following this experience we Sakura fine automated tools to analyze smart contracts a story was created in Switzerland to audit block chains and and smart contracts and the loop is really between auditing contracts and seeing the common patterns and try to extract the the routine out of it and so this is release this feedback loop that we try to to maintain to develop new tools that will they will improve on the current state of art so you can check out the information about chain security if you're interested on this website so to summarize a presidency clarify which is fully automated provide strong guarantees that is when it tells you that you're the bug doesn't exist they didn't means that it really doesn't exist in your contract and it's also extensible via a domain-specific language to create new patterns using the primitives already implemented following the experience we secured if I contact chain security was was created a startup that specializes in audit of small contracts and automated program analysis and with this thank you for your attention [Music]