基于模型检测的区块链智能合约公平性形式化验证  

Formal Verification of Fairness of Block Chain Smart Contract Based on Model Checking

作　　者：肖美华[1] 周浩洋 朱志亮 罗敏[2] Xiao Meihua;Zhou Haoyang;Zhu Zhiliang;Luo Min(School of Software,East China Jiaotong University,Nanchang 330013,China;Jiangxi Institute of Computing Technology,Nanchang 330003,China)

机构地区：[1]华东交通大学软件学院,江西南昌330013 [2]江西省计算技术研究所,江西南昌330003

出　　处：《华东交通大学学报》2021年第3期52-60,共9页Journal of East China Jiaotong University

基　　金：国家自然科学基金(61962020,61562026);江西省主要学科学术和技术带头人资助计划(20172BCB22015);江西省研究生创新专项基金(YC2019-S251);江西省青年科学基金资助项目(20202BAAL212006)。

摘　　要：随着第二代区块链平台及应用的爆发式增长,作为部署在区块链上可执行代码的智能合约面临越来越多的安全性问题。但是目前针对智能合约安全性问题的研究大多集中在对安全漏洞的挖掘,很少关注智能合约本身公平性对安全性的影响,对此提出一种基于模型检测的智能合约公平性验证方法。采用该方法对Puzzle合约的公平性进行验证,找到了一个已知的交易顺序依赖漏洞。结果表明提出的方法可以为发现智能合约中存在的漏洞提供新的思路。With the explosive growth of the second generation blockchain platforms and applications,smart contracts as executable code deployed in the blockchain are facing more and more security problems.At present,most of the researches on the security of smart contracts focus on the mining of security vulnerabilities,while insufficient attention has been paid to the impact of the fairness of smart contracts on security.To address this problem,a fairness verification method based on model checking is proposed,which is used to verify the fairness of Puzzle contract,and a known transaction order dependency vulnerability is found.The results show that the proposed method can provide a new idea for verifying the fairness of smart contracts.

关 键 词：智能合约 形式化方法 模型检测 交易顺序依赖漏洞 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]