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

Update (2021)

In order to simplify reproducing the results from our CCS 2020 submission, we provide a docker image:

Update (2023)

This version incorporates fixes for bugs found by the SmartBugs team. Check README.md for more details.

Known Limitations

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 -v option. 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.

Talks