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.
翻译:智能合同是用来管理金融资产的分散应用软件,因此可以实施先进的金融工具,例如分散的交易所或自治组织(DAOs ) 。 其金融性质使得智能合同成为具有吸引力的攻击目标,正如大量利用广受欢迎的合同造成数百万美元的财务损失所证明的那样。这种无处不在的攻击危险促使需要完善的静态分析工具,帮助智能合同开发商在部署之前消除合同脆弱性。对EVM合同来说是健全和深刻的弱点评估是一项艰巨的挑战,因为合同在基本未知和潜在的敌对执行环境中执行低层次的字码。迄今为止,没有一种可感知的自动分析器,使得能够根据方案依赖性来核查安全性质,尽管普遍的攻击类别属于这一类别。在这项工作中,我们介绍HOST(HERS)智能合同依赖性的第一个自动化分析器,根据健全的静态分析,将它的准确性证据用于一个静态程序的正式证据框架,即我们立即进行精确的SEV-M(S)级,从而证明我们不具有足够的精确的可靠性。