/VeriSmart-public

a safety verifier for Solidity smart contracts

Primary LanguageOCamlOtherNOASSERTION

VeriSmart

VeriSmart is a safety analyzer for Solidity smart contracts. Currently, VeriSmart supports two types of analysis modes.

  • Safety verification (VeriSmart, S&P '20)

In this mode, VeriSmart can be used to prove the absence of bugs or detect bugs. The key feature in this mode is, VeriSmart automatically infers transaction invariants, which are conditions that hold under arbitrary interleaving of transactions, of smart contracts. With this ability, VeriSmart can precisely analyze safety properties (e.g., no integer overflows) in smart contracts.

  • Vulnerable transaction sequence generation (SmarTest, Security '21)

VeriSmart in this mode can be used to generate vulnerable transaction sequences (with concrete arguments for each transaction) that demonstrate the flaws. The key feature in this mode is, we guide a symbolic execution procedure with language models to find vulnerable sequences effectively. VeriSmart in this mode is called SmarTest.

VeriSmart has been developed and maintained by Software Analysis Laboratory at Korea University.

The benchmarks used in our papers (S&P '20, Security '21) are available here.

Installation

Dependencies

  • Install OCaml libraries below:
opam install -y conf-m4.1 ocamlfind ocamlbuild num yojson batteries ocamlgraph zarith
  • Install Z3:
wget https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1.tar.gz
tar -xvzf z3-4.7.1.tar.gz
cd z3-z3-4.7.1
python3 scripts/mk_make.py --ml
cd build
make -j 4
sudo make install
  • Install Solidity Compiler (solc).

Build

Clone this project.
chmod +x build
./build

Usage

You can check execution options by ./main.native -help.

Examples

  • Set verification timeout to 1 minute with -verify_timeout, and set Z3 timeout (per query) to 10 seconds with -z3timeout.
# -verify_timeout: specified in seconds (default: 5 minutes)
# -z3timeout: specified in milliseconds (default: 30 seconds)
./main.native -input CONTRACT.sol -verify_timeout 60 -z3timeout 10000
  • Specify a root contract with -main.
./main.native -input CONTRACT.sol -main ROOTNAME

Note that, if -main option is not provided, VeriSmart will assume the last contract in source code as a root contract.

  • Specify a solc version with -solc.
./main.native -input CONTRACT.sol -solc 0.5.11

Note that, in this case, CONTRACT.sol must be compiled with solc v.0.5.11, where the solc binary named solc_0.5.11 should be located at the path identified by which solc_0.5.11. If the -solc option is not explicitly provided, VeriSmart will attempt to compile the source code with solc binary named solc, located at the path identified by which solc.

  • To run SmarTest (vulnerable sequence generation mode), specify the mode with -mode.
./main.native -input examples/leak_unsafe.sol -mode exploit -exploit_timeout 10 leak

Note that the default mode is verification mode. You can also explicitly specify verification mode by providing -mode verify option.

  • Vulnerability types to be analyzed can be specified by their names (e.g., see the above example).

    • io (integer over/underflow), dz (division-by-zero), assert (assertion violation), leak (ether-leaking), kill (suicidal), re (reentrancy, only verification mode), tx (tx.origin, only verification mode), erc20 (erc20 violation, only exploit mode)

  • You can check the full list of available options by: ./main.native --help

Related Publications

For technical details of VeriSmart and SmarTest, please see our papers below.

Questions

If you have any questions, please submit issues in this repository, including a source code of your input Solidity contract (if relevant) and a command that can reproduce your problem.