Computer Science

Computer Science ›› 2023, Vol. 50 ›› Issue (6A): 220300220-7.doi: 10.11896/jsjkx.220300220

• Information Security • Previous Articles     Next Articles

Formal Verification of Supply Chain Contract Based on Coloured Petri Nets

ZHENG Hong1, QIAN Shihui1, LIU Zerun1, DU Wen2   

  1. 1 School of Information Science and Engineering,East China University of Science and Technology,Shanghai 200237,China;
    2 First Research Institute of Telecommunications Technology,Shanghai 200032,China
  • Online:2023-06-10 Published:2023-06-12
  • About author:ZHENG Hong,born in 1973,Ph.D,associate professor,master supervisor,is a member of China Computer Federation.Her main research interests include formal verifivation and blockchain.
  • Supported by:
    2019 Shanghai Informatization Development(Big Data Development) Special Fund Project(201901043).

PDF (PC)

276

Abstract: The security of smart contracts is particularly vital to the application of blockchain in the supply chain field.Currently,most of formal verification work on smart contracts focuses on vulnerability detection,and there is still relatively little attention to how to generate secure smart contracts before deploying them on chain,and there are difficulties in how to effectively and stan-dardly map the properties of specific fields to smart contracts.Therefore,this paper proposes formal specification of supply chain business logic based on coloured Petri Net(CPN) before writing contracts and constructing a two-layer simulation model with a graphical interface to describe transaction state changes for formal verification and state analysis,thus reducing logic vulnerabilities at the modeling stage.Finally,a conversion method from the CPN modeling language to contracts written in Solidity is provided to improve the security and reliability of smart contracts.

Key words: Smart contract, Formal methods, Model checking, CPN, Supply chain

CLC Number: 

  • TP311
