论文标题
与达夫尼的智能合约的演绎验证
Deductive Verification of Smart Contracts with Dafny
论文作者
论文摘要
我们提出了开发经过验证的智能合约的方法。我们在验证友好的语言dafny中撰写智能合约，其规格和实现。在我们的方法论中，编写规范，实施和理论正确性的能力是主要问题。我们为有关具有外部呼叫的合同的推理提出了一个简单，简洁而有力的解决方案。这包括任意重新进入，这是智能合约中错误和攻击的主要来源。尽管我们还没有从DAFNY到EVM字节码的编译器，但我们可以合理地假定在DAFNY代码上获得的结果可以符合坚固的代码：DAFNY代码将其转换为坚固性很简单。结果，我们的方法可以轻松地用于制定和部署更安全的合同。
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.
