# Making Smart Contracts Smarter - Oyente - Loi Luu

- Speakers: [Loi Luu](https://streameth.org/speakers/loi-luu)
- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2017-10-09
- Duration: 11:46
- Topics: blockchain, smart contracts, distributed ledger
- Watch: https://streameth.org/watch/yt-bCvh6ED-cj0
- YouTube: https://www.youtube.com/watch?v=bCvh6ED-cj0

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/2/making-smart-contracts-smarter-oyente

The contract analyzer OYENTE was built to detect vulnerabilities in smart contracts and will soon be released as open source. This presentation will give an overview of Oyente and how it can me used to make smart contracts smarter.

Speaker(s): Loi Luu
Skill level: Advanced
Track: Developer Infrastructure
Keywords: progress, security, vulnerability, bugs, challenges, contributions, dependency

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 2 was held in Shanghai, China on Sep 19 - 21, 2016.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

okay cool so today I'm going to talk about a recent project in smartphone check security namely eientei making smart engage smarter to see the joint project with my team from NUS and yo and us college so okay so we all know that programming security is hard because especially for you know complex program because your system or your program may have you know multiple components and the adversary or the attacker can choose you know to attack you know any component and to exploit your system so that's well you know people say security can be no stronger than its quickly you know component so programming smart CQ smart conjecture is even harder because because of several reasons so I myself you know smartphone jackass on short programs because you have only cha only one chance to make it right once you deploy it you know it's really hard nearly impossible to you know change it if if you find any flaw in the you know contract and secondly you know the execution model of this mark inject is a little bit different it is executed by the consensus model running on the blockchain and the third reason is a you know we use new language with a little bit we we have a pretty much similar to the existing language so often people you know make some assumption about the language which exists in JavaScript and Python but do not exist in solidity and answer pen so that's why you know we have seen a lot of you know problem in our smartphone checks for example you know the Dow with our tree engine see work you know eater dies with a gas problem can you be thrown with the same you know instruction so the question that we asked before we started our project is you know others others buffs that we don't know you know you know existing platform and secondly you know how many smart contracts are there are vulnerable so surprisingly you know the number of smartphone checks is increasingly it post it potentially starting from you know 2015 so right now we have roughly 120,000 smartphone jars and we want we really want to quantify you know among these con smartphone choice how many of them are vulnerable so there are several challenges first of all you know contract costs are not always available see see what we see when we write a smart contract but what is eventually stall on the blockchain is a binary code which is compiled from the high level code and you know you can use some disassembler to you know to translate the binary code into the by code but it's still really hard for you to make any sense of this and secondly we have so many smart contracts to and analyze and you know if we have someone really good who can you know read the bytecode is still you know takes them several years to analyze all the 120,000 smartphone charts so what we contribute in this project is first of all we identify new smartphone check box namely generation Auto independence and tons time dependence and we talk about them shortly second we introduce Oriente the new the analyzer for smart contracts which is beyond simply execution so eientei can detect all the popular box including the known and their new ones so we one oriented with almost 20,000 smartphone charts and we were able to flag you know roughly night of Zen of them as for narubu okay so what is generation order independence so I will use a simple smartphone check to Allah to illustrate this problem so here we have the the puzzle solver contract break you know allows the owner to set up some puzzle and you know anyone can and and then he deposit some ether so that anyone can submit the solution for the Paso to collect the reward and you know if the owners see that the prewar is a little bit low and the pizzoli is so hot so so he can update the reward to attract more more uterus so now let's consider this scenario where you know some users submit the the a solution would include their some of the same generation would include a solution to the to the contract so some miners they include the generation in in his block and then the submit solution is trigger the others received the reward if his solution is correct so this is totally fine but let's consider this scenario where you know we have the owner saying a different generation at the same time to update that we were to 0 so now the miners can you know see like a set of generation in his block and he can freely decide which generation to include and which an adjacent to it know and which order between the generations so for some reasons he includes the generation which update the reward first and then the submit solution generation later so now there appear reward is executed first and the Ballon is set to zero and then the submit solution generation is executed now although the you to submit submitted a correct solution he still get 0 reward for his solution but he's unfair so the problem in this generation are independent dependence Bob is a you know they're the state that the the either observed when he when he submit the generation is different from the actual state of the smartphone check when the connection is executed and this can be a you know coincidence because you know to generation can happen at the same time or the term right but it can be a malicious scenario because you know if the owner saw the targeted generation from the victim which includes a you know correct solution for the puzzle he can you know on second letter saying a different Chanin to abate the reward and now the to generation until enter the race and you know the owner has some non zero probability of winning the race so that's it for their generation or independence next thing you can spend time stem dependence so we know that interim allows this mark on check to access the block times time within the contract and really we we have seen two main use case of these thumbs them first people use the thumbs them as a random seed to generate the random number and secondly they use the timestamp to to simulate the real time and the problem with with with these two Eve's case is that you know the tough stem can be many manipulated and the miners they can vary their block times them to you know the value of weight by us them so they can totally buy out the output of the execution to their benefit you know either in both of their use cases so in our papers we propose the solution for both of their problems so I think you can take a look at the paper you are interested next I will talk about int their analyze analyze that for smart contracts so here's a high-level architecture of int which is based on symbolic execution so eientei takes the bike or as an input and then based on the bike code we generate the control flow graph and from the control flow graph we pass it to the simple Explorer and we will explore the possible part of the program so for every part that we can explore we we said we forgot it to the core analysis which will be take whether the part of the program we detect whether the part has some you know prop some problem that we want to be take and if there is we will forward to the result to the validator to validate whether the the Rizal is positive so a little bit more about symbolic execution so this is our control flow graph we will visit every single execution choice at the program so given some input X we will you know collect all the part condition which eventually we essentially summarize or the execution characteristic of that part and for example we want to check this property whether Z is equal to X plus 2 with us you know most other condition together into one which simplex formula and the rest is used to ask whether there exists any instant of the input that satisfies this formula so in order to answer this question we send the formula to the theorem prover which ec3 in int and this theorem prover we say whether there exist input or not and if there is it will generate an example for us so what can orient they do Oh aunt they can detect but in existing smart contracts as Isis described and we run eientei with you know almost 20,000 smart contracts back in May 2016 and we were able to detect all the popular box back then this is the number of box for each category and second orion taken you can be used to prove the test generation because symbolic execution allows us to cover all the possible paths of each program understand we can based on that path we can generate one example input that drives the smartphone check to that I secrets in part and I thing is open source business really believes it two days ago you can go to that to that github repo - you know clone to and contribute to the project there are a lot of future work that that we can do to improve their you know performance and functionality of their project us for example we can support more of course right now we discover you know a large fraction of the EVM of code but not all of them we can also handle the loops precisely or we can combine you know static or dynamic a simple execution to reduce a rate of fun positive so with that I want to conclude my presentation thanks thank you very much light