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.
- 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).
Clone this project.
chmod +x build
./build
You can check execution options by ./main.native -help.
- 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
For technical details of VeriSmart and SmarTest, please see our papers below.
-
VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts
Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, and Hakjoo Oh
S&P2020: 41st IEEE Symposium on Security and Privacy
[paper] [video abstract] -
SmarTest: Effectively Hunting Vulnerable Transaction Sequences in Smart Contracts through Language Model-Guided Symbolic Execution
Sunbeom So, Seongjoon Hong, and Hakjoo Oh
Security 2021: 30th USENIX Security Symposium
[paper]
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.