Move Fast and Break Nothing

Transcript

uh thank you for staying that late I'm s uh I'm originally from Tel Aviv University but now I'm on leave I'm working in Satora so Satora is actually a sizable company which is actually trying to protect the smart contract and it's very much related to the talk you you heard by eel about applying static analysis and basically what we can show you we have this static analysis tool which actually can prevent many of the bugs before the code is deployed our team consist of actually many many excellent people many of them are actually here we combine expertise in formal verification with expertise in

C security we come from top school from uh etherum for for for the IDF and we basically try to match them in order to make the this area more secure so what we are trying to do here and it's basically we are trying to to convince the community to actually write formal specification for software and this is of course something that has been around for a long time but we think that in this domain where you have a lot of money at stake this is where you actually go going to do this specification and we have our own language and you can look into our website we have a lot of specification we have specification that we wrote and

we have more interesting specification that customer like maker and others wrote and it's very interesting that we see people in this domain writing specifications and these specification they are reviewed by human but they are also checked by the machine and we are developing the technology to check the specification we check the specific the specification themselves but we also check that the code adheres to the specification and interestingly we are finding a lot of bugs before the code is deployed so in terms of whom we work with we are really we started actually working in this domain and this is domain is an expensive domain because you have to invest a lot of effort in

writing the specification and also a lot of computational effort in actually checking the specification so we we start where the paint Point are and the pain point is where you have a lot of money at stake so basically what we are doing we are controlling the and actually we are checking the code before it's deployed and this is complementary to auditing it's applied before the audit and after the audit and we are very proud to find the bugs and prevent them before the code is deployed our technology actually can run with the actual executed code so it can also find boxs after the code is deployed and we of course report them in in a quiet manner our technology integrate into CI

and we'll talked about it later what is the technology that we are developing so actually this technology has been around for a while and I think Isel mention it in the talk it's called abst interpretation actually most of this work has been done very very close to here in in a place called a COR normal super year and we have a workshop there tomorrow so please come to this workshop and actually we are teaching in them and this technology has been industrialized and there are different tools there is the cover to Tool which is a standard tool it it's a very simple tool but it's a standard tool there there is absin which is a more advanced tool which is actually started by the cuso and there are other tools and in

domain of smart contract the the leader tool is sliter and sliter is actually a tool developed by 12 bits that is security company and it does static analys to check the code and it's actually Implement clever static analysis to check for vulnerabilities uh I guess you see this is the application of slitter to uh a lot of basically very very simple contract taken from our website and you see all the red lines there are errors do you want to guess how many of them are real people not from Satur there are very few two of them nobody guessed okay there's zero

okay so the idea is actually these are errors that are reported by Static analysis tools but in fact because the tool and this is also what elel mentioned in the talk because the tool is not aware of what he's checking here the tool is actually reporting errors which are not real so why is static analysis not used in practice and and this is something that is is is being known by companies there are kind of two problem with static analysis one these are the errors that is missed and that's a bad thing and it could happen in SL and many other tools not in obscene but the other ones which I pointed out here is that many of the errors that are reported in fact

most of them from the studies that people done are actually false alarm they are not real errors so these are the two things that are kind of problematic but in fact I claim there is a another one which is even worse and this is what happened in the blockchain the idea is that the bus that were found and the bus which are prevented by the Sor approver they are not actually contract specific they take into account something which has to do with the meaning of the contract and it's basically checking the fact that you are doing a liquidation you're doing something which has to do with that so therefore if you apply this General static analysis the usage of it is limited so what we implemented in Sora we

implemented something that in the community called deductive verification but it doesn't matter if you want to call it whatever the idea is that you have the code in one hand and you have the specification on the other hand and the user has to write specification and we are trying to make specification natural like you're writing variance about your Cod and these are the things that you write about your code once you do them our tool can prove the property for you so it can prove that these invariant are maintained forever but more interestingly it can find rare buxs and it can find rare bus of the code before it's deployed it finds these violations of the

envirment so this is this tool you you have basically it's an automatic tool you think about it like a QA but it has the Environ and it checks that and it's it's static it statically analyze the code so uh in fact I'm not telling you the exact truth because what happened this is a problem which is a computationally hard which means that the computer cannot always prove this kind of environments so what happen is that our tool fails sometimes and this is actually where you have to do something and of course we are improving the technology but at the end our tool always can fail on some programs and and the user can do

something you can apply modularity you can apply many many techniques that if you want you can learn in the workshop about this technique uh why do it stop okay I just computed it so the interesting thing and that this is the most interesting thing that you can take from Sora in the last four years what we have been doing and new do is here is leading this effort we are actually writing interesting specification for Defi and I think this is the biggest value that we have to this community and of course it's a collaborative effort we

have it with our fantastic customer we are writing requirement and we are writing formal requirement at the moment for defi but for other things and of course you think of requirement this is something even if you're not a coder this is sort of a basic property going back to our Plateau but or or or aristol but the idea is it's coming from D that you have to write some properties of your C okay so for example the Cino always win it's an interesting property but more interestingly in the case of defi you have assets and you want to make sure that you have enough asset to cover your loan so this is something that you have to write as a human and this is what you do with the sover you write this in v as

