智能合约的形式化验证方法  

Formal Verification Method of Smart Contract

作　　者：胡凯[1] 白晓敏[1] 高灵超[2] 董爱强[2] 

机构地区：[1]北京航空航天大学计算机学院,北京100191 [2]北京中电普华信息技术有限公司,北京100192

出　　处：《信息安全研究》2016年第12期1080-1089,共10页Journal of Information Security Research

基　　金：国家自然科学基金项目(91538202)

摘　　要：智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程,以支持规模化智能合约的生成.研究提出了一个应用于智能合约生命周期的形式化验证框架和验证方法,针对一个智能购物场景,采用Promela建模语言对智能购物合约进行建模,用SPIN进行了模型检测,验证了形式化方法对智能合约的作用.Smart contract is a code contract and algorithm contract and will become the basis of future agreements in digital society.Smart Contract utilizes protocols and user interfaces to facilitate all steps of the contracting process.This paper summarized the main technical characteristics of smart contract and existing problems such as trustworthiness and security and proposed that formal method is applied to the smart contract modeling,model checking and model verification to support the large-scale generation of smart contract.In this paper,a formal verification framework and verification method for smart contract in the whole life circle of smart contract has been proposed.The paper presented a smart shopping scene,in which Promela language is used for modeling a SSC（smart shopping contract） and SPIN is used to simulate and model checking to verify the effect of formal method on smart contract.

关 键 词：智能合约 形式化方法 建模 验证 SPIN模型检测工具 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]