Event-B 中 Solidity 合约的形式化验证
软件工程
2020-05-14 v2
摘要
智能合约是区块链的产物，提供物理交易的不可变且可验证的规范。Solidity 是一种领域特定编程语言，用于定义智能合约。其旨在降低在诸如以太坊等分布式账本上执行合约所产生的交易成本。然而，Solidity 合约需要遵守安全和安保要求，这要求形式化验证与认证。本文提出一种方法，通过将 Solidity 合约翻译为 Event-B 模型来支持认证，从而满足此类要求。为此，我们定义了一个受限的 Solidity 子集以及一个将 Solidity 合约翻译为 Event-B 模型的转移函数。随后我们利用 Event-B 方法在不同抽象层级精化模型的能力来验证 Solidity 合约的性质。并且我们可以借助 Rodin 平台验证 Event-B 模型生成的证明义务。
引用
@article{arxiv.2005.01261,
title = {Formal Verification of Solidity contracts in Event-B},
author = {Jian Zhu and Kai Hu and Mamoun Filali and Jean-Paul Bodeveix and Jean-Pierre Talpin},
journal= {arXiv preprint arXiv:2005.01261},
year = {2020}
}