a human so this is a simple Environ it's a very very simple property it says I have an erc20 Checker erc20 and what I want to check I want to check that the the total is equal to the sum of the balance this is a very basic property but even this basic property is not checked by the compiler currency and there are others the bank has enough money if we think of more clever properties so if you have LP tokens we heard about it you have a constant pool then you want to have some property that the the pool is constant so the the the multiplication of the two tokens is constant or another property is that if one of them is zero then the

other one is also zero so there cannot be the case that one of them is zero and the other one is not zero so these are properties that you have to write when you write with work with your with our tool and these properties are written by human and I checked by the machine so maybe I give you a trivial example everybody give this example I'll give it to you I'm sorry about it but there are a lot of more interesting example in our website so here is a transfer okay and you transfer a property and you you see that it it shows that we maintain the sum of the balance so that's a very simple example and we can mathematically prove that always maintain the sum of the balance so this is something that we can

do we can give you a formal proof the code is very simple oops what happen if you if you change it like if you have something that wait you get oops I want to show your a bug but I'm unable to show it it's okay so the idea is the tool can actually uh find bugs for you and the the the flow of the tool is fairly complex the tool actually Implement a lot of clever techniques that has been around in Academia for a long time okay so it's not so easy because this problem is computational hard we have to do a lot of things and we have to actually I mean you think about it I don't know if you

know like operating system or you think of system like C this is actually in four years we have implemented a fairly complex software which is a product and each this actually is is a full tool check it takes all the code and it actually checks the code from the source code into the bite code there's a clever abstract interpretation in mind there's a lot of smt in mind and actually a lot of these things that of course I have to to acknowledge our colleagues at Stanford University at at Microsoft all of these which are helping us in doing this thing and interestingly this tool checks the code which is executed so in fact we are the number one reported reporter of solidity bus because we find

these bugs by analyzing the code and by enforcing the invariance on the code and this is something that you can actually check there's a demo site and you can check it so maybe I give you uh just sort of give you the a kind of intuition what this kind of Technology can find so let's look at the most basic properties of economic which is solvency so what does solvency means it means everybody runs to the bank the bank can still pay the money so that's a very very simple property okay and here are the top protocols and this is code which is analyzed by the seror tool after the top

Auditors okay so basically the tool went to auditing the auditing came back the auditing flag some problems and the auditing said this is C is okay and these are the solvency issues which were found by the tool after the auditor and this of course you see here the menu of course this these boxs were found before the code was deployed but you see the total value which is saved if this because this these boxs were found before the code was deployed so how are we doing in terms of comparing to other tool I already mentioned static analysis so static analysis is complementary as we said it

finds some bugs but it actually Mis bugs we have also techniques like we heard about fuzzing so fuzzing is of course cheaper in terms of computation but it's actually just enumerating behaviors we are not enumerating behaviors we are basically doing an exhaustive checking of all the behaviors so we cover all the box that are found by exhaustive by by testing but we cover rare box which cannot be found by just random testing and in fact if you can see the box that found by our tool you can see that now of course a complementary technique is the human the auditor and the auditor can find BS after us too if we didn't write the right Environ the auditor would actually

miss so basically the auditor we'll find out some invar that we didn't check and then of course we update our tool we update our tool we we we we add this Environ so at least next time that you add this code we can we can check that so this is complimentary the human and the and the Machine they are complimentary so this is very very great basically we have a customer maybe they're here I'm not sure they call trash token or tofi are they here no so they but they are here in the conference I guess they are doing something else so what they did they took our tool and they basically manually inserted box and they want to see who who catches it whether it's the auditor whether it's

the tool and what you see here the tool CAU 12 bugs which actually everybody else missed you see also that the the to actually missed one bar because there were not the right property so this is a complementary where the human and the Machine together so I want to give you sort of a glimpse if you come to the workshop you see more but I want to give you a glimpse of how this tool works and I will get take you a very very complex code but very very simple Environ okay so the code is called Sushi trien is a constant pool it has about 2,000 line of solidity code our tool

actually analyzed the evm code which is much larger the interesting thing the tool actually the UN the tool actually finds bus that actually are very very hard to find with unit testing because in the code there are many many behaviors so I'm going to show you just one bug like this so the envar that is maintained is that if if one of the tokens is zero the other token is also zero so you see here you see Bob and Alis they both can deposit tokens and the beginning the bank is empty so you have zero tokens for A and B and then what happen B comes and deposit 100 tokens and then Ellis also deposit 100

tokens so basically they both have this these 100 tokens they they get some LP shares but it's not shown I'm not showing you so they get the lp shares this is all good and then there is another opportun operation which is possible it's a transfer is basically you are transferring 500 tokens so basically Ellis decided to transfer 500 token so you see here the bank has more money and you say what's the significance of it and it's it's just an operation nothing is is wrong here but what happened is now there is a bug in the code I'm not showing you the code the code is not big but it is complex and the code did not

