Oyente: Development update

[Music] Thanks good afternoon everyone my name is Laurie I'm a cooperative cable network a decentralized you know it changed for the cryptocurrency and tokens but today I'm not going to talk about Kaiba I'm going to talk well Oriente the work that I did before Khyber and Ont is now maintained and supported by melon pot right so what is int I think it's not working right right so what is int orient is a smart contract analyzer that you know based on symbolic execution so basically you know given a smart contract event a can just you know scan oh you know went through the contract and you know find all the possible vulnerabilities in your smart contract so we released the first version of int back into the 2016 you know with my team from National University of Singapore and I first present-oriented DEFCON two in Shanghai last year and after after my presentation Mellon port you know Rachel and they wanted to support the development appointee so and today o enter is available online at this URL if you are if you have your laptop with you you can check it out so here's a github URL Oriente as well is I mean Oriente still under active development so if you have you know you wanted to contribute feel free to go to github and start exploring right so first of all what is symbolic execution the techniques Baha'i Oriente so I will use a simple function here that you know get the bonus given some you know contribution amount in some token sale right so if the amount is like greater than hundred Eater then the bonus is 15% otherwise you know if the mouse is greater than 50 Eater then you get 10% bonus otherwise there's no bonus for you so if you look at this function there are three means there are three main branches in the entire function you know H is greater than 100 and you know H is greater than 50 and less than 100 and X is less than 50 eater so symbolic execution allows us to explore the possible parts of the program of your functions and it will record all the you know contract behaviors in its part right and it will summarize all the behaviors in something called a part condition here you will see that for every part we will have the condition for the input to drive the contract or the program to that part right so with this summer right part volition with this summer right heart condition we can we can easily check if some prob some property is violated so for example we can check whether if you know H is less than 50 and you know the bonus is still greater than zero so the way we do it is that we encode or the part condition and also the property that we want to check in some Terim proofing language and and you know we use some tour improver or server to check the feasibility right so we can check we can use the theorem provers over to check the feasibility of you know the you know property violation right so this is the main architecture int so our intake works with you know the EVM by code and it also detect the interim state into account so given the by code it will generate the control flow graph of the contract and if we use simpler execution to explore the possible part and you know for every part we will just analyze to see whether you know some properties violated and of course we use the theorems software here to check that and if if I want a flux and above then there is a validator component to check whether the buck is you know found positive on our so what is the main difference between int and you know other formal verification technique so Oriente basically you know try to find all the possible part in the program and see whether you know some buck or some property is violated on the other hand you know form of verification allows you to formally prove that you know if you know some the the correctness of some runtime property of your contract a program right so orient it doesn't orient it doesn't guarantee the the absence of some buck right it to say you know I have checked you know this many part in the program and you know these are the bucks that I found on the other you know eientei is easy to use and you know goes for most of the existing smart contract but for form of verification you know sometime you know it doesn't go automatically so maybe it requires some people like Joey or you know some other people's presenter to - you know configure the program and you know run it with a tool and right so what are the new features that we support in Oriente after the DEF CON presentation I will quickly walk through all of them so the first one that we support is you know checking the assertion violation in in the program so you know developers they you know sometimes they make some subtle mistakes right they are not even aware of that so for example this is a simple function that transfer the token from you know the sender to the receiver so any of you can detect you know the major problem in this function oh oh sorry this is this will be - sorry yeah right that so I can just quickly fix it but there's an right right sorry this is the naive but right there is more subtle but sorry what right this is another naive box sorry yeah um another naive buck mmm not really okay right so what happens if sender and receiver are the same so this guy can just you know print more token out of thin air right so this is really subtle and you know it happens in one of the contract that we have audited before so with int it can check you know the this you know if we add some assertion there and Oriente can check whether this assertion is violated before you even deploy the contract on the main air or test net so I can just quickly show you the demo right this is another no bug right so this is the the live version of int it's a you know oriented Melander network so you can just click to compile with right click to int and analyze Oh something's wrong sorry I get back to it later but you know right but basically you know you can with oriented you can shake you know whether some assertion is violated before you know you evenly deploy the contract to the manor or test net another another feature that we support is you-know-who loop handling so if you ever you know work with you know program and analysis you will know that you know handling loop is you know a nightmare right because basically you know loop can just force the analyzer to run forever and you know did make the program termination non-deterministic so this simple function here can just make you know eientei run forever because we have like no idea like what is the land here right what did the lands at the value X array X so in Oriente we handle loops in different ways so first of all we allow the user to specify the gasps limit so oriented we just keep exploring the program until the gasps limits is a rich we also like allow user to specify the number of iteration that they want they look to be to run right so here's the argument that you can use orient a user can also like specify the time out that they allow wanted to run so after that time I oriented with this you know stop another another thing that we added after the DEF CON to is you know making Oriente more dynamic so so when you when you analyze so Ont is based based on static a similar execution so that means we only care about the contract itself we do not care much about the environment outside of the contract right so for example if the contract cost another contract then we do not like analyze the the contract that you know this contract is calling so with Oriente we allows user to set up a customized blockchain or environment so you know so you know when this contract Co another contract then Oriente will go to that contract SQL and analyze it so this is how how you can specify the environment to work with Oriente so it looks complicated but basically you can specify the gas limit the difficulty of the block the channel data that you know you want to send to the function you can also specify the archive state including you know the balance and the storage of some of cloud so there are a bunch of new features that we are planning to air the first one is to generate all the test cases because you know Oriente visit order you know all the possible parts of the program right and it records all the behaviors of the program so it is possible for oriented to generate the corresponding input that drives the program to the same part so basically you can you know use all the other generated input as a test guy for your smart contract and use it in other framework like shuffle we also plan to like simply simplify all the constrain in the park condition so for example if you you have to condition like you know actually it's greater than zero and Isis small less than 2 then we can simplify it to you know X equal to 1 so that will reduce the term that we query the server or the theorem prover we also Li want to reduce the number of font positive reports in order to provide more helpful feedback to the developers so these are all the other new features that we are going to add in the in the near future right so with that I want to conclude my presentation again this is the URL to the github repo and eientei is available online these are automated developer volunteers that have you know been contributing to the project and again thanks to Mellon port for sponsoring and you know further supports over [Applause] [Music]