Mooly Sagiv - Tel Aviv University - Ethereum London

so I prefer that you ask questions during the top if you get I'm not going so I'm academic I come from a Nutella vivre University actually I've been in Imperial many times I have many colleagues here I'm also a visiting researcher at VMware and also we are starting a company called cetera I tell you a little bit about it so the business that we are interested is social application this is a an older mature area the idea is that the programmer has to define what is the required property and then we have a mechanism for formally proving that the code does what it's supposed to do and you can ask why verify smart contract it's probably an obvious question in this cloud by the way how many of you are coders maybe you can just raise hands good so so it's really hard to get the smart contract right and there are even those smart contracts are kind of simple and small program it's hard to get them right so this is the famous dau bug that you probably heard of that somehow there is a contract that and I will talk about it a little bit later so this is a kind of a very very simple bug that actually you can do attack there's other kind of problems or pieces and another case of bug which happens when you are when you updated a contract and and and so on and so forth and actually interestingly just recently this is another case and actually very similar to the Dow where actually these bugs happen and all of these bugs they are costly okay and they they really lead to loss of money but more than that they are kind of a barrier to trust because if you want to use the blockchain and you see these bugs they're actually kind of barrier to track so of course software verification is an old topic and getting software right is always hard but what happened usually in traditional software we get software right by evolution the first version is kind of not so okay but then the next version becomes better and so on but in the case of blockchain this is impossible because the moment you you upload the contract it's immutable so you really have to get it right from the start which is very hard and the slogan that you say is the code is the law so if you have wrong code you have wrong law and I like transactions which are done by the bank or other you cannot revert ones action look what happened with that once you have a bug it's actually the money is lost so the standard currently which is which is I guess kind of a bad eye for a best effort is the idea of auditing or code review that's lovely it's very important you grow and you order to call and you check its correctness and this procedure is very useful it can find box and it can find problems but it's expensive and it actually misses many bugs and it's not surprising it's like looking for a needle in the haystack there are so many behaviors in the program so actually finding that and we can show you that we run our tool after the audit opps and we find bugs which is not surprising because the procedure is not exhaustive another thing to notice about all the things that auditing actually is actually helped the centralization because you ended up actually relying on the audit or if you have a good auditor it's good but and and there are there are very few good auditor section so you actually make this you have the centralization so what we want to do in program verification that this has a huge history actually many of its starting in the UK that basically we want to take the system on one oops we want to take the system on one hand and we want to take the desired behavior on the other hand and we actually want to compare we want to check if there if there if the software adheres to the desired behavior and other we find a bug we find the situation of the program which are which are which indicate a bug oh here's a mathematical proof of correctness and this is again it go back to Turing actually is go back to very old old ideas in computer science but they are complete yes so we will see later in the talk but that's a very interesting question actually a biggest problem in computer science one of the biggest that there are many articles what is in the desire behavior and we'll show you I'll have some answer to that that's a very that's a great question but even if you can define the design behavior the idea is that from computational it's a computationally hard problem so in fact comparing this we have the required behavior to the desired behavior to the system is a hard question and the question how do we solve this hard question I'm going to talk a little bit about it in the talk and there are more material that I'll be happy to distribute so what we do at the company we are doing two things so we are hope we are hoping to do to fix one of them we actually develop technology the technology assume that you have some kind of a required behavior and we are and any text the code then we will give you a demo later but the idea is it compares and it finds arrows but in the end the interesting thing it's a technology which is exact in a sense that each of the arrows which are found are will and and in fact it can find all arrows okay so it's exhaustive technology and we can talk about it later and I will explain you why but the second thing that we do we address your question what's your name Graham we are to address gun question we are trying to define what is a required behavior and that's a very interesting question and we have partial answers for that okay so so one answer is that we have some generic properties we have some properties which are must be correct for all programs okay and these are the property that we check and I'll show you later something very interesting which is a generic property that we check and this property is not it does not guarantee correctness but for example it avoid the Dow it avoids many of the bugs so that's one thing that we do we contribute generic property here I say we I take credit actually this result is by Shelley Grossman she she's part of the company and actually this is this is her result and they are published in a paper in pop well this is a principle of programming languages you are welcome to find it and I can also send it to who is interest so we define what's correct and I should say by we the community define what's correct so for example GRC 20 is standard for meeting with new token so every time you meet a new token you check for example that the balances may take so these are generic properties but we can think of also of contact specific properties and this relies on the programmer to define them okay so something specific to the programmer for example I have a wallet and the wallet should have sufficient number of signers okay does it answer your question partially you can't you can actually define it in code you can define it in a set we will see later in the video you can also define it like like this kind of things we can actually automatically generate it from the from from kind of high-level specification okay more questions okay so we so far I should say the tool has not been released we will release the tool soon but we work actually with one customer which is lovely this is a company in San Francisco called compound finance what they are developing they are developing money market on top of material and they they actually we didn't give them our tool we basically Shelly and David deal with a professor from Stanford we would they took they took the English specification and they convert it into our tool and they run it and the interesting thing to notice that actually we find bugs and that's not surprising because in specially specifically we find corner cases we find cases which are really hard for human as expert as out to find and another thing perhaps which is interesting that actually there are some problems that they were worried about and we can show them since the technology is exhaustive we can show them that they can ever happen because we show them the in fact it satisfies the specification that they care about ok so I want to give you sort of an interesting idea of what is a correctness property for contract ok so here I'm going to be a little technical please stop me if it doesn't make sense so I want to define some kind of a correctness property for contract and this is a gender property the sense that I claim it is empirically that all reasonable contact have to satisfy that okay so I'm going to show you cold but hopefully it's not too bad so here is some code you see the blue code there is a red code and think about it it's like II tell you but I'm not showing you it's like if it will have it at any blockchain so this is the the look the blue code and the red code and interesting you see the blue code actually calls the red code this is this is kind of the situation that you can't have you can think of each of one of them as a contact okay and the interesting thing in the in the in the kingdom or in any blockchain that this is evolving system basically contact comes and go okay when I define a contract like for example the DAO later under which there can be another organization you see this is a contract written by FL and later on Paris IBM contributor country and later all you see Facebook actually change this red contract so all of this somehow this is an evolving system and we want to guarantee that it's correct so how do we do it look this is a very very simple code okay I have this model blue and there is this document and this document think about it for example it accept a and X suppose X is your balance and what it does if the if your balance is positive then it's document okay then and it's actually it's a very very simple code but it demonstrate the kind of a bug that happens in doubt and in other contracts okay and and this code looks like it's it's a benign code it looks like it's a reasonable code it's basically Church that something is is greater than a its locks it and that is that roommate okay and this looks like a reasonable code you would imagine that you can throw away the lobe okay because it doesn't matter the log is just log the value and it doesn't matter so we see that we prove this property X is greater than 0 here and now X is greater than 0 and greater and greater than a and this looks all good is it good does it guarantee that actually doesn't guarantee that we can always look at it independent of the other work is it guaranteed to be correct sorry so what so still going to be okay the ideas every time I check the value I check that it's X is greater than zero then a and I reduce it so it looks okay okay so it looks like I could drop the block but in fact it's not the case and that's exactly what happened in each area what happened is that look at this code I did this deck which calls low but low occasionally calls the deck what will happen in this code what will happen in this code so what will happen I will execute it and I'm showing the execution I start by x equals hundred okay and I'm showing you the execution of the program I'm showing you the stack of the program in the trace of the poem so so the blue the blue model executes the deck 100 this calls the red model which executes the log hundred now the red world will call back the blue so it's execute this deck 100 again okay and now the red the red model here called the log okay and it's Lea and it's now details and now when it returns you see it executes this actually this instruction here actually at X minus 8 so X becomes 0 and now if we go back we go back to the to the red red model we go back to the blue model and then once again we execute this instruction at line eight line L and the and the balance becomes negative so our one is lost okay our money is lost here and this is the looks like a weird situation by the idea is we have this back and forth cause that actually cost our money to be lost that's exactly what happened in the DAO at other cases so we want to prevent this kind of situation we don't want to have it because we want to have a code which is simpler to reason about okay that's what we want to do so you loop this is very strange X was a was greater than L before the log and after that X is no longer greater than it so something really strange happened it happens because of the callback because of the fact that Dec can call log and log can call Dec back okay and it's it's a it look like it's a weird situation but in fact it's a situation that it is actually required in detail please ask me questions if you want to clarify please ask me question okay so what do we do so in this paper we define a generic correctness property for all contract and we say a contract is effectively callback free if for every time wherever you have an execution which has a callback there is another execution without Colbeck or if you want to think about it intuitively what it means is that you don't have to worry about callbacks you can just ignore them and the ideas we want to make sure that any program that we write this is the case and this is nice because it will allow us to handle each of the contacts accurately my contact and your contract I can check their correctness separately so it's okay that the contract evolved over time and the interesting thing there are other tools syntactic tools that check these things but they have many false alarm we do not have false alarm I will show you this empirically every bug that we find at least now infinitely it is a real bug okay so let's again look into this thing so you see the problem in this model is that you see I have this call and call and this way I lost the money maybe I should ask you the code there how do you fix this code do you know how do you fix the code solidity program how do you fix the code what's the way to fix the code yeah so so one way is to get a tail call but that's not going to work all the time because in fact if you have many methods it's not a bitter cold but there is something weakened that you can do which will be enough here what you have to do there no no so that's that that's that's too restrictive because I'll show you that there are many many behavior that we need for that especially because we have local state so you could do that but that would be too restrictive the community will not accept it because there are many because you don't have think about it called back the implement kind of event or even programming so you do want to have the ability to have callback so the trick is what we have to do in this case we have to order the statement this statement X gets X minus a it must be executed before the log that's the only thing that we have to do to get it correct of course it's tricky but that's the only thing that we have to do we swap it together and one we spoke with it's okay and our tool basically we check your property and in fact it's of course you can write what property you want but if you don't we can check these generic properties okay yes sorry what do you say no so I'll show you later in the demo but the idea is what we have for the tool you have a set of user-defined you can you can define your property and there are predefined properties and you can select the predefined property from the list I'll show you very soon a devil hopefully maybe it would be clear okay so just to give you experiment actually this is in all data it should give you out so basically what we did we run this tool basically we run it on all the transaction in the blockchain because we are worried because maybe we have false alarm maybe we find behaviors which are flagged an arrow as arrows and they are not error but in fact this doesn't happen we check it empirically the interesting thing by the way that you see these are all the contract these are the number of callback they are quite pretty there are many callbacks but in fact the ones which violate our property they are all bugs so we do not have false alarm which is very nice usually if your syntactic tools the check your code they can be valuable but they have false alarm I should say our check is much more expensive but we do not have for setup okay so how does it work so basically what happened we have some of the contact development environment you right you're smart control you right the properties that you want and you fit it to our tool which we call sir Toa AEV it's a tramatic exact verification and it gives you a verification report of the properties which hold and it also gives you a test cases which indicate they are so it will automatically identify and I'll give you a demo it will automatically identify the input which leads to the error and the interesting thing this technique is fully automatic you just have to write the property the program and the property and you get the error and you don't actually all the else that you get are wheel in the fact that they lead to and in the lead to a case that the property is violated and also we do not miss her that's another property so we are actually solving a very very difficult problem in computer science so we are solving this problem and how does it work so the idea is in fact we don't work at the solidity level because we want to be agnostic to the programming language we take the programming for example if solidity we run it by the compiler and compiled into a VM awasum or other representation and then we feed it to the our tool and we find either a verification report or a test case by the way you do not have to trust that the verification that will report that we have it can be checked by another program and of course we can have bugs but the tools which will identify that ok so you can check the verification report that we produce yes because the idea is that we have and I'll show you later we have an exhaustive technology that summarized all the behavior of the code so in fact and basically the ideas that I should say when I say bug-free I should be more careful what I'm saying why Baxley I'm not necessarily saying that they are bug free I'm saying that the vet they satisfy the property that we define okay if you differ if you define the wrong property that's that's not I cannot help you there but when you define a property we check all the behavior that the elf the program would satisfy this property okay so for example you check that your X is greater than zero then we check that all behavior X is greater than zero yes it's not related to callback it could be look at the property related to callback is built in but you get the you can define your own property we will see that you can define your own property okay you can define your own property I'll give you more data yes more question please wonderful yes we will see in a second but the idea is to think about it that you write a set think about it that you write something in solidity that actually space specify like the property that you have sorry you usually usually checking the property so you're saying what happened if the property itself is incorrect that's what you're asking so the answer is if the property is incorrect you are lost kind of but in fact it's easier to to actually write in a show you with the wallet whatever it's much easier to define the property than defining the code I'll show you color coded bugs in the parity or whatever because the property that you define is actually define something like like what is happening and not how its implemented I'll show you that in fact it's easier to write an it so in our experience in so far it's not so bad you can define the property and defining the property you do not understand it to understand fully the code okay but of course it's the end of the day and there are also general poverty like ELC xx all of these guys the EFC 20 we take them from the community and there is actually they are defined they are actually definition by the community and we take them and we enforce these best efforts there was one more question but we are here to show you how easy it is to ensure the safety of your smart contracts using a new tool called Sartori Evie to be available soon bugs have terrible consequences especially in blockchain platforms the tool can help you ensure correctness and increase the trust in blockchain what is a Evie AEV stands for automatic exact verification it checks all possible executions of smart contracts but how can all executions be checked isn't there an infinite number of executions there is therefore Satori a Evie has an algorithm to exhaustively check all executions without explicit enumeration how does her Torah AEV work Satori a Eevee receives a contract which can be written in any programming language compiles it using standard compilers and analyzes all executions defined by the low-level instruction code against a set of expected properties a Eevee produces a report with all the properties which hold and test cases demonstrating bugs this way AEV provides you with definitive assurance that your contracts behave the way you intended them to behave what properties can be checked let's start with an example at any location in the contract code the user can declare a property which must hold in all executions that reach that location this code defines the effect of withdrawing coins the property ensures that the balance is correctly updated whenever the withdraw function is executed the above code violates this property so when the property is checked sir Torah AEV automatically identifies an input with the callback for which the property is violated the developer then corrects the code by reordering the lines and then run sir Torah AEP again the tool exhaustively checks all possible executions in the corrected code and reports that the property holds should I always write the properties myself No you can also select predefined properties from a list the list grows continuously as we add new properties based on standards and best practices from the community the user selects a property out of a list of useful properties for instance this list covers common vulnerabilities in smart contracts more information is available at www.geogebra.org check it because it I did you see the model checker are very good in finite state behavior and we do not assume finite state we actually reason about infinite state so we actually have so that's actually explained in the bottom of this slide but can I explain that too I go fast I don't actually know how to go there sorry Tony Hoare many of the figs actually were invented here but actually you see how we find so actually let's see this one box you see actually this is this is actually a wallet and you define this think and you see the tool actually I automatically identified actually it's it's it's actually inspired by a code which is a very which is executed now okay so maybe I'll I skip that I just want to tell you how do we so how do how do we check correctness so the idea is I Sophia so so the idea is that I see some recognized a yeah so the idea is we take the smart contract we take the front end and we actually generate a verification condition this is a formula that represents all behavior okay and this is actually a formalized overall it's sort of represent all behaviors and it actually is particular we are looking for behaviors which satisfy the semantics of the program and violate the property we are looking for some cases and then we feed it to con joints over there are many tools they are public domain actually we feed it to them and they either give us a solution which indicates a bug or I think that no solution which is a poop so here is a very simple program you see this program and basically it has few behavior and I want to check that X is equals to what so you see that the tool actually generates a formula that represents all behavior and then automatically and that's how we found a bug in the tool automatically we identify the input which leads to there so automatically we find that and once you fix the error we can actually generate the proof for you it's not going to be necessarily a pretty poof but it's a proof that you can check by a machine okay this makes a little more sense to you hopefully I can talk to you later maybe more questions yes yeah yeah yeah yeah ideally what we want to do we actually want to sit on the blockchain and every time you upload a new contract we want to check it and also every time you you you upload the new property you wanna check it backward on all the contact because maybe we don't know actually what property is checked and later on we can we get some report from the community and we want to check it so we want to make it like a tool that would be hopefully a continuous tool that you every time a contact is uploaded we check it and every time a new property is uploaded we also check it but at the moment it's a tool that works on a single control so it's actually depends on the size so far we have experience with medium-sized program and it takes seconds two minutes but when we go to larger one it's a hard computational problem I assume it could be ten minutes but it's still better than human medium in solidity is there is a thousand line I think right yeah that's what the yesterday that's what there are more authority extra than I am but I think that let's say a thousand line yeah Thank You Sofia yes yeah yeah yeah so one thing that we are thinking is just basically give this as a free tool for developer to just try it as a developing the environment and integrate it into remix and other environment so that you you run it and you check the property test development is is wonderful but the idea is here what it does it automatically identified for you test cases which violate the property and and an interesting thing that you do when you work with this kind of system and we of course we are not the original one day a lot of system like that you find out that sometimes you have a bug in the code and sometimes you have a bug in the property and when you have a bug in the property of course if the tool tell you that it doesn't virulence you understand in fact that you have a bug because for each of the code that we have when we tell you that the property holds it is guaranteed to halt okay so you some of the usage of this tool and this tool you can also use to do some other thing like first exploration or other things yes that's what we are trying to do there so they come in and explain to us how because that's exactly what we are trying to do we are trying to understand what is they that's why we we are damaged but we are trying to our understanding of businesses is a bit limited but this is exactly what we are trying to understand what will be the commercial value of such a tool so we're not going to do that with this this is not work we're not going to be it's nice to be Robin Hood but I don't think I think I lost my chance I'm too old for that so I don't think I can be Robin Hood maybe Shelli or the other we are younger guys in the tip it's nice to steal from the rich and going to the poor or whatever it makes sense but I'm not going to do it but you are absolutely right also I should say that when we find an input it's an input to the violator poppy for example in the doubt case but it's not necessarily input that you can use to steal the money but interestingly actually you can use this technology to help you there too but I'm not going to talk about so you actually could use this tool in a in a better way somehow to taste because when you find a bag you are you are looking for a case which is actually violate the property but maybe violate the property in a sense that you can for example maximize the number of things that you can steal perhaps or something like that yes and so the tool actually verified the byte code level we decided it's a design design decision that we will because a it's somewhat easier for us and B we don't want to trust the compiler but I should say that in fact in order to get meaningful errors when we find an error we actually do use the compiler in order to go back and give you that because we want to give you the error messages and the student fog for solidity so we do actually call the compiler and you actually we use data from the compiler in order to put to produce meaningful else yes sorry we have to check it and I will check it thanks a lot I will check it I'll check it thanks a lot so hopefully we are thinking of something two to three months to have a trial version that you can try probably this is an S ASM is something that you can just run your contract put it there and try but we are also looking for volunteers to work with us maybe send us contracts that we see the understanding especially if they are interesting contract it have something more interesting we are really happy to hear but we will release it to the public very