Sound static analysis for Ethereum smart contracts.
eThor is a sound static analyzer for EVM smart contracts based on HoRSt
You can get either build eThor from the latest sources (follow the instructions in
README.md) or download a precompiled jar.
The HoRSt framework, upon which eThor builds, it available here.
The tool used to reconstruct the control flow is available here.
Generate SMT-LIB files from contracts with reconstructed control flows
Given a contract with reconstructed control flow (such as the ones below, or the ones generated with the tool above) you can generate SMT-LIB files for z3.
sat result shows a potential reentrancy vulnerability.
java -jar ethor.jar --smt-out-dir=. --no-output-query-results --preanalysis --prune-strategy=aggressive --predicate-inlining-strategy=linear <input-file> z3 <input-file>.smt
The different options can be shown with
java -jar ethor.jar --help, the ones above are reasonable defaults.
Execute z3 directly from eThor
You can also execute z3 directly from within eThor, if a compatible
libz3.so is in
A simple way in Linux is to extend the
LD_LIBRARY_PATH environment variable with the directory containing
export LD_LIBRARY_PATH=<path-to-libz3>:$LD_LIBRARY_PATH # this step may be unnecessary java -jar ethor.jar --preanalysis --prune-strategy=aggressive --predicate-inlining-strategy=linear <input-file>
- contracts in the benchmark (720 contracts)
- non-trivial contracts in the benchmark contracts with reconstructed control flow (605 contracts)
- Solidity sources for the benchmarks, where available (601 contracts)
- SMT-Lib files generated for the experimental evaluation (42 MiB, 4.5 GiB uncompressed)
- classification of contracts and ground truth
- data set for functional correctness case study