ethereum / oyente Goto Github PK

View Code? Open in Web Editor NEW

63.0 15.0 196.0 60.62 MB

The project has been moved to this new repo https://github.com/melonproject/oyente

License: MIT License

Python 100.00%

oyente's Introduction

Oyente

Note: The project has been moved to the new repo https://github.com/melonproject/oyente

Quick Start

A container with the dependencies set up and the blockchain snapshot installed can be found here.

To open the container, install docker and run:

docker pull hrishioa/oyente && docker run -i -t hrishioa/oyente

To evaluate the greeter contract inside the container, run:

cd /home/oyente/oyente && source ../dependencies/venv/bin/activate && python oyente.py greeter.sol

and you are done!

Dependencies

solc and disasm from go-ethereum
z3 Theorem Prover

Evaluating Ethereum Contracts

python oyente.py <contract filename>

And that's it! Run python oyente.py --help for a list of options.

Paper

The accompanying paper explaining the bugs detected by the tool can be found here.

Miscellaneous Utilities

A collection of the utilities that were developed for the paper are in misc_utils. Use them at your own risk - they have mostly been disposable.

generate-graphs.py - Contains a number of functions to get statistics from contracts.
get_source.py - The get_contract_code function can be used to retrieve contract source from EtherScan
transaction_scrape.py - Contains functions to retrieve up-to-date transaction information for a particular contract.

Benchmarks

Note: This is an improved version of the tool used for the paper. Benchmarks are not for direct comparison.

To run the benchmarks, it is best to use the docker container as it includes the blockchain snapshot necessary. In the container, run batch_run.py after activating the virtualenv. Results are in results.json once the benchmark completes.

The benchmarks take a long time and a lot of RAM in any but the largest of clusters, beware.

Some analytics regarding the number of contracts tested, number of contracts analysed etc. is collected when running this benchmark.

Known Issues

If you encounter the unhashable instance error, please add the following to your class AstRef(Z3PPObject): in /usr/lib/python2.7/dist-packages/z3.py:

def __hash__(self):
        return self.hash()

The latest version of Z3 does support this, but some previous version does not.

oyente's People

Contributors

Stargazers

Watchers

Forkers

oyente's Issues

No documentation on "Money concurrency bug"

The Oyente report generates an error for Money Concurrency Bugs, however no documentation exists outlining what behaviour causes this bug, or how to avoid it.

"Reentrancy bug" given for send()

Oyente will state there's a reentrancy bug on a line like msg.sender.send(this.balance), however send() is safe from reentrancy attacks as it limits the gas to 2300 if transferring to another contract. I believe only call() is vulnerable to reentrancy (as stated in https://github.com/ConsenSys/smart-contract-best-practices#reentrancy)

Handle all opcodes

At the moment, Oyente does not support a large fraction of existing EVM opcodes, but not all of them. Please check the main file symExec.py to see which opcodes are supported at the moment.

Testing our evm intepreter

There are existing tests built for evm virtual machines https://github.com/ethereum/tests/tree/develop/VMTests
We may use these tests to test the correctness of our vm implementation.

Division by zero

In the yellow paper, DIV and SDIV instructions return zero when the divisor is zero. Is this also the case in oyente?

Add more performance options

Add several options like:

Limit Memory Space
DFS depth limit
Gas-limit constraint
and so on

disasm not found

I think new ethereum release don't have disasm. Hence unable to satisfy the dependencies. Any help regarding this?

Refactor and optimize codebase

Currently, the codebase is very messy, hard to follow. It also lacks documentation.

Support ERC20 token contracts

Expand the transaction-ordering-dependence analysis to ERC20 token contracts to track the flow of tokens.

Integrate with the state of the Ethereum's blockchain

One way to improve the performance of the symbolic execution is to consider the existing blockchain state in the execution environment. For example, if a contract calls a function
a = contractB.getSomeData()
we can fetch the blockchain state to see what the value that contractB.getSomeData() would return and assign the value to a, instead of using a new symbolic value for a.

