🛠 Effective Code Security Tools - Mooly Sagiv

foreign [Applause] [Music] so don't worry it's uh it's basically a Hands-On Workshop but I thought maybe I can give you a little bit sort of high level interview about a sort of overview of how this tool works I I really encourage you to ask questions during the during the presentation so the pain point that we are addressing I'm sure you know it's but it's not specifically to web tweet that you have buggy code I think there are a lot of code analysis Tools in web 2 and in web3 and what my feeling is somebody who's working it mainly from the academic side that they don't work and there are two reasons why they don't work and you can see it from most existing tool is that they have false positive and they have false negative they have many they miss arrows and actually most of the errors that they report are not with and this is actually where you will see if you can come and stay in the in the workshop you are in such an arm and they will actually show you how to make this actually this tool which actually works in this at the moment is only in web3 and solidity and Viper but we think that this tool can be used also outside the area of web3 uh what Chateau is doing and we are building different tools I'm not gonna I'm only going to show you and this or the workshop it will be only the Satora program but Satora is building different tools for code security and the other side of the coin which is something Satora doesn't do but it's equally interesting for us and that's why we are here is the connection with the security team so basically there are security teams like code Arena actually interested in spare beats and others 12 of bit that interested to use this technology and there is synergy between the people between the community and between the tools and that's actually something we love about it and of course if you want to engage with us we will get actually a trial key and you can try the tool and if you want to work with us and all also with code Arena that's actually doing this that's great uh so basically the the the glue the the interface between the community and the people at the moment is the severe language that you will learn and and you will learn from the team here is that basically it's a language for expressing properties of your code so you write some kind of properties of your code in our language and then you can use our tool to do many things and in particular we can find bugs for you so maybe just sort of just to give you intuition why I say that actually existing tools do not work I'm actually using one of the best effort tools so this is liter how many of you know slither fantastic how many of you used Lita looks like yeah so Slither is fantastic tool because it's actually very easy to use but the problem is little and you can see that here I ran it on a very very small contract it's a it's a tiny it's basically a low word and you see many many red arrows do you want to guess how many of them I will none exactly so the problem we want tools and what you will see today is tools that you have arrows that when they are produced they are produced with with actually sort of a test case showing the violation so how does this tutorial tool work you will see actually today you will see you will learn but the idea is that you you kind of write your code twice you write once you write your code in solidity or Viper or Russia or any other language and then you write what you think about your code these are specification these are some properties of your code and the tool can do two things the tool can give you a proof that's very interesting but it's a bit boring it says okay verify but the most interesting use case of this is finding bugs which are hard to find and we have actually used this tool before auditing and after the best auditing and found very interesting edge cases in your code some of them you can actually use to actually deplete completely the money so this is the tool that we are using it's basically a tool that actually automatically either proof property or actually find a basically find test cases in the case indicating violations of these properties I have to warn you we are addressing a very very hard computational problem it's considered the hardest problem in computer science and this means that the tool is doomed to fail in certain cases if your code is too complex if you have inline assembly we can handle it and we need sometimes help from the user so there are failures of the tool and their their mechanism where you can handle failures so if your card is too complex that this is unavoidable because we are addressing a problem in computer science which is called undecidable which means that the computer will always and since our tool is automatic unlike existing framework if you have this tool is automatic you just write what you think about your code and you it's almost like unit testing you get you get a proof or you get a violation inside sector approver I'm not going to be able to show you but there's a lot of Technology involved there's a lot of Technology it's actually and interestingly the tool actually doesn't analyze your solidity code it analyzes your bytecode so it invokes the compiler and then after that it analyzes your solid your bytecode and it's implemented a lot of sophisticated method that we actually have developed and they it were developed in academic in Academia in the last 30 years in order to work them most of them are relevant not just for blockchain they are relevant for low level code in particular I want to point out that we have sort of a very very we pointed out about Slither so inside Satora there is actually a very very complex leader there is a very very complex code that checks your code and actually this complex code by the way it found many bugs in the solidity compiler itself which are acknowledged by the solidity and the other thing that we are doing at the moment you can think of Satora like a kind of smart compiler that compiles your code into a mathematical firmware but this is is a naive solution and usually it works in certain small code so what we do we do a lot of things to make your tool work on realistic code and this is a lot of complex things there's some information on the website we actually just published yesterday evening a white paper we encourage you to read and I don't know if you got it we asked so we just published it for this Workshop so please read it and also I'm here this week and there's a lot of people on the team they have a D team is coming so please ask us questions uh this is just one acknowledgment from the solidity team about bug security bug actually was found by by the center approver so how does it work you will see later from Europe but the idea is you write your code and you write some environment you see for example this is a very very simple kind of transfer and the invine says that the total is is equal to the sum of balance or maybe you say that the sum of the balance doesn't change and the tool can actually give you a proof that this is preserved and maybe it's boring because it's very simple code but this is the kind of fish that you can prove and of course if you have overflow in your code then the tool will identify that and give you an edge case for the Overflow but if you do not have a flow overflow for example you're using save mass or use you're using solidity 0.8 then in fact it can guarantee a generator proof and you generate the proof on the evm level uh so that's nice but that's kind of boring I said this is a bit more interesting here is I guess it's it's kind of a trivial bug but this is a case that you have a bug a cold with a bug I'm sure everybody most of you have seen this bag it's so silly but still do you wanna do you know what's the bug here so the problem is that this chord does not maintain the envirity you want to guess there is a violation the tool will find it but I'm sure you will find it too just a bit so what what can get wrong here it's almost like the same code it's like done in two steps basically it's a sign in a to a local variable and later on and then these local variables is stored into storage nobody can help no so so let's assume it to you in so balance cannot be negative overflow is is an interesting thing but let's assume we are working in safe match because otherwise the previous code also so let's assume overflow is is a bug but I'm interested I'm looking into a more interesting bucket this bug by the way allows you to a lot of money was stolen using this button so it's a it's more interesting than overflow it's it's it's almost trivial but still be that is some yes valency is is not a problem here because it doesn't call other codes we can check reactive but here it doesn't call either code yes exactly fantastic thank you very much so it's a self transfer and you see the tool actually you can find it so this is the kind of thing that we want to find and I can show you that we have we found many more interesting errors because this is a very very simple error but still you know Visa text lost few minutes this way but this is a this is a kind of box that we want to prevent before the code is shipped uh so the biggest value of this technology is inside your development is basically integrating to your CI so every time you change your code you run this this thing you write this specification and if you write this specification right you can reuse them every time you change your code we are finding that sometimes different customers can reuse the same specification which is fantastic uh so what you will learn is writing specification and specification one way to think about them and this is of course go back to Aristo his invariant you write some things that you think if this is the property that all your stage in your program has to satisfy and in D5 the interesting thing when you have assets you want to basically make sure that you have this the the enough asset to cover your bill and this is what you have to write and you will see later in the workshop that you write these environment and what the Torah does it does two things it's basically build you these tools and these tools you but you can actually write in variant and you can check them and it's basically a tool for the community for auditor for security researcher for developers to have to write this environment and to check whether they hold or don't hold how is the Torah doing today so this is just so you see that actually it's a storage is actually protecting some of the most important protocols ah in this space we are actually analyzing many many lines of code actually if you count in evm it's even more the things that we are and people run it like this companies will run it actually more than us it's a cloud-based you will see the thing that we are very very proud of the bugs that we have prevented so with this technology we have prevented a lot of security bugs and I will give you just example but you'll see a lot of our website and some actually acknowledged by our our customers so maybe I just give you few kind of examples that we have found so sort of the biggest property that you can think for for D5 is solvency which means that even if everybody goes to the bank you can still get your money so maybe insolvency means that you are bankrupt and these are insolvencies issues which are found by the sector approver after a manual audit so these are teams which are very very careful about security they use the top and you see that they use the top Auditors and we want the tool after the top auditor said that the code is correct okay and these are the bugs that are found by this technology and I think this is actually how you can measure this technology how many bugs are found uh how is this technology compared to other tools so of course there's no Silver Bullet and even if the formal verification is not actually observable so the idea is manual audit scores can find bugs that flow multiplication will not find especially if you don't have device specification and and writing specification as you can see is actually hard so the the idea is that many allowed it actually supplement formal verification and you should do them both testing and fuzzing it's very interesting and usually cheap and actually it's a tour is building his father his father but that's usually Peaks and inputs so the coverage is much less none of the bugs that I showed you in the previous slide were actually found by five things but it's of course things you want to do and I mentioned already static analysis like Slater which is incomparable it misses some bugs and actually most of the bugs that are reported are not with so that's very very different but of course used I want to give you just one example and I feel I think it it doesn't have significant but this is a true fire this is a team that using the sector approver they have done kind of uh uh study they basically use the sator approval with Auditors and they inserted bug manually and they want to know who found the box so what you can see it's kind of interesting many Auditors even good one they miss Park Seto also missed one bug but and of course I mean with the woods that they were but with the rules that they wrote you see that actually it's a 12 pound more significant bug the tool than all the the humans themselves all the human together sorry so the idea is this tool is really really useful if you compare that to human because humans are very good in intuition but identifying edge cases this is a case that a machine can sometimes be better than human especially if you write the right requirements uh I want to sort of give you uh a little bit of sort of technical Contents I mean you will see actually much more with your and and Sasha so the idea is just give you an intuition of what is going on so I took a very case of simple case of the sushi so basically sushi but that's actually amm you have you have basically constant product pull so you have two tokens and the multiplication is constant so for example you have 50 tokens a and and and 200 B tokens and for example you want to buy 50 B tokens okay so this is what happened you buy 50 then you have 66. and you see that you why do you have now 66 do you want to tell me why is why is it that you have 66 what's the rule that is maintained here exactly the multiplication is constant so this is the environment that we maintain so we maintain the environment that the multiplication is constant so that's the idea and if you want to think about it even more simply it's basically you maintain the fact that if one of the tokens is zero the other is also zero and this is a very simple variant of the code okay but guess what the trident broke this environment and when this environment is broken all the money is lost okay so our tool basically found and this is the code actually the code is not very complex but still you see it has some non-linear Mark so it's been single this is an operation and the tool finds an edge case it's actually a very rare Edge case but under this Edge case you can break the environment and as a result you can actually get all the tokens in the in the post so how does it work you see this juicy Dragons by the way you see I told you it's a simple code but it's already actually a 2000 line of solidity code and it's actually 24 000 line of evm so actually the two handles actually quite significant part of the code and basically the environment that we maintain is that the both of them need to be zero or nine of them is zero and this is a very simple invariant but look what happened it found the case that Alice bands her holding and gets 200 tokens and as a result you see now the basically the the B tokens is zero and the a token is not zero and the environment is broken and what is the significance of it the significance of it is that somebody and this is something of course that is a Torah tool doesn't do this Torah tool doesn't find the exploit the Satora tool only finds the violation of the environment but then we manually look at that and show the team that actually you can now once this environment is broken you can actually exploit the quantum and how will this work so basically this is the case you have this tridents you have Alice and Bob so Bob basically deposit 100 tokens 108 tokens at 100 B tokens at least now deposit also hundred eight hundred B tokens so all together we have 208 tokens and 200 B tokens everything looks fine there is also something about LP shares but I'm not showing it to you because it is not relevant to us but of course there are LP shares I'm not showing it to you it's not relevant and then Alice transfers transfers a tokens to Trident so you see now there's a lot of money in the in the case but now Alice can burn a holding and she can basically get this 200 token and now you see the environment is broken as we see so what happened now when the invite is broken what can you do how can you take the money home so you I'm not asking you because you're probably not familiar with the sushi code but the idea is in the sushi code there is so the environment is broken so basically as Alice she pays one token and she gets all the sushi okay so she gets all the money basically you see that now Bob is left with nothing and that has got all the money because the invite is broke so this is exactly what we want to prevent and actually formal verification is one of the tools to get this uh I want to give you just another example it's even more interesting I think because it's example that found by a team is found by the make your team and basically they actually this is a code that was actually live for four years and actually they they basically uh this code I think uh holds about six billion dollars and you see that's actually called very uh fantastic developer at the sushi team and so at the make your team he basically uh wrote the environment with the software approver and that's the top of us say it's not environment and usually you know when we work with static and as a tool when it is a violation we suspect the problem there is a problem in the tool but no in this case it's a problem in the code the invite is broken because there is a problem in the init case so basically there is a complicated invariant it's a bit complex it has some some about and actually what it says is that it's a stable coin so the die actually actually represents a stable coin and guess not guess what the tool actually can show you that it under certain cases it's no longer a stable and it actually show you you see that the unique has an edge case in the in in the edge case of the need it's not a stable uh I want to actually just give you a little bit of why we are doing all these complex things so there's a lot of other projects there are open source at the moment we are not open source including uh these are a lot of some fantastic academic colleagues I guess there is a mystery lab they have the move language so a lot of people have actually formal verification and it's called vanilla and what they do they reduce to smt which is what we do too but it's only the beginning so basically the idea is that we you can actually build a tool for formal verification at least an initial tool very easily you basically reduce it's like you you take your code and you convert it to mass and then you so use a solver either to find bugs or prove their absence so that's basically the idea of the vanilla solver you see I take this code with the bug and you see that actually each line of the code is converted into a mathematical equation and it looks almost the same but it's not exactly the same in the left hand side you have a chord in the right hand side you have mathematics in particular for example in the left hand side you have 256 integers in the right hand side you have mathematical integers and in the right hand side we can actually reason about the behavior precisely and then basically the tool automatically finds the bug this is the vanilla verification but and this is something that I have to uh I'm not going to explain to you but if you do this vanilla verification on interesting code it will not work and what we have in Satora we have mechanism to avoid that and we are not actually doing this vanilla we are doing we are starting with this vanilla verification but we are doing more things to make formal verification work uh and the key idea is actually specialization we basically sort of do things which are specific to D5 we understand something and we understand some invariants some properties of your code that makes this formal verification feasible and this is actually why we can catch all these bugs so when I told you that we handle evm I I cheated a bit in a sense that we actually handled evm that we like but we can check if the evm is the event we like and of course this is checked by computer so the tool is fully automatic the tool handle your code and checks the properties and verify them uh and and and basically I I'm just repeating we need the simplification for financial systems because there's a lot of things that make formal verification hard in financial system non-linear mathematics and other things uh I just want to point out that we found as I said many bugs in the compiler basically using our analysis so these are bugs that we found all of them are disclosed and actually uh fixed I guess resigned usually a week by the solidity team uh let me just give you one to give you intuition so basically there is persistence torrent in the evm and it's separated from the memory and you see that actually this is the code that the solidity compiler had to check that so you see that anybody Sports the bug here so basically you see that anybody with a good ions on code do you see the bug here it's actually very silly but it was found by a tool but a human also if you look at it uh you see the bug there is so this code is buggy it's a it's meant to check your memory that you don't do buffer over but in fact it allows you to do buffer over uh do you see the bug okay it's it's a so basically you see that the this here it says if if a length is greater than 31 then it's it says if a legs is equal to zero this is not reachable and even worse it is not checked where it's supposed to be checked so this is so this is redundant the problem is that the solidity compiler guy I guess he worked too late so instead of fighting this if here we wrote the if here so this is a bug in the compiler itself which was actually caught by the Satora tool and that's the idea so this week so basically it allows you to actually read memory so you can read memory out of bound which we don't want and of course this is actually prevented by us music for my verification I think we are preventing more interesting bugs but then we need specification but this is a case that we even don't need the specification to find bugs I want to conclude basically this tool for formal verification that you see it's basically give you the ability to check the properties of the code and we reason about very very complex things on your car I think we have this analysis which we call pointer analysis we analyze the memory in a precise way I didn't explain but if you want a lot of information in the website and in the white paper and and and basically the importance of this technology is the bug that we are to invent maybe just to give you a quick overview because you probably heard a lot of tools there was a cave framework there's framework there is about a lot of tools so these are very very uh these are academic tools they're very interesting a lot of people have been working on it and on the right hand side you see Industrial Tool they're equally interesting these are things like Mutual by consensus and kidnapped anti-coins liter by 12 of B so all of these so these tools are very scalable these tools are very hard to use and you can check because it's actually require different things and where is the tour hopefully Satora wants to be somewhere in the middle so Torah wants to be almost as expensive as as sorry as expensive as powerful as this but she wants to be something that you can use and you can judge yourself if you stay for the workshop if this is where we are but if you want to compare we have teams which used to work in maker and you can ask them they like to make it so so do you choosing k for example they make your team they they they work large long time with scale framework and you can see so basically using our tool is much easier it's almost big like a unit test and you will be the one to judge uh I think I'm done there are a lot of people in the team we have a lot of people that some of them are here we have expert informal verification in tools uh we have a uh yeah and we uh so I I don't have the sounds like we have a lot of experts which are here on on the D5 and why I'm missing the slide I want to basically uh uh uh finish this talk by by the uh um sort of tell you a few lessons and of course I've been in this space for a long time formal verification is is a very very beautiful area of computer science and a lot of very good results I don't know if you know in computer science this thing which is called touring world like a Nobel Prize the most number of token in the world are informal method but there are a lot of myths people miss a lot of things and there are a lot of myths about formal verification which are not real and I want to basically point out to you because a lot of hype here especially in the area of smart contact but not only so the biggest missed on formal verification is only for proof but actually I think it's wrong the biggest value of formal identification is actually the the is finding bugs not actually the proof so that's actually and actually I'm not the first one to say it's actually people have applied formal verification hardware and they by far they reached that the other thing which is actually unders not well understood is that people think that formal verification is hard because it's hard computationally it's of course to but the hardest problem informal qualification is actually writing the specification and I think this is where in blockchain it's very interesting uh there are a lot of other things but I wanna and I I already mentioned that formal verification does not replace auditing but maybe the last thing this is what I want you to come from this talk is that formal verification is not a one-time deal and you don't want to start it late formal verification is something that you want to integrate into your development and you want to start early and if you are an early project and if you are working on any project whether you're using other tools or not it doesn't matter but start thinking about at least format specification and even later formal verification or even tools like nkid now Slither or any other tool when you start developing that's much easier and that's much more useful uh I'm done I want to say basically we are working on this area of D5 of or smart contract you will see a lot of things but we have a lot of things about the specification and uh we have a lot of other tools for for checking their specification so I'm I'm ready to take questions I'm hoping you'll get some questions but you also get the other people who will give you more Technical and hands-on experience but I'm happy to take questions no questions thank you very much thank you for your time [Applause]