论文标题
使用固体器正式化和验证智能合约：有限的模型检查器固体性
Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
论文作者
论文摘要
对智能合同漏洞的开发可能会带来灾难性的后果，例如损失价值数百万英镑的加密资产。正式验证可以是确定漏洞并证明它们已被固定的有用工具。在本文中，我们使用坚实的语言及其区块链提出了牢固性和以太坊区块链的形式化。通过阐明/解除坚固的程序获得一个固体程序。我们进行了一些抽象，使坚固/以太坊的行为方式过高。基于此形式化，我们创建了巩固器：有限的模型检查器以实现固体性。它将固体转化为Boogie，这是一种中间验证语言，后来使用Boogie的有限模型检查器Corral进行了验证。与该领域的许多工作不同，我们不会尝试找到可能导致漏洞的特定行为/代码模式。取而代之的是，我们提供了一个工具来查找错误/不良状态，即程序所指出的不符合开发人员的意图。无论是否漏洞，都可以通过执行特定的已知代码模式或尚未预期的行为来达到如此糟糕的状态。
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that they have been fixed. In this paper, we present a formalisation of Solidity and the Ethereum blockchain using the Solid language and its blockchain; a Solid program is obtained by explicating/desugaring a Solidity program. We make some abstractions that over-approximate the way in which Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. It translates Solid into Boogie, an intermediate verification language, that is later verified using Corral, a bounded model checker for Boogie. Unlike much of the work in this area, we do not try to find specific behavioural/code patterns that might lead to vulnerabilities. Instead, we provide a tool to find errors/bad states, i.e. program states that do not conform with the intent of the developer. Such a bad state, be it a vulnerability or not, might be reached through the execution of specific known code patterns or through behaviours that have not been anticipated.
