内容简介：胡凯教授本文将介绍基于模型检测形式化方法应用于智能合约辅助生成和验证的一个案例，便于大家了解相关的技术路线。作为形式化方法的工程实践，模型驱动工程（MDE）旨在提高程序规范中的抽象级别，从而提高程序规范中的抽象级别，通过使用可执行模型转换来增加程序开发中的自动化，较高级别的模型被转换为较低级别的模型，直到该模型可以使用代码生成或模型解释来执行。
胡凯教授
本文将介绍基于模型检测形式化方法应用于智能合约辅助生成和验证的一个案例，便于大家了解相关的技术路线。作为形式化方法的工程实践，模型驱动工程（MDE）旨在提高程序规范中的抽象级别，从而提高程序规范中的抽象级别，通过使用可执行模型转换来增加程序开发中的自动化，较高级别的模型被转换为较低级别的模型，直到该模型可以使用代码生成或模型解释来执行。
1、MDE方法工程框架
MDE可以支持智能合约的整个生命周期，从建模、验证、代码生成到一致性测试，应用于智能合约的形式化方法流程如图 1所示。
图1 智能合约的MDE方法流程
在模型驱动框架下，由于体系结构模型包含的系统特征和信息较多，一般不直接对体系结构模型进行验证和分析，而主要采用模型转换的方式，即将体系结构模型（或子集）转换到另一个形式模型，或者直接转换到模型检测 工具 或定理证明器，目的是为了重用这些已有的验证和分析能力。我们提出智能合约的模型检测工程化形式化方法框架如图 2所示。一个合约的生成包括：首先，用户提出需求，根据用户需求制定合约文本。然后对合约文本进行形式化描述，并选择合适的建模语言和建模工具对形式化规格说明文档进行建模和性质验证。其中，模型验证包括理论证明和模型检测，在模型检测中，我们通常使用模型转换来验证更多的性质。最后是一致性测试。为了证明合约代码与合约文本在性质和执行力是保持一致的，因此，需要对合约文本和合约代码进行一致性测试。这就是将形式化方法应用于智能合约完整生命周期的框架。
图 2 MDA形式化方法应用框架
2、智能合约的验证案例
我们使用Promela建模语言和检测工具SPIN来建立和验证一个互联网智能购物合约SSC（Smart Shopping Contract）的模型。
SPIN是一个通用的形式化验证工具，以严格的和大多数自动化的方式验证分布式软件模型的正确性。是一种著名的分析验证并发系统逻辑一致性的工具，以其简洁明了和自动化程度高而备受注目。SPIN已成功应用在安全协议验证、控制系统验证、软件验证及最优化规划等领域。作为一种形式化自动验证工具，SPIN可以提供：1）系统建模语言Promela（Process Meta Language），用于直观、明确地描述系统Promela模型规约，而不考虑具体实现细节；2）功能强大而简明的描述系统应满足性质（属性要求）的逻辑表示法；3）提供一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。除模型检测之外，SPIN还可以作为模拟器操作，遵循系统的一个可能的执行路径并且向用户呈现所产生的执行轨迹。
基本合约包括商品订货、分销和售后服务，合约可以组合和定制。
合约1: 货物订购与分配：
合约方：客户和商家
Contract goods_ordering_and_distribution (goods_information, payment, distribution)
Begin
IF goods are available AND pay is completed AND distribution is available
Inform merchant to send the goods to customer, set the terminator=timestamp + one week
ELSE
The transaction failed and returned the money to customer
Wait one week for the acknowledgment message from customer
IF acknowledgment message received
Pay to merchant and quit
IF TIMEOUT
The transaction failed and returned the money to customer
END
合约2: 售后服务合约:
合约方：客户和商家
Contract sale_after_service (item_information, payment, terminator)
Begin
While(timestamp Wait for the feedback message from customer IF merchant received message from customer SWITCH(message){ Case goods_return message: IF timestamp < terminator merchant wait for the goods IF merchant received the goods merchant return the money back to customer ELSE merchant reject and quit Case goods_exchange message: IF timestamp < terminator merchant wait for the goods IF merchant received the goods merchant send the new goods to customer Other: NULL } } Quit End
SSC应在用户订单之后触发，并且它具有两个参与者，即用户和商店。
智能购物合约的描述如下：当用户下订单时，他需要将购物所需的资金提交给智能购物合约，智能购物合约暂时持有资金。同时SSC启动两个子进程，用户进程和商店进程。用户进程：如果商家在七天内没有交货，用户将取消交易，SSC会将资金退还给用户，用户进程定时、周期地检测交货状态；商店进程：商家收到订单后，系统判断订单是否结束，如果订单没有超时，则商店发货。SSC需要确保资金的安全性和交易过程中各个状态的可达性。
我们可以简单建立SSC的Promela模型如下：
byte money=100
byte user_money=0
byte shop_money=0
byte day=0
bool isSend=false
ltl { <>isSend }
active proctype user() {
do
:: isSend -> atomic{
shop_money=100;
money=0;
break; }
:: (day>6)->{
user_money=100;
money=0;
break; }
:: else -> day=day+1;
od
:: }
active proctype shop() {
do
::(day<7)->isSend=true;
::break;
od
::}
init {
atomic{run user();run shop(); }
}
然后我们可以使用模型检测工具SPIN检测SSC模型，模型的模拟结果如4所示。从图4的模型仿真结果可以看出，一旦超时（day= 8），SSC将钱退还给用户。
图 4 模型模拟结果（超时退款）
如图 5结果所示，当商店在第二天送货时，SSC将钱转给商店。由于SSC是有限状态模型，通过对SSC的建模和验证，SPIN可以随机生成合约的所有状态，实验结果与合约的预期结果一致。
图5 模型模拟结果（交易完成）
基于这个案例，本文针对智能合约存在的可信与安全问题，将形式化方法应用于智能合约的生命周期验证，从形式化描述和形式化验证方法方面进行了详细的阐述。一个好的模型检测工具有助于检查和验证智能合约的各项属性。通过实例可以看出，智能合约可以在合约的不同节段获得不同的状态，当智能合约验证时，SPIN可以随机产生若干种不同的结果,形式化方法可以在智能合约的建立、验证和代码生成中得到重要应用，是智能合约可信和安全性的发展方向。
北京航空航天大学分布式实验室
北京航空航天大学分布式技术实验室具有悠久历史传承，是国内最早的分布式技术和形式化方法研究和应用的专业实验室，上世纪八十年代起就开始承担航空电子等各类军民两用分布式系统研制，先后承担国家基金、863重大、核高基等国家重点工程项目，获多项国家科技成果奖。在分布式处理、高性能计算、嵌入式、FPGA设计等方面国内领先。主编了国内分布式计算权威教材《分布式计算系统导论》，是国内区块链和智能合约技术早期研究单位，智能合约工程（SCE）和验证即服务（VaaS）等概念和理论方法的提出者。实验室与法国INRIA成立了形式化方法联合研究实验室，推动区块链和智能合约形式化验证方法和工具的应用。多年来潜心研究自有知识产权区块链底层技术，已拥有全系列区块链产品和工具，先后完成中国移动、国家网络应急中心、国家电网、金融领域等国内重要区块链应用落地项目，获得国家发明专利和软件著作权30余项。形成了科学研究与人才培养相结合，理论研究与应用系统研发协调发展的学科发展格局。
来源：北京航空航天大学分布式实验室--胡 凯
本文由布洛克专栏作者发布，不代表布洛克观点，版权归作者所有
——TheEnd——
关注“布洛克科技”
以上就是本文的全部内容，希望本文的内容对大家的学习或者工作能带来一定的帮助，也希望大家多多支持 码农网
猜你喜欢:
- 智能合约的形式化验证工具
- CertiK联合创始人顾荣辉：形式化验证 为智能合约实现100%安全 | 金色财经独家专访
- 引介 | 形式化验证 Gasper 共识机制的终局性
- 智能合约攻击分析之庞氏代币合约漏洞
- 检测了3万多份智能合约，这份白皮书找到了9大智能合约安全漏洞（附下载链接）
- 智能合约工程
本站部分资源来源于网络，本站转载出于传递更多信息之目的，版权归原作者或者来源机构所有，如转载稿涉及版权问题，请联系我们。
