基于CPN的供应链合约的形式化验证

doi:10.11896/jsjkx.220300220

计算机科学 ›› 2023, Vol. 50 ›› Issue (6A): 220300220-7.doi: 10.11896/jsjkx.220300220

基于CPN的供应链合约的形式化验证

郑红¹, 钱诗慧¹, 刘泽润¹, 杜渂²

1 华东理工大学信息科学与工程学院上海 200237;
2 电信科学技术第一研究所上海 200032

出版日期:2023-06-10 发布日期:2023-06-12
通讯作者: 郑红(zhenghong@ecust.edu.cn)
基金资助:
2019年度上海市信息化发展(大数据发展)专项资金项目(201901043)

Formal Verification of Supply Chain Contract Based on Coloured Petri Nets

ZHENG Hong¹, QIAN Shihui¹, LIU Zerun¹, DU Wen²

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).

摘要/Abstract

摘要： 智能合约的安全性对于区块链在供应链领域的应用尤为重要。目前,大多数对智能合约的形式化验证工作集中于漏洞检测,对于如何在部署上链前生成安全的智能合约的关注仍然比较少,如何有效规范地将特定领域的属性安全地映射为智能合约代码存在难点。因此,提出在编写合约前基于CPN(Coloured Petri Net)对供应链业务逻辑进行形式化规范并构建双层仿真模型,以图形化界面描述交易状态变化,进行形式化验证和状态分析,从而在建模阶段就减少逻辑漏洞。最后,提供了一种从CPN建模语言到Solidity编写的合约的转换方法,以提高智能合约的安全性和可靠性。

关键词: 智能合约, 形式化方法, 模型检查, CPN, 供应链

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

中图分类号:

TP311

郑红, 钱诗慧, 刘泽润, 杜渂. 基于CPN的供应链合约的形式化验证[J]. 计算机科学, 2023, 50(6A): 220300220-7. https://doi.org/10.11896/jsjkx.220300220

ZHENG Hong, QIAN Shihui, LIU Zerun, DU Wen. Formal Verification of Supply Chain Contract Based on Coloured Petri Nets[J]. Computer Science, 2023, 50(6A): 220300220-7. https://doi.org/10.11896/jsjkx.220300220

参考文献

[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.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于CPN的供应链合约的形式化验证

Formal Verification of Supply Chain Contract Based on Coloured Petri Nets

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0