[1]DHILLON V,METCALF D,HOOPER M.The DAO hacked[M]//Blockchain Enabled Applications.2017:67-78.
[2]STEINER J.Security is a process:A postmortem on the parity multi-sig library self-destruct[EB/OL].https://www.parity.io/blog/a-postmortem-on-the-parity-multi-sig-library-self-destruct.
[3]ATZEI N,BARTOLETTI M,CIMOLI T.A survey of attacks on ethereum smart contracts(sok)[C]//International Confe-rence on Principles of Security and Trust.Berlin:Springer,2017:164-186.
[4]ZHANG X H,SUN L L.Attribute Proxy Re-encryption for Ciphertext Storage Sharing Scheme on Blockchain[J].Journal of System Simulation,2020,32(6):1009-1020.
[5]JENSEN K,KRISTENSEN L M,WELLS L.Coloured PetriNets and CPN Tools for modelling and validation of concurrent systems[J].International Journal on Software Tools for Technology Transfer,2007,9(3):213-254.
[6]LI H,SUN T,WANG X R,et al.Testing the concurrent beha-vior of systems based on CPN[J].Computer Science,2016,43(1):218-225.
[7]The American PetroleumInstitute(API).Energy:Understanding Our Oil Supply Chain[EB/OL].https://www.api.org/-/media/Files/Policy/Safety/API-Oil-Supply-Chain.pdf.
[8]HIRAI Y.Defining the ethereum virtual machine for interactive theorem provers[C]//International Conference on Financial Cryptography and Data Security.Cham:Springer,2017:520-535.
[9]AMANI S,BÉGEL M,BORTIN M,et al.Towards verifyingethereum smart contract bytecode in Isabelle/HOL[C]//Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs.2018:66-77.
[10]NEHAI Z,PIRIOU P Y,DAUMAS F.Model-checking of smart contracts[C]//2018 IEEE International Conference on Internet of Things(iThings) and IEEE GreenComputing and Communications(GreenCom) and IEEE Cyber,Physical and Social Computing(CPSCom) and IEEE Smart Data(SmartData).IEEE,2018:980-987.
[11]WANG Y,LAHIRI S K,CHEN S,et al.Formal specificationand verification of smart contracts for azure blockchain[J].ar-Xiv:1812.08829,2018.
[12]KALRA S,GOEL S,DHAWAN M,et al.Zeus:Analyzing safety of smart contracts[C]//Ndss.2018:1-12.
[13]MORTENSEN K H.Automatic code generation method based on coloured petri net models applied on an access control system[C]//International Conference on Application and Theory of Petri Nets.Berlin:Springer,2000:367-386.
[14]PHILIPPI S.Automatic code generation from high-level Petri-Nets for model driven systems engineering[J].Journal of Systems and Software,2006,79(10):1444-1455.
[15]WANG D,HUANG X,MA X F.Formal analysis of smart contract based on colored petri nets[J].IEEE Intelligent Systems,2020,35(3):19-30.
[16]LIU Z,LIU J.Formal verification of blockchain smart contract based on colored petri net models[C]//2019 IEEE 43rd Annual Computer Software and Applications Conference(COMPSAC).IEEE,2019:555-560.
[17]DONG C Y,TAN L.Formal Validation of Auction Smart Contract Based on CPN Model[J].Journal of Chinese Computer Systems,2020,41(11):2292-2297.
[18]ZHENG H,LIU Z R,HUANG J H,et al.Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN[J].Journal of System Simulation,2022,34(7):1629-163.
[1] LIN Feilong, YUE Yuedong, ZHENG Jianhui, CHEN Zhongyu, LI Minglu. Blockchain-based Identity Authentication and Authorization Mechanism [J]. Computer Science, 2023, 50(6A): 220700158-9.
[2] YANG Xiaobo, GAO Haiwei, LIU Tianyue, GUO Binghui. Key Risk Node Identification Methods in New Energy Vehicle Supply Chain [J]. Computer Science, 2023, 50(6A): 221100052-7.
[3] CAI Ran, HUANG Pengpeng. Study on Product Recovery Model of Remanufacturing Enterprises Based on Game Theory [J]. Computer Science, 2023, 50(6A): 220300113-6.
[4] PEI Cui, FAN Guisheng, YU Huiqun, YUE Yiming. Auction-based Edge Cloud Deadline-aware Task Offloading Strategy [J]. Computer Science, 2023, 50(4): 241-248.
[5] LIU Zerun, ZHENG Hong, QIU Junjie. Smart Contract Vulnerability Detection Based on Abstract Syntax Tree Pruning [J]. Computer Science, 2023, 50(4): 317-322.
[6] WANG Zi-kai, ZHU Jian, ZHANG Bo-jun, HU Kai. Research and Implementation of Parallel Method in Blockchain and Smart Contract [J]. Computer Science, 2022, 49(9): 312-317.
[7] HUANG Song, DU Jin-hu, WANG Xing-ya, SUN Jin-lei. Survey of Ethereum Smart Contract Fuzzing Technology Research [J]. Computer Science, 2022, 49(8): 294-305.
[8] WU Gong-xing, Sun Zhao-yang, JU Chun-hua. Closed-loop Supply Chain Network Design Model Considering Interruption Risk and Fuzzy Pricing [J]. Computer Science, 2022, 49(7): 220-225.
[9] XU Jia-nan, ZHANG Tian-rui, ZHAO Wei-bo, JIA Ze-xuan. Study on Improved BP Wavelet Neural Network for Supply Chain Risk Assessment [J]. Computer Science, 2022, 49(6A): 654-660.
[10] FU Li-yu, LU Ge-hao, WU Yi-ming, LUO Ya-ling. Overview of Research and Development of Blockchain Technology [J]. Computer Science, 2022, 49(6A): 447-461.
[11] GAO Jian-bo, ZHANG Jia-shuo, LI Qing-shan, CHEN Zhong. RegLang:A Smart Contract Programming Language for Regulation [J]. Computer Science, 2022, 49(6A): 462-468.
[12] WEI Hong-ru, LI Si-yue, GUO Yong-hao. Secret Reconstruction Protocol Based on Smart Contract [J]. Computer Science, 2022, 49(6A): 469-473.
[13] ZHANG Ying-li, MA Jia-li, LIU Zi-ang, LIU Xin, ZHOU Rui. Overview of Vulnerability Detection Methods for Ethereum Solidity Smart Contracts [J]. Computer Science, 2022, 49(3): 52-61.
[14] ZHANG Bo-jun, LI Jie, HU Kai, ZENG Jun-hao. Distributed Encrypted Voting System Based on Blockchain [J]. Computer Science, 2022, 49(11A): 211000212-6.
[15] CHEN Qiao-song, HE Xiao-yang, XU Wen-jie, DENG Xin, WANG Jin, PIAO Chang-hao. Reentrancy Vulnerability Detection Based on Pre-training Technology and Expert Knowledge [J]. Computer Science, 2022, 49(11A): 211200182-8.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.