This repository is meant to be used as a submodule in existing projects.
An example project that makes use of this repository is smart-contract-analysis-tools-example.
$ git submodule update --init --recursive$ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
$ source ~/.bashrcCopy analysis-config-example.toml to the root of your project and update as required.
In this configuration file you can define the required paths for your project. You can also enable or disable different tools to run for the report generation.
After updating the configuration run the following command from your project root. Depending on which tools are enabled it can take from several seconds to an hour.
$ yarn --cwd < path to this security scanner root > run \
scan:generate-report \
< absolute path to repository root > \
< relative path from repo root to source project > \
< absolute path to config toml file >For example:
$ yarn --cwd ./ run \
scan:generate-report \
${PWD} \
./examples \
${PWD}/examples/analysis-config.tomlDISCLAIMER
It is important to remember that no tool on it's own will find all problems in your smart contract. Nor are all found problems actual problems.
We process the results from the tools to our best effort in order to give the most useful report.
No guaranties about the security of your contract can be claimed based solely on the report.
More information about the techniques used in the tools can be found in the analysis-techniques.md document.
Slither is a static analysis tool. It checks the code for several known problems when writing solidity code.
What is good about Slither is that in a very short time you get an idea of the quality of your code.
Mythril is a symbolic execution tools that tries to find problems linked to the SWC registry. When it finds a problems it tries to create a sequence of transaction that will lead to the found problem.
The SMTChecker is a tool that combines both a bounded model checker and a constraint Horn clause solver.
This tool is not available yet for the report generation. Some more needs to be done on this.
KEVM is an implementation of the EVM in the k-framework. The k-framework is based on matching logic.
While most tools don't require any user input other than some flags and the source files, kevm is different. For it to work you have to define for each function the expected state with optional pre- and postconditions. Additionally, sometimes you have to add custom rules for the analysis to work. Due to the manual changes required, the specifications for the contracts should be created outside of the submodule. The path to these specifications should be configured under the [kevm] section at kevm_spec_rel_path in the analysis.toml (here called ./analysis-config-example.toml) file.
The specification file MUST have the name <contract name>-spec.md. An example can be found at VeriToken-spec.md.
TODO: Currently updating
analysis.tomlfor kevm doesn't do anything. Instead, run the command below to run kevm.
From the root of the project repository that uses this as a submodule run the following command
$ yarn --cwd < path to scanner root > run \
scan:kevm \
< absolute path to repository root > \
< relative path to the security scanners folder from the repo root > \
< relative path to the project contracts folder from repo root > \
< relative path to the kevm specs folder from the repo root > \
< relative path to the foundry project folder from the repo root > \
< contract name without .sol >As an example:
$ yarn --cwd ./ run \
scan:kevm \
${PWD} \
./ \
./examples/src/smart-contracts \
./examples/kevm-specs \
./examples \
VeriToken