基于CPN的智能合约交易顺序依赖漏洞的验证

doi:10.16182/j.issn1004731x.joss.21-0208

系统仿真学报 ›› 2022, Vol. 34 ›› Issue (7): 1629-1638.doi: 10.16182/j.issn1004731x.joss.21-0208

• 仿真模型/系统置信度评估技术 • 上一篇下一篇

基于CPN的智能合约交易顺序依赖漏洞的验证

郑红(), 刘泽润, 黄建华, 钱诗慧

华东理工大学信息科学与工程学院，上海 200237

收稿日期:2021-03-15 修回日期:2021-04-26 出版日期:2022-07-30 发布日期:2022-07-20
作者简介:郑红（1973-），女，博士，副教授，研究方向为形式化建模、服务计算。E-mail：zhenghong@ecust.edu.cn
基金资助:
国家自然科学基金(61472139);产学研项目：区块链关键技术研究(H300-41819)

Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN

Hong Zheng(), Zerun Liu, Jianhua Huang, Shihui Qian

School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China

Received:2021-03-15 Revised:2021-04-26 Online:2022-07-30 Published:2022-07-20

摘要/Abstract

摘要：

智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究，而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象，分析合约中潜在的漏洞，自顶向下地对合约本身及其执行环境建立着色Petri网模型，并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞，最后基于Remix平台在以太坊网络中证实结论的正确性。

关键词: 区块链, 智能合约, 着色Petri网, 形式化验证, 交易顺序依赖漏洞

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.

Key words: blockchain, smart contract, colored Petri nets, formal verification, transaction ordering dependence vulnerability

中图分类号:

TP391.9

郑红, 刘泽润, 黄建华, 钱诗慧. 基于CPN的智能合约交易顺序依赖漏洞的验证[J]. 系统仿真学报, 2022, 34(7): 1629-1638.

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.

图/表 7

图1

图2

图3

图4

表1

图5

图6

参考文献 17

1	Wang S, Ouyang L, Yuan Y, et al. Blockchain-Enabled Smart Contracts: Architecture, Applications, and Future Trends[J]. IEEE Transactions on Systems, Man, and Cybernetics: Systems (S2168-2216), 2019, 49(11): 2266-2277.
2	Liu J, Liu Z. A Survey on Security Verification of Blockchain Smart Contracts[J]. IEEE Access (S2169-3536), 2019, 7: 77894-77904.
3	Hajdu Á, Jovanović D. Solc-verify: A Modular Verifier for Solidity Smart Contracts[C]// Working Conference on Verified Software: Theories, Tools, and Experiments. New York, USA: Springer, Cham, 2019: 161-179.
4	Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volume 1[M]. Springer Science & Business Media, 2013.
5	Bartoletti M, Pompianu L. An Empirical Analysis of Smart Contracts: Platforms, Applications, and Design Patterns[C]// International Conference on Financial Cryptography and Data Security. Sliema, Malta: Springer, Cham, 2017: 494-509.
6	Li X, Jiang P, Chen T, et al. A Survey on the Security of Blockchain Systems[J]. Future Generation Computer Systems (S0167-739X), 2020, 107: 841-853.
7	Rahimian R, Eskandari S, Clark J. Resolving the Multiple Withdrawal Attack on Erc20 Tokens[C]// 2019 IEEE European Symposium on Security and Privacy Workshops. Stockholm, Sweden: IEEE, 2019: 320-329.
8	Vujičić D, Jagodić D, Ranđić S. Blockchain Technology, Bitcoin, and Ethereum: A Brief Overview[C]// International Symposium Infoteh-jahorina. East Sarajevo, Bosnia and Herzegovina: IEEE, 2018: 1-6.
9	Eskandari S, Moosavi S, Clark J. Sok: Transparent Dishonesty: Front-running Attacks on Blockchain[C]//International Conference on Financial Cryptography and Data Security. St. Kitts and Nevis: Springer, Cham, 2019: 170-189.
10	Daian P, Goldfeder S, Kell T, et al. Flash boys 2.0: Frontrunning in Decentralized Exchanges, Miner Extractable Value, and Consensus Instability[C]// IEEE Symposium on Security and Privacy. San Francisco, USA: IEEE, 2020: 910-927.
11	Zaki M H, Tahar S, Bois G. Formal Verification of Analog and Mixed Signal Designs: A Survey[J]. Microelectronics journal (S0026-2692), 2008, 39(12): 1395-1404.
12	Bhargavan K, Delignat-Lavaud A, Fournet C, et al. Formal Verification of Smart Contracts: Short Paper[C]// 2016 ACM Workshop on Programming Languages and Analysis for Security. New York, USA: Association for Computing Machinery, 2016: 91-96.
13	胡凯, 白晓敏, 高灵超, 等. 智能合约的形式化验证方法[J]. 信息安全研究, 2016, 2(12): 1080-1089.
	Hu Kai, Bai Xiaomin, Gao Lingchao, et al. Formal Verification Method of Smart Contract[J]. Journal of Information Security Research, 2016, 2(12): 1080-1089.
