首页 | 本学科首页   官方微博 | 高级检索  
     

基于CPN的智能合约交易顺序依赖漏洞的验证
引用本文:郑红,刘泽润,黄建华,钱诗慧. 基于CPN的智能合约交易顺序依赖漏洞的验证[J]. 系统仿真学报, 2022, 34(7): 1629-1638. DOI: 10.16182/j.issn1004731x.joss.21-0208
作者姓名:郑红  刘泽润  黄建华  钱诗慧
作者单位:华东理工大学 信息科学与工程学院,上海 200237
基金项目:国家自然科学基金(61472139);产学研项目:区块链关键技术研究(H300-41819)
摘    要:智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究,而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象,分析合约中潜在的漏洞,自顶向下地对合约本身及其执行环境建立着色Petri网模型,并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞,最后基于Remix平台在以太坊网络中证实结论的正确性。

关 键 词:区块链  智能合约  着色Petri网  形式化验证  交易顺序依赖漏洞
收稿时间:2021-03-15

Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN
Hong Zheng,Zerun Liu,Jianhua Huang,Shihui Qian. Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN[J]. Journal of System Simulation, 2022, 34(7): 1629-1638. DOI: 10.16182/j.issn1004731x.joss.21-0208
Authors:Hong Zheng  Zerun Liu  Jianhua Huang  Shihui Qian
Affiliation:School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China
Abstract:The formal verification of smart contracts researches mainly focus on programming language-level vulnerabilities, and the transaction ordering dependence is more difficult to be detected as a blockchain-level vulnerability.The latent transaction ordering dependence vulnerability in smart contracts is formally verified based on colored Petri nets.The latent vulnerability in the Decode reward contractis analyzed, anda colored Petri net model of the contract itself and its execution environment is established from top to bottom.The attacker model is introduced to consider the situation that the contract is attacked. By running the model to verify the existence of transaction ordering dependence vulnerability in the contract,thecorrectness of the conclusion is finally verified in the Ethereum network based on Remix platform.
Keywords:blockchain  smart contract  colored Petri nets  formal verification  transaction ordering dependence vulnerability  
点击此处可从《系统仿真学报》浏览原始摘要信息
点击此处可从《系统仿真学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号