eThor
A sound static analyzer for EVM smart contracts based on HoRSt
Try eThor
You can 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.
A 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 java.library.path
.
A simple way in Linux is to extend the LD_LIBRARY_PATH
environment variable with the directory containing libz3.so
.
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>
Publication
The paper describing eThor is to be published at CCS 2020. A version including appendices is available here.
Data set
- 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
Update (2021)
In order to simplify reproducing the results from our CCS 2020 submission, we provide a docker image:
- docker image
- docker build files (includes usage instructions)
Talks
- CCS 2020: watch at youtube
- ISoLA 2020: watch at youtube
- Teaser: watch at youtube