VeriSolid：面向以太坊的正确构造智能合约
密码学与安全
2019-01-23 v2 软件工程
摘要
基于区块链的分布式账本因其能在无可信实体情况下提供可靠性、完整性与可审计性而快速普及。这些新兴平台的关键能力之一是创建自执行的智能合约。然而，智能合约的开发在实践中已被证明易出错，因此部署在公共平台上的合约常充斥安全漏洞。这些平台的设计（禁止更新合约代码与回滚恶意交易）使该问题加剧。有鉴于此，在部署合约并托付大量加密货币之前确保其安全至关重要。为此，我们引入 VeriSolid 框架，用于对采用具严格操作语义的基于转换系统模型所规约的合约进行形式化验证。我们基于模型的方法使开发者能在高抽象层级推理并验证合约行为。VeriSolid 允许从已验证模型生成 Solidity 代码，从而实现智能合约的正确构造开发。
引用
@article{arxiv.1901.01292,
title = {VeriSolid: Correct-by-Design Smart Contracts for Ethereum},
author = {Anastasia Mavridou and Aron Laszka and Emmanouela Stachtiari and Abhishek Dubey},
journal= {arXiv preprint arXiv:1901.01292},
year = {2019}
}