After several months of implementing, testing and refactoring, today, we are happy to announce the first beta release of Oyente, a symbolic execution based analyser for Ethereum smart contracts. This release is made possible with support and funding from Melonport AG. The release can be found on Github, and an online version is available at http://oyente.melonport.com/.
What is Oyente and how it works?
Oyente was part of a research project carried out at the National University of Singapore. The academic paper which reports Oyente was accepted in a major security conference last year, and a very early version of the tool was released soon after that. Oyente analyses Ethereum smart contracts directly at the EVM bytecode level to ascertain whether there are any bugs that could cause security issues. This means Oyente can work with all high level EVM languages, including Solidity, LLL, Serpent and Viper. Currently, Oyente is able to detect common and well-known bugs including reentrancy, transaction race, call stack limit and timestamp dependence bugs amongst others. Support for analysis of smart contracts such as token contracts is underway.
At a high level, Oyente explores all possible execution paths of a smart contract. For every path, Oyente checks if any possible bug is present, and flags the contract as anomalous if so. Oyente uses symbolic execution, a well known technique in programming analysis to symbolically represent the behavior of an execution path in a mathematical formula. Oyente then compares the newly generated formula of the execution path with the formulas that summarize the common bugs to see if the two can both be valid at the same time, i.e. the execution path is buggy. This methodology, if implemented correctly, is one of the most generic and cost effective approach to reason about security of computer program in general and smart contract in particular.
What are the changes since the initial open source release?
The Oyente team has made significant changes during for this beta release:
- Implemented unit tests for our symbolic EVM interpreter which symbolically reasons about the execution path at the bytecode level. We have found and fixed several bugs in the interpreter implemented in the initial release of Oyente.
- Support nearly all of the opcodes in the EVM, so we can cover all possible paths of the contracts. However, some opcodes are not possible to represent symbolically, e.g. DELEGATECALL, EXTCODECOPY and so on. For these opcodes, it makes more sense to add more context to analyse them precisely. That’s why we have enabled the next feature!
- We allow users to set the analysis environment, e.g. blockchain source, storage values, contract address and so on and so forth. This makes the analysis context-sensitive and reduces the potential for false positive results.
- Loops are handled well in this release. In the initial release, Oyente terminated the path whenever it encounters a loop. In this release, we allow users to specify the number of iterations that a loop can go, or just let it run as long as the gas limit allows.
- There are a bunch of features (e.g. gas tracking, limit depth of exploration and so on), optimizations, cleanups that we have done as well. You can check all the issues closed in the last 3 months to see how much effort has been put in.
What I can use Oyente for?
For non-technical users, Oyente can be used as it is to analyse any contract that you may wish to engage with! Oyente will inform you if there are any potential bugs that might cause you problems. While this is not a magical bullet, and CANNOT guarantee ultimate safety, we hope it will be used as a first safety-check for users before they interact with any contracts.
Oyente is of course also very useful for developers who wish to analyse their own contracts. It is always helpful to have a tool that checks your code, especially when you are new to a programing language like Solidity. Developers can also implement a new detection module for the a specific bug/ property that they want to check for in their contracts.
This has far reaching implications for anyone designing a smart-contract protocol. It allows to check for certain smart-contract specific properties that are in general not considered a bug but are within the context of the smart-contract protocol considered a security risk.
Imagine you’re using a smart-contract module in Melon — think of it as a smart-contract linked to another smart-contract. Oyente can now be modified to check whether this specific module does have opcodes for external calls — if it does it could be flagged as violating the guidelines of the Melon protocol and thus help enforce a security standard for Melon modules.
Another modified check could be to track all ERC20 token transfers and values thereof. Doing this for all possible execution paths can lead to something particularly close to a formal proof that ERC20 tokens cannot be transferred or siphoned off of a smart-contract in any unintended. This methodology can be applied to all Melon funds!
Another use case for Oyente is generating test cases for smart contracts with high coverage. The execution path exploration module in Oyente allows us to visit all possible paths, and generate corresponding inputs that drive the contract’s execution to these paths. One can run the generated inputs and check if the outputs are as expected to verify the correctness of their implementation.
Oyente has also been used by other researchers to detect bad coding patterns in a contract by leveraging the state exploration and symbolic execution engine in Oyente. We look forward to seeing their their detections being contributed to the main Oyente repository!
Next step?
There are several things we want to improve and add to Oyente. One direction is that, given the ubiquity of token contracts, we may support the analysis of ERC20 and token contracts. As mentioned in above example, the team aims to detect and track ERC20 token transfers and values thereof.
The other direction is to give more precise feedback to users. Currently Oyente only tells which bugs that the contract is potentially vulnerable to, and which execution traces (or paths) lead to the bugs. We plan to give better representation for the results (e.g. tell which line, which function of the source code may cause the problem) and produce some concrete input set for users to self-verify the reported bugs. We also aim to reduce the false positive rate by adding an new module to verify the report from the detection modules. If you are interested in working on any of these directions, please join the team on github!
Reminder: this is still a work in progress, so watch out for bugs! :)
We look forward to receiving feedback from our future users!
On behalf of the Oyente team,
Loi Luu
Loi Luu
Loi is a researcher working on cryptocurrencies, smart contract security and distributed consensus algorithms. Loi believes in the force of the Ethereum and Blockchain technology. Much of his work revolves around this community. Apart from Oyente, the first open-source security analyzer for Ethereum smart contracts, Loi also cofounded SmartPool, another open source project which embraces decentralization of mining pools in existing cryptocurrency. He continues to champion decentralisation and trustless properties of the Blockchain with the KyberNetwork project, taking inspiration and developing value for the community.
Github - https://github.com/loiluu
Twitter - https://twitter.com/loi_luu