14	陈强军, 张明清, 孔红山, 等. 基于CPN的信息系统安全防护能力建模方法[J]. 系统仿真学报, 2018, 30(10): 3699-3709, 3716.
	Chen Qiangjun, Zhang Mingqing, Kong Hongshan, et al. Modeling for Security Protection Capability of Information System Based on CPN[J]. Journal of System Simulation, 2018, 30(10): 3699-3709, 3716.
15	宋小庆, 陈永星, 朱昀炤, 等. 基于有色Petri网的MiLCAN网络仿真与性能分析[J]. 系统仿真学报, 2013, 25(增1): 95-98, 103.
	Song Xiaoqing, Chen Yongxing, Zhu Yunzhao, et al. Simulation and Performance Analysis of MiLCAN Network Based on Coloured Petri Net[J]. Journal of System Simulation, 2013, 25(S1): 95-98, 103.
16	Liu Z, Liu J. Formal Verification of Blockchain Smart Contract Based on Colored Petri Net Models[C]// Annual Computer Software and Applications Conference. Milwaukee, USA: IEEE, 2019, 2: 555-560.
17	董春燕, 谭良. 基于CPN模型Auction智能合约的形式化验证[J]. 小型微型计算机系统, 2020, 41(11): 2292-2297.
	Dong Chunyan, Tan Liang. Formal Validation of Auction Smart Contract Based on CPN Model[J]. Journal of Chinese Computer Systems, 2020, 41(11): 2292-2297.

攻击发起者	Winner
无	1`{id=1,reward=1}
合约拥有者(id=0)	1`{id=1,reward=0}
其他用户(id=2)	1`{id=2,reward=1}

[1]	黄海涛, 刘勤明, 叶春明, 陈翔. 基于区块链技术的政府采购合同融资博弈分析[J]. 系统仿真学报, 2021, 33(8): 1947-1958.
[2]	段婷, 王维平, 朱一凡, 王涛, 黄美根. 基于区块链智能合约的UAV集群访问控制机制[J]. 系统仿真学报, 2021, 33(11): 2656-2662.
[3]	张小红, 孙岚岚. 属性代理重加密的区块链密文云存储共享研究[J]. 系统仿真学报, 2020, 32(6): 1009-1020.
[4]	张志利, 张云荣, 马世欣. 基于CPN Tools的“多种权限+操作队列”并发冲突控制方法研究[J]. 系统仿真学报, 2019, 31(6): 1092-1100.
[5]	张云荣, 张志利, 李向阳, 徐卫昌, 韩奎侠, 李良. 虚拟维修人员与工步等级匹配调解方法研究[J]. 系统仿真学报, 2019, 31(4): 624-631.
[6]	郝莉莉, 顾浩, 康凤举, 杨惠珍. 不确定条件下AUV编队决策系统的WIFTCPN形式化建模[J]. 系统仿真学报, 2015, 27(8): 1740-1746.

基于CPN的智能合约交易顺序依赖漏洞的验证

Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 7

参考文献 17

相关文章 6

编辑推荐

Metrics

本文评价