eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts (artifacts)

This dataset contains the software and benchmarks accompanying the paper "eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts" (published at the ACM Conference on Computer and Communications Security (CCS) 2020).

ethor-sources.zip and horst-sources.zip contain the sources for our smart contract analyzer eThor and the HoRSt framework on which it is based.

ethor.jar and horst.jar are the compiled versions of eThor and HoRSt.

control-flow-reconstruction-tool.zip contains the sources for the tool used to reconstruct the control flows.

contracts.zip contains the contracts in the reentancy benchmark with redacted bytecodes (720 contracts). See below for unredaction.
contracts-with-reconstructed-control-flow.zip contains the non-trivial contracts in the benchmark contracts with reconstructed control flow and redacted bytecodes (605 contracts). See below for unredaction.
contracts-with-sources.txt contains the addresses of contracts in the reentrancy benchmark, to whose Solidity source code we had access to during assessment of the ground truth (601 contracts).
results.csv contains the classification of contracts and ground truth.

case-study-data.zip contains the data set for the functional correctness case study.

Provenance, Licenses, Recovery of Original Files

The software developed developed by the authors of this resource (ethor-sources.zip, horst-sources.zip and control-flow-reconstruction-tool.zip, ethor.jar, horst.jar) are licensed under GPL 3 or later.

All contract bytecodes in our benchmark were obtained from Ethereum Mainnet.

We redacted the bytecodes of the the smart contracts in our benchmarks due to licensing concerns. To obtain the file that we used for our experiements, first obtain the hex-encoded bytecode of any contract XYZ and place it next to XYZ.json in a file XYZ.hex.  Then executed

sed -i "s/REMOVED-DUE-TO-LICENSING-CONCERNS/$(cat XYZ.hex)/" XYZ.json

The bytecode for a contract XYZ can be, for example, obtained via etherscan, https://etherscan.io/address/XYZ#code (where XYZ has to be replaced with the actual address). Please note that all our tools ingest deployed/runtime bytecodes, not contract creation codes. Etherscan was also where we obtained the sources mentioned in contracts-with-sources.txt.

contracts.zip, contracts-with-reconstructed-control-flow.zip, contracts-with-sources.txt, and results.csv are distributed under CC0.

The addresses of the contracts in our benchmark were gathered from https://goo.gl/kFNHy3 (taken from "ZEUS: Analyzing Safety of Smart Contracts", NDSS '2018).

The solidity files in case-study-data.zip were derived from https://github.com/OpenZeppelin/openzeppelin-contracts/blob/9fdc91758dbd958a28a238a87c71b21e501a47c7/contracts/math/SafeMath.sol and are distributed under MIT.

Limitations on Reproducibility

The SMT-LIB files produced by eThor are not 100% deterministic, as the order of some statements is not fixed. This should not change the semantics of the respective file but may impact solver performance.