HoRStify: Sound Security Analysis of Smart Contracts

TL;DR

HoRStify is a novel static analysis tool that provides the first sound verification of dependency-related security properties in Ethereum smart contracts, helping to prevent common vulnerabilities before deployment.

Contribution

It introduces a sound static analysis framework for verifying dependency properties in EVM bytecode, addressing a critical gap in smart contract security analysis tools.

Findings

HoRStify can verify absence of timestamp dependency attacks.

It is capable of analyzing real-world smart contracts efficiently.

The tool provides formal guarantees of soundness for dependency analysis.

Abstract

The cryptocurrency Ethereum is the most widely used execution platform for smart contracts. Smart contracts are distributed applications, which govern financial assets and, hence, can implement advanced financial instruments, such as decentralized exchanges or autonomous organizations (DAOs). Their financial nature makes smart contracts an attractive attack target, as demonstrated by numerous exploits on popular contracts resulting in financial damage of millions of dollars. This omnipresent attack hazard motivates the need for sound static analysis tools, which assist smart contract developers in eliminating contract vulnerabilities a priori to deployment. Vulnerability assessment that is sound and insightful for EVM contracts is a formidable challenge because contracts execute low-level bytecode in a largely unknown and potentially hostile execution environment. So far, there exists no provably sound automated analyzer that allows for the verification of security properties based on program dependencies, even though prevalent attack classes fall into this category. In this work, we present HoRStify, the first automated analyzer for dependency properties of Ethereum smart contracts based on sound static analysis. HoRStify grounds its soundness proof on a formal proof framework for static program slicing that we instantiate to the semantics of EVM bytecode. We demonstrate that HoRStify is flexible enough to soundly verify the absence of famous attack classes such as timestamp dependency and, at the same time, performant enough to analyze real-world smart contracts.