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

Authors

Hong Zheng, School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China;Follow
Zerun Liu, School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China;
Jianhua Huang, School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China;
Shihui Qian, School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China;

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.

Recommended Citation

Zheng, Hong; Liu, Zerun; Huang, Jianhua; and Qian, Shihui (2022) "Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN," Journal of System Simulation: Vol. 34: Iss. 7, Article 23.
DOI: 10.16182/j.issn1004731x.joss.21-0208
Available at: https://dc-china-simulation.researchcommons.org/journal/vol34/iss7/23

First Page

1629

Revised Date

2021-04-26

DOI Link

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

Last Page

1638

CLC

TP391.9

Recommended Citation

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