Formal Analysis of Smart Contract Based on Colored Petri Nets

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.