通过静态分析在以太坊智能合约中捕获重入攻击
Hunting for Re-Entrancy Attacks in Ethereum Smart Contracts via Static Analysis
摘要：
以太坊智能合约是在由点对点网络管理的基于共识的区块链中部署和执行的程序。近年来，已经发现了几种旨在窃取以太坊中使用的加密货币Ether的重入攻击，这些加密货币存储在部署的智能合约中。这种攻击的对策是基于执行智能合约本身的动态分析，但它需要花费以太币和提前分析攻击模式的知识。在本文中，我们提出了一个名为\textit{RA (Re-entrancy Analyzer)}的静态分析工具，它结合了符号执行和等价性检查，通过可满足性模理论求解器来分析智能合约对重入攻击的脆弱性。与现有工具相比，RA支持仅使用目标智能合约的以太坊虚拟机字节码来分析合约间行为，即，即使事先不知道攻击模式，也不消耗以太币。此外，RA可以在不执行智能合约的情况下验证是否存在重入攻击漏洞，并且不会提供误报和漏报。我们还提出了一个RA的实现，以评估其在分析部署的智能合约对重入攻击的脆弱性方面的性能，并表明RA可以精确地确定哪些智能合约是脆弱的。
英文摘要：
Ethereum smart contracts are programs that are deployed and executed in a consensus-based blockchain managed by a peer-to-peer network. Several re-entrancy attacks that aim to steal Ether, the cryptocurrency used in Ethereum, stored in deployed smart contracts have been found in the recent years. A countermeasure to such attacks is based on dynamic analysis that executes the smart contracts themselves, but it requires the spending of Ether and knowledge of attack patterns for analysis in advance. In this paper, we present a static analysis tool named \textit{RA (Re-entrancy Analyzer)}, a combination of symbolic execution and equivalence checking by a satisfiability modulo theories solver to analyze smart contract vulnerabilities to re-entrancy attacks. In contrast to existing tools, RA supports analysis of inter-contract behaviors by using only the Etherum Virtual Machine bytecodes of target smart contracts, i.e., even without prior knowledge of attack patterns and without spending Ether. Furthermore, RA can verify existence of vulnerabilities to re-entrancy attacks without execution of smart contracts and it does not provide false positives and false negatives. We also present an implementation of RA to evaluate its performance in analyzing the vulnerability of deployed smart contracts to re-entrancy attacks and show that RA can precisely determine which smart contracts are vulnerable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