Dockerfile and upgrade

Can you add the Dockerfile for https://hub.docker.com/r/hrishioa/oyente/ to the repo? Link it on docker hub too if possible.

I'd like to make some changes to it.

Does not work for Solidity 0.4.12

When using any of the 0.4.12 compiler version and a corresponding pragma solidity ^0.4.12; I do not get any outputs regarding the checked issues, the result box is in fact empty:

oyente segmentation fault

When running oyente on https://github.com/ethereum-alarm-clock/ethereum-alarm-clock it fails with Segmentation fault when analysing contracts/Library/PaymentLib.sol

Tested on

0.2.7 release on OS X
enzymefinance/oyente@920fe9d on docker

Log from 0.2.7 OSX

oyente -s contracts/RequestFactory.sol 
WARNING:root:You are using an untested version of z3. 4.5.0 is the officially tested version
WARNING:root:You are using evm version 1.7.3. The supported version is 1.6.6
WARNING:root:You are using solc version 0.4.19, The latest supported version is 0.4.17
INFO:root:Contract contracts/IterTools.sol:IterTools:
INFO:oyente.symExec:Running, please wait...
INFO:oyente.symExec:	============ Results ===========
INFO:oyente.symExec:	  EVM code coverage: 	 90.7%
INFO:oyente.symExec:	  Callstack bug: 	 False
INFO:oyente.symExec:	  Money concurrency bug: False
INFO:oyente.symExec:	  Time dependency bug: 	 False
INFO:oyente.symExec:	  Reentrancy bug: 	 False
INFO:root:Contract contracts/Library/ClaimLib.sol:ClaimLib:
INFO:oyente.symExec:Running, please wait...
INFO:oyente.symExec:	============ Results ===========
INFO:oyente.symExec:	  EVM code coverage: 	 100.0%
INFO:oyente.symExec:	  Callstack bug: 	 False
INFO:oyente.symExec:	  Money concurrency bug: False
INFO:oyente.symExec:	  Time dependency bug: 	 False
INFO:oyente.symExec:	  Reentrancy bug: 	 False
INFO:root:Contract contracts/Library/ExecutionLib.sol:ExecutionLib:
INFO:oyente.symExec:Running, please wait...
INFO:oyente.symExec:	============ Results ===========
INFO:oyente.symExec:	  EVM code coverage: 	 100.0%
INFO:oyente.symExec:	  Callstack bug: 	 False
INFO:oyente.symExec:	  Money concurrency bug: False
INFO:oyente.symExec:	  Time dependency bug: 	 False
INFO:oyente.symExec:	  Reentrancy bug: 	 False
INFO:root:Contract contracts/Library/MathLib.sol:MathLib:
INFO:oyente.symExec:Running, please wait...
INFO:oyente.symExec:	============ Results ===========
INFO:oyente.symExec:	  EVM code coverage: 	 99.6%
INFO:oyente.symExec:	  Callstack bug: 	 False
INFO:oyente.symExec:	  Money concurrency bug: False
INFO:oyente.symExec:	  Time dependency bug: 	 False
INFO:oyente.symExec:	  Reentrancy bug: 	 False
INFO:root:Contract contracts/Library/PaymentLib.sol:PaymentLib:
INFO:oyente.symExec:Running, please wait...
INFO:oyente.symExec:	============ Results ===========
[1]    545 segmentation fault  oyente -s contracts/RequestFactory.sol

Steps to reproduce:

git clone [email protected]:ethereum-alarm-clock/ethereum-alarm-clock.git
cd ethereum-alarm-clock
oyente -s contracts/RequestFactory.sol

Handle loop better

At the moment, Oyente terminates a path when seeing a loop, and proceeds to other ones. In other words, our SE only explores an under-approximation of all the program symbolic paths.

It might be useful to note that there is a technical challenge regarding loops: statically analysing bytecode will result in unbounded loops. E.g. Array copy from data input will result in a loop, and statically we don’t know the size of the data input.