Building Your Ethereum Security Lab

This guide is a living work, subject to change and addition as time permits.
This guide heavily leverages Docker because containers are great.
This guide utilizes contracts from “Not So Smart Contracts“. 

In efforts to build up a at home lab these are the tools and techniques I’ve found, learned, and utilized to better understand the inner workings of Solidity Smart Contracts and the Ethereum Virtual Machine. 

Static Analysis

Static analysis is the analysis of computer software that is performed without actually executing programs. In most cases the analysis is performed on some version of the source code, and in the other cases, some form of the object code. 

https://en.wikipedia.org/wiki/Static_program_analysis
  • Oyente – An Analysis Tool for Smart Contracts
  • Surya – A set of Utilities for Exploring Solidity Contracts

Oyente – An Analysis Tool for Smart Contracts

Github: https://github.com/melonproject/oyente
Dockerhub: https://hub.docker.com/r/luongnguyen/oyente/

Oyente has a very quick “setup and scan” process because we’re provided with a docker image from the original developer. The github repository has the Dockerfile if you want to build it or the source code yourself. 

I prefer to pull down the image from dockerhub, if you do too, run the commands below. 

Next we want to make our smart contracts accessible to the container image by using the bind mount (-v <local_dir>:<mount_point>) flag of docker run. In the example below we use $(pwd) which will inline our current directory path where we have the contacts we want to evaluate, which will be mounted and accessible to the running container at /tmp/contracts

We can see from the output above some useful information about the smart contract. We were able to cover over 99% of the code and a potential bug was identified; an integer overflow bug which can be exploited under the discovered conditions.

Be sure to check out the many options oyente has to offer figure out what works best for you!

Surya – A set of Utilities for Exploring Solidity Contracts

Github: https://github.com/ConsenSys/surya

There is no docker image available for Surya but there is a very easy installation process via npm. Install it and then verify by checking the help.

If the install was successful and help menu displayed, you’re now equipped to use this tool as part of your arsenal.  Using the describe command shows a summary of the contracts and methods in the files provided.

Dynamic Analysis

Dynamic analysis is the analysis of computer software that is performed by executing programs on a real or virtual processor. For dynamic analysis to be effective, the target program must be executed with sufficient test inputs to produce interesting behavior. Use of software testing measures such as code coverage helps ensure that an adequate slice of the program’s set of possible behaviors has been observed.

https://en.wikipedia.org/wiki/Dynamic_program_analysis
  • Manticore – A symbolic execution tool for analysis of binaries and smart contracts.

Manticore – A symbolic execution tool for analysis of binaries and smart contracts

Github: https://github.com/trailofbits/manticore
Dockerhub: https://hub.docker.com/r/trailofbits/manticore/

The great folks at Trail of Bits offer both a docker image and Dockerfile for your setup ease. Pull it down and fire it up!

[..snip..]

You’ll find manticore to be feature rich, well documented and if you’re not familiar with symbolic execution then it’s an amazing introductory tool.

Definitions

Code coverage is a measure used to describe the degree to which the source code of a program is executed when a particular test suite runs. A program with high test coverage, measured as a percentage, has had more of its source code executed during testing, which suggests it has a lower chance of containing undetected software bugs compared to a program with low test coverage.

https://en.wikipedia.org/wiki/Code_coverage

Symbolic execution is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for inputs rather than obtaining actual input. It thus arrives at expressions in terms of those symbols for expressions and variables in the program, and constraints in terms of those symbols for the possible outcomes of each conditional branch.

https://en.wikipedia.org/wiki/Symbolic_execution