A sound static analyzer for EVM smart contracts based on HoRSt
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.
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
In order to simplify reproducing the results from our CCS 2020 submission, we provide a docker image:
This version incorporates fixes for bugs found by the SmartBugs team.
README.md for more details.
The parser of eThor assumes that the executable part of a contract only contains valid opcodes and treats all code starting from the first invalid opcode as (non-executable) metadata suffix.
Since eThor targets the Constantinople version of Ethereum (2019), the results for code targeting newer version will not yield the correct results if unsupported instructions are used in a contract.
To see if a contract uses such an instruction, run eThor with the
If the output contains lines similar to
18:20:32.621 [main] WARN wien.secpriv.ethor.ContractLexer - Integer 238 does not correspond to opcode! 18:20:32.621 [main] WARN wien.secpriv.ethor.ContractLexer - Encountered an unknown bytecode, skipping the subsequent after the byte...2
the results of the analyses should not be trusted, unless it is verified that the invalid opcode indeed appears in the metadata suffix.