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

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

Abstract

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

CLC Number:

TP391.9

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.

Figures/Tables 7

Fig. 1

Fig. 2

Fig. 3

Fig. 4

Table 1

Fig. 5

Fig. 6

References 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]	Duan Ting, Wang Weiping, Zhu Yifan, Wang Tao, Huang Meigen. Access Control Mechanism of UAV Cluster Based on Blockchain Smart Contract [J]. Journal of System Simulation, 2021, 33(11): 2656-2662.
[2]	Zhang Xiaohong, Sun Lanlan. Attribute Proxy Re-encryption for Ciphertext Storage Sharing Scheme on Blockchain [J]. Journal of System Simulation, 2020, 32(6): 1009-1020.
[3]	Zhang Zhili, Zhang Yunrong, Ma Shixin. Concurrent Conflict Control Method of "Multi-rights+Operation Queues" Based on CPN Tools [J]. Journal of System Simulation, 2019, 31(6): 1092-1100.
[4]	Zhang Yunrong, Zhang Zhili, Li XiangYang, Xu Weichang, Han Kuixia, Li Liang. Study on the matching mediation method between virtual maintenance personnel and work steps [J]. Journal of System Simulation, 2019, 31(4): 624-631.
[5]	Wang Yuhong, YangPu. Application of PWA-Based Safety Diagnosis Method in CSTR System [J]. Journal of System Simulation, 2018, 30(1): 292-297.