This is version of Securify is deprecated and will be no longer supported. Please use Securify v2.0.
It features an extensive list of security patterns commonly found in smart contracts:
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.
soufflebinary. As of writing, Soufflé is not available on Windows, so Securify should not be expected to run on Windows either.
solcbinary is required to be able to use Solidity file as input. Securify assumes that the right version is installed for the given file.
solcis available here.
To run Securify on a Solidity file:
java -jar build/libs/securify.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.jar -co out.json
To run Securify on some EVM binary (produced e.g. by
java -jar build/libs/securify.jar -fh src/test/resources/solidity/transaction-reordering.bin.hex
To see the full list of options:
java -jar build/libs/securify.jar -h
To run the tests (which use JUnit4):
A Python wrapper helps to deal with
truffle. The requirements are
in the requirements.txt file. The Dockerfile can be used as
a reference to set-up your local environment to use this wrapper.
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
--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
to obtain the full list of options. In particular, if the user wants to receive
compilation information from Truffle, he should add the
If one wants to receive JSON output, the docker supports a
--json flag that
will suppress the pretty output and return JSON instead. Make sure to add the
-q flag if no progress information should be displayed, hence resulting in
pure JSON output. 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.
Basic end to end tests can be run through the test.py file:
The requirements can be installed using Pipenv:
pip install -r requirements.txt
These tests compare the current json output given by Securify with some past output, and report differences between the two.
You can add the following
.travis.yml to your project to run Securify on new
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).
The output loosely follows the clang style. Only warnings and vulnerabilities
are reported. If one wishes to also get the compliance information, please use
--json flag in the docker, or
-co flag on the Java executable to get
all analysis information in JSON format.
Join our Discord to discuss with other users.
Although Securify is regularly used to help audits at ChainSecurity, there are still bugs, including:
computeBranchesbeing recursive. In most cases, it is enough to increase the stack size using the
java -Xss1G -jar ....
solc) are not supported
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.