基于Dafny的智能合约演绎验证
计算机科学中的逻辑
2022-08-08 v1
摘要
我们提出一种开发已验证智能合约的方法论。我们在易于验证的语言Dafny中编写智能合约及其规约与实现。在我们的方法论中，编写规约、实现以及对正确性进行推理是首要关注点。我们针对具有外部调用的合约推理问题，提出了一种简单、简洁而强大的解决方案。这包括任意重入，而重入是智能合约中缺陷与攻击的主要来源。尽管我们尚无从Dafny到EVM字节码的编译器，但在Dafny代码上获得的结果可合理假定在Solidity代码上成立：Dafny代码到Solidity的翻译是直接的。因此，我们的方法可立即用于开发和部署更安全的合约。
引用
@article{arxiv.2208.02920,
title = {Deductive Verification of Smart Contracts with Dafny},
author = {Franck Cassez and Joanne Fuller and Horacio Mijail Anton Quiles},
journal= {arXiv preprint arXiv:2208.02920},
year = {2022}
}