use the right API and there is a bug in the code and you can look in our website and see that there is a bug in the code and because of this bug in the code Ellis now she Burns her holding and the result what happened after this operation you see that in fact the token a is not zero but the token B is zero so you see that now we broke this invariant we basically went from a state that satisfied the invariant into a state that violates the envir and you can see you can ask what's the sign ific of it and the significance of it is that now Ellis actually can swap the tokens and the bank is empty so

basically all the money is lost so this is the kind of bug that we are trying to prevent these are solvency issues and we are writing in variant in order to to to check solvency issues and then we have techniques that check that the code does not have the solvency issues and these are the things that we are doing with the envirment in the C so this is one error the other error is equally or even more interesting so one of the heiller or one of the best applications of defi is basically stable coins and the leader in stable coin is maker down they have the 10% and they

basically have this m uh stable coin they have been around for a long time and actually and basically what they have they have this stable coin but they also started I think about a year and a half ago they started using our technology and they integrated our technology into their build and every time they change the code they check it so and the code actually you know it carries significant amount of value so what happened and this is actually something that could the the of the developers in in in maker found basically found out that the basic invariant of the code is broken so one

of the functions can actually break break the basic Environ so basically the the the coin is not actually stable and this is something that was found it's a four year old so basically the the code is four year old and after four years this bug was was found and it was found by this technology so this is why you have this incentive to write envir in order to prevent situations like this so maybe I I'm kind of uh closing the talk I want to sort of give you uh several uh sort of lessons I learned I've been in this domain almost forever you can see and basically what happened is that I actually came to work in smart

contact because I realized it's actually one of the best application of formal methods because you have small with large value and and this is actually I sort of uh basically this is sort of an interesting domain for this kind of technology and because this technology is kind of well understood there are a lot of myth about this technology and I want to take this opportunity to explain them and maybe the biggest M about formal method is that formal method is about finding proofs it is of course true but formal method is about finding buxs and the most inter in usage of our application is that we are finding rare bugs before the code is deployed so this is sort of

the most interesting application of course you can get a guarantee but most interesting this is actually where the tool actually giving you surprising result you're finding some bad behaviors of your code by using this Environ so basically this is a a case that you have and maybe the second one which is also very when we talk about formal verification there are a lot of theorems in computer science like rise theorem or other that tell you that formal verification is a problem that can never be solve and they show you some things and I have myself work on decidability result these are of course true but in fact the biggest value and the biggest the hardest problem of formal

verification is actually coming up with a specification coming up with the requirement about the code and this is also what we are seeing basically we have to write these specifications of course in terms of Technology there also a lot of things that we have to do and this is where our tool implements a lot of things and this is where Satora innovates so the idea is that we are not modeling actually the exact machine we have an intermediate representation but we are actually have some ideas that we can forget we don't actually need to to actually model exactly what it is in order to find bugs and prove the objects and this is of course something very

fairly technical that I will have to explain but I'm happy to elaborate about it uh the other thing and that's has been known and we see it in our tool that in fact you don't actually need to analyze all the code at once and this is very very interesting in the case of defi because defi is composable by other things so what happen is we can apply modularity if your code is modular then of course also you will work with us and we we have a subscription model you will pay less because we actually can analyze your code in a simpler way so we actually can apply modularity in order to S side step the complexity of running

the code if you can break your code into several pieces this will make formal verification easier so that's important thing and maybe the the the last but I think not the least is that the biggest value of formal verification this is actually where defi are very interesting that it is not a onetime thing formal verification is actually very very useful when your code is changed so every time you change your code you write these Environ and then you have to check them every time you run the code so uh I'm basically want to tell you what's the takeaway here so I think the be best thing that you can learn

from Sor and from us and this is actually where we learn a lot that the is a very interesting domain for formal specification and sator is actually trying to contribute we also engage with the community you probably heard the talk by stani we have a a grant with a we basically give people money to give Ain variant and if you want to to join that please and actually there is a workshop there are other ways that you can contribute in varant and we are doing it with other protocol we're engaging the community and also with Auditors we are have partnership where people write Environ for us and basically of course they have incentive to write this envir so that's one thing and the other thing and this is

basically where I only hinted we have technology for checking the environment and we have three type of Technology one of them is the technology that I talk to you about is checking the code the other one which is very interesting it's led by Chandra nandi in our team it's a mutation testing tool it's a tool for checking the inv varant themselves are okay because for example we had one customer where basically they wrote in varant and they of course were audited and then somebody found a bug and guess what nobody accused the auditor they only accuse for formal verification and they are right usually when people have machines and human they tend to to to to say that the machines are Thea okay like

in automatic driver and other things so what we want to do and we are doing it we are actually checking the environs themselves and we can find out that for example one envir in this case is a topology so this means that the envir is actually independent of the code and we are doing it's a tool which is coming and the other tool which is coming and we have actually here you Val in the audience which is leading it is a dynamic tool we actually want to have a tool on the chain that finds the problems which are not detected before the code is is is a deployed so we want to have a tool that monitors and check the same or similar kind of rules when the code is deployed thank you very [Applause]

much thank you [Applause]