Azure 区块链智能合约的形式化规约与验证
编程语言
2019-04-30 v2
摘要
确保智能合约的正确性对于保障基于区块链系统的信任至关重要。本文研究了 Microsoft 企业级区块链即服务产品 Azure Blockchain Workbench 中智能合约的安全性与安全性。作为该研究的一部分，我们针对带有访问控制策略的状态机模型形式化了智能合约的语义一致性（semantic conformance），并开发了一个高度自动化的 Solidity 形式化验证器，能够生成证明以及反例。我们已将验证器 VeriSol 应用于分析随 Azure Blockchain Workbench 发布的所有合约，包括应用示例以及用于权威证明（PoA）的治理合约。我们在这些已发布的智能合约中发现了先前未知的漏洞。在修复这些漏洞后，VeriSol 能够成功地对所有这些合约执行完整验证。
引用
@article{arxiv.1812.08829,
title = {Formal Specification and Verification of Smart Contracts for Azure Blockchain},
author = {Yuepeng Wang and Shuvendu K. Lahiri and Shuo Chen and Rong Pan and Isil Dillig and Cody Born and Immad Naseer},
journal= {arXiv preprint arXiv:1812.08829},
year = {2019}
}
备注
13 pages