Security Scanner for Ethereum Smart Contracts
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.

README.md

Securify

securify

Securify is a security scanner for Ethereum smart contracts supported by the Ethereum Foundation and ChainSecurity. The core research behind Securify was conducted at the ICE Center at ETH Zurich.

scan now

It features an extensive list of security patterns commonly found in smart contracts:

  • some forms of the DAO bug (also known as reentrancy)
  • locked ether
  • missing input validation
  • transaction ordering-dependent amount, receiver and transfer
  • unhandled exceptions
  • unrestricted ether flow

The project is meant to be an open platform welcoming contributions from all of the Ethereum Security Community. To suggest new patterns, to volunteer for testing or to contribute developing new patterns please get in touch through our Discord group.

Getting Started

Requirements

  • Soufflé: https://github.com/souffle-lang/souffle/releases (Securify should work with the latest package, please raise an issue if it does not). If you cannot install Soufflé, look at the Docker container for an alternative. Securify will crash without the souffle binary. As of writing, Soufflé is not available on Windows, so Securify should not be expected to run on Windows either.
  • Java 8
  • A solc binary is required to be able to use Solidity file as input. Securify assumes that the right version is installed for the given file. solc is available here.
  • Linux users must have the timeout command, OS X users must have the gtimeout command, which can be install with brew install coreutils.

Use

To build:

./gradlew jar

To run Securify on a Solidity file:

java -jar build/libs/securify-0.1.jar -fs src/test/resources/solidity/transaction-reordering.sol

To run Securify on the decompilation output provided by the pysolc.py script (which requires py-solc):

java -jar build/libs/securify-0.1.jar -co out.json

To run Securify on some EVM binary (produced e.g. by solc):

java -jar build/libs/securify-0.1.jar -fh src/test/resources/solidity/transaction-reordering.bin.hex

To run the tests (which use JUnit4):

./gradlew test

Docker

The installation should be simple enough on Debian derivatives, or any other platform supported by Soufflé.

For a quick demonstration which does not require Soufflé, you can use Docker.

Build the Docker image:

docker build . -t securify

Run Securify on a small example:

docker run securify

You can change the files analyzed by specifying a volume to mount, and every *.sol file contained will then be processed by Securify:

docker run -v $(pwd)/folder_with_solidity_files:/project securify

Adding a --truffle flag should allow Securify to run over Truffle project in which dependencies have already been installed (so run npm install before if need be). Without this flag, the project is compiled using solc. Add a -h to obtain the full list of options.

The indices of the lines matched are 0-based, meaning that a match to line i means that the i+1th line is matched. In particular, the first line has an index of 0.

Travis

You can add the following .travis.yml to your project to run Securify on new commits:

services:
  - docker

before_install:
  - docker pull chainsecurity/securify

script:
- docker run -v $(pwd):/project chainsecurity/securify

This should allow Securify to run over Truffle project in which dependencies have already been installed (so run npm install before if need be).

Output

The output is a in JSON and gives the vulnerabilities found over the files analyzed and the corresponding line numbers.

Contributing

See CONTRIBUTING.md.

Join our Discord to discuss with other users.

Known Limitations

Although Securify is regularly used to help audits at ChainSecurity, there are still bugs, including:

  • the code in the fallback function is currently not analyzed. A workaround is to name this function instead.
  • in some cases, a StackOverflowError exception is thrown, due to computeBranches being non tail-recursive (but recursive). In most cases, it is enough to increase the stack size using the -Xss option of java, e.g. java -Xss1G -jar ....
  • libraries are not properly supported
  • abstract contracts (whose binary cannot be obtained via solc) are not supported

Presentations, research, and blogs about Securify

Technical details

Securify statically analyzes the EVM code of the smart contract to infer important semantic information (including control-flow and data-flow facts) about the contract. This step is fully automated using Soufflé, a scalable Datalog solver. Then, Securify checks the inferred facts to discover security violations or prove the compliance of security-relevant instructions.

The full technical details behind the Securify scanner are available in the research paper.