智能合约设计遇上状态机综合：案例研究

现代区块链系统支持创建智能合约——托管并在区块链上执行的有状态程序。智能合约持有并转移大量数字货币，这使其成为安全攻击的有吸引力的目标。已有研究表明，部署到公共账本的许多合约包含安全漏洞。此外，区块链系统的设计不允许智能合约的代码在部署到系统后被更改。因此，在部署前保证智能合约的正确性十分重要。形式化验证被广泛用于检查智能合约相对于给定规范的正确性。在本工作中，我们考虑程序综合技术，其中规范被用于生成构造即正确的程序。我们关注程序综合的一个特例，其中程序用有限状态机（FSM）建模。我们展示 FSM 综合如何应用于自动智能合约生成问题。概述了几个智能合约案例研究：众筹平台、盲拍和许可合约。对于每个案例研究，我们用一组线性时序逻辑（LTL）公式指定相应的智能合约，并使用该规范与测试场景来综合该合约的 FSM 模型。这些模型随后被用于生成可直接在区块链系统中使用的可执行 Solidity 代码。