TY - JOUR
T1 - Formal Analysis of Smart Contract Based on Colored Petri Nets
AU - Duo, Wang
AU - Xin, Huang
AU - Xiaofeng, Ma
N1 - Publisher Copyright:
© 2001-2011 IEEE.
PY - 2020/5/1
Y1 - 2020/5/1
N2 - 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.
AB - 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.
KW - Colored Petri Net
KW - Formal Analysis
KW - Model Checking
KW - Smart Contract
UR - http://www.scopus.com/inward/record.url?scp=85081392610&partnerID=8YFLogxK
U2 - 10.1109/MIS.2020.2977594
DO - 10.1109/MIS.2020.2977594
M3 - Article
AN - SCOPUS:85081392610
SN - 1541-1672
VL - 35
SP - 19
EP - 30
JO - IEEE Intelligent Systems
JF - IEEE Intelligent Systems
IS - 3
M1 - 9019834
ER -