Computer Engineering Commons^™

Verification Of Transaction Ordering Dependence Vulnerability Of Smart Contract Based On Cpn, Hong Zheng, Zerun Liu, Jianhua Huang, Shihui Qian

Journal of System Simulation

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 …