计算机工程

作者：刘阳, 张圣杰

单位：上海海事大学 物流科学与工程研究院, 上海 201306

关键词：区块链,智能合约,时间自动机,UPPAAL工具,模型验证,映射规则

基金：新加坡-英国联合网络安全专项(EP/N020170/1); 国家自然科学基金(61303022)

区块链是一种去中心化的计算范式，在诸多领域具有良好的应用前景。智能合约是区块链应用的关键，然而，智能合约的安全问题时有发生，有些甚至造成重大的经济损失。为了避免智能合约在设计开发阶段出现由逻辑不严谨或错误逻辑所造成的安全漏洞，提出一种基于时间自动机模型的安全智能合约生成方法。相较于直接编写合约代码，该方法通过将证明为正确的模型转换为可执行的智能合约代码，有效解决在智能合约开发设计阶段所存在的安全性问题。利用UPPAAL工具将人类可理解的文本合约建模为时间自动机并通过模型验证来确保模型的安全性和可靠性。通过对智能合约的正式定义建立时间自动机与智能合约的映射规则，根据相应的映射规则，时间自动机被转换为模块化的Solidity智能合约代码。设计一个具体的商品预售活动案例进行分析，结果表明，通过所提方法生成的商品预售合约的Solidity代码可成功编译并部署在以太坊测试网络中。

来源：2023年第9期

《计算机工程》期刊编辑部

查看计算机工程杂志2023年第9期