Research Unit

eThor

Sound static analysis for Ethereum smart contracts.

image

About

eThor is a sound static analyzer for EVM smart contracts based on HoRSt

Try eThor

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