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.

翻译：以太坊加密货币是智能合约最广泛使用的执行平台。智能合约是分布式应用程序，管理金融资产，因此可以实现高级金融工具，例如去中心化交易所或自治组织（DAO）。其金融属性使智能合约成为有吸引力的攻击目标，针对流行合约的多次利用事件已造成数百万美元的财务损失。这种普遍存在的攻击风险凸显了对可靠静态分析工具的需求，这些工具可帮助智能合约开发者在部署前消除合约漏洞。对EVM合约进行可靠且富有洞察力的漏洞评估是一项艰巨挑战，因为合约在高度未知且可能充满敌意的执行环境中运行底层字节码。迄今为止，尚不存在可证明可靠的自动化分析器允许基于程序依赖关系验证安全属性，尽管流行攻击类别属于这一范畴。本文提出HoRStify——首个基于可靠静态分析的以太坊智能合约依赖属性自动化分析器。HoRStify将其可靠性证明建立在静态程序切分的形式化证明框架之上，我们将其实例化到EVM字节码语义中。我们证明HoRStify足够灵活，可可靠验证时间戳依赖等著名攻击类别的不存在性，同时性能足以分析真实世界的智能合约。