Formal Analysis of Smart Contract Based on Colored Petri Nets
Duo Wang, Xin Huang, Xiaofeng Ma · IEEE Intelligent Systems · 2020
Smart contracts increasingly cause attention for its ability to widen blockchain's application scope. However, the security of contracts is vital to its wide deployment. In this article, we propose a multilevel smart contract modeling solution to analyze the security of contract. We improve the program logic rules for bytecode and apply the Hoare condition to create a Colored Petri Net (CPN) model. The model detection method provided by the CPN tools can show the full-state space and the wrong execution path, which help us analyze the security of the contract from several perspectives. The example shows that the counter-example path given by the contract model is accord with our expected results based on code analysis, proving the correctness of the solution. In addition, we design a highly automated modeling method, introducing custom call libraries and a path derivation algorithm based on backtracking, which improves the efficiency and pertinence of the dynamic simulation of CPN models.