基于Event-B的可靠智能合约自动生成方法

doi:10.11896/jsjkx.220800134

计算机科学 ›› 2023, Vol. 50 ›› Issue (10): 343-349.doi: 10.11896/jsjkx.220800134

基于Event-B的可靠智能合约自动生成方法

朱健¹, 胡凯^2,3, 王军¹, 李洁^2,3,4, 叶亚飞³, 时希言⁵

1 中国电子科技集团第十四研究所南京210039
2 北京航空航天大学计算机学院北京100191
3 北京航空航天大学云南研究院昆明650233
4 北京物资学院信息学院北京101149
5 北京化工大学经济管理学院北京100029

收稿日期:2022-08-15 修回日期:2023-01-12 出版日期:2023-10-10 发布日期:2023-10-10
通讯作者: 叶亚飞(yeyf@bhynii.com)
作者简介:(zhujian@buaa.edu.cn)
基金资助:
北京市自然科学基金(M22040);云南省重大科技专项(202103AN080001-001,202102AD080006)

Reliable Smart Contract Automatic Generation Based on Event-B

ZHU Jian¹, HU Kai^2,3, WANG Jun¹, LI Jie^2,3,4, YE Yafei³, SHI Xiyan⁵

1 The 14th Research Institute of CETC,Nanjing 210039,China
2 School of Computer Science and Engineering,Beihang University,Beijing 100191,China
3 Yunnan Innovation Institute of Beihang University,Kunming 650233,China
4 School of Information,Beijing Wuzi University,Beijing 101149,China
5 School of Economics and Management,Beijing University of Chemical Technology,Beijing 100029,China

Received:2022-08-15 Revised:2023-01-12 Online:2023-10-10 Published:2023-10-10
About author:ZHU Jian,born in 1997,master,assistant engineer.His main research intere-sts include formal methods and smart contract.YE Yafei,born in 1982,master,engineer.Her main research interests include blockchain and smart contracts.
Supported by:
Natural Science Foundation of Beijing,China(M22040) and Science and Technology Major Project of Yunnan Province(202103AN080001-001,202102AD080006).

摘要/Abstract

摘要： 智能合约是一种以代码的方式执行合同条款的可计算交易协议,其应用场景与规模日益增长,承载着多达数十亿美元的各类资产。由于其代码缺陷可能会造成严重的经济损失,因此智能合约的可信开发成为技术关键。为此,提出了一种基于集合论语言Event-B的智能合约可信验证与自动生成方法。Event-B方法是一种基于精化的形式化方法,可用于规约、设计和验证软件系统。通过对智能合约的模型验证和可执行代码的自动生成技术,研发了自动转换工具EB2S,打通了形式化模型和智能合约编程语言的语义鸿沟和技术壁垒。最后,选取典型的在线支付智能合约场景,应用基于Event-B的智能合约模型自动生成合约代码,验证了EB2S转换工具的有效性。

关键词: 智能合约, Event-B方法, 自动代码生成, Solidity合约, 定理证明

Abstract: Smart contract is a new computable transaction agreement that executes contract terms in code.Its application scena-rios and scale are growing with each passing day,carrying up to billions of dollars of various assets.However,smart contracts may cause serious economics losses due to code defects.Therefore,the trusted development of smart contract is particularly critical.This paper proposes a method of trusted verification and automatic generation of smart contracts based on the set theory language Event-B,which is a formal method based on refinement and can be used for specification,design and verification of software systems.Through the model verification of smart contracts and the automatic generation technology of executable codes,an automatic conversion tool EB2S is developed,which bridges the semantic gap and technical barriers between formal models and smart contract programming languages.Finally,this paper selects a typical online payment smart contract scenario,and the smart contract design and verification method based on Event-B is applied to automatically generate the smart contract code,which verifies the effectiveness of the conversion tool.

Key words: Smart contract, Event-B method, Automatic code generation, Solidity contract, Theorem proving

中图分类号:

TP311.5

朱健, 胡凯, 王军, 李洁, 叶亚飞, 时希言. 基于Event-B的可靠智能合约自动生成方法[J]. 计算机科学, 2023, 50(10): 343-349. https://doi.org/10.11896/jsjkx.220800134

ZHU Jian, HU Kai, WANG Jun, LI Jie, YE Yafei, SHI Xiyan. Reliable Smart Contract Automatic Generation Based on Event-B[J]. Computer Science, 2023, 50(10): 343-349. https://doi.org/10.11896/jsjkx.220800134

参考文献

[1]ZHU J,HU K,ZHANG B J.Review on Formal Verification of SmartContract[J].Acta Electronica Sinica,2021,49(4):792-804.
[2]ZHANG G Q.Introduction to formalmethods[M].Beijing:Tsing-hua University Press,2015.
[3]RYZHYK L,BJØRNER N,CANINI M,et al.Correct by construction networks using stepwise refinement[C]//14th USENIX Conference on Networked Systems Design and Implementation.USA:USENIX Association,2017:683-698.
[4]ABRIAL J.Modelling in Event-B:System and Software Engineering[M].UK:Cambridge University Press,2009.
[5]SCHNEIDER S.The B-method:An introduction[M].UK:University of Surrey,2001.
[6]BUTLER M,YADAV D.An incremental development of the mondex system in event-B[J].Formal Aspects of Computing,2008,20(1):61-77.
[7]BACK R J R,KURKI-SUONIO F.Distributed cooperation with action systems[J].ACM Transactions on Programming Languages and Systems,1998,10(4):513-554.
[8]BUTLER M.Decomposition structures for Event-B[C]//International Conference on Integrated Formal Methods.Germany:Springer,2009:20-38.
[9]BUTERIN V.Critical update re:Dao vulnerability [EB/OL].https://blog.ethereum.org/2016/06/17critical-update-re-dao-vulnerability.
[10]The parity wallet hack explained [EB/OL].https://blog.openzeppelin.com/on-the-parity-wallet-multisig-hack-405a8c12-e8f7.
[11]Batch overflow bug on Ethereum ERC20 token contracts andsafeMath[EB/OL].https://peckshield.medium.com/alert-new-batchoverflow-bug-in-multiple-erc20-smart-contracts-cve-2018-10299-511067db6536.
[12]BHARGAVAN K,DELIGNAT-LAVAUD A,FOURNET C,et al.Formal verification of smart contracts:short paper[C]//the 2016 ACM Workshop on Programming Languages and Analysis for Security.USA:ACM,2016:91-96.
[13]NIELSEN J B,SPITTERS B.Smart contract interactions in Coq[J].arXiv:1911.04732,2019.
[14]ZHU J,HU K,FILALI M,et al.Formal simulation and verification of Solidity contracts in Event-B[C]//2021 IEEE 45th Annual Computers,Software,and Applications Conference(COMPSAC).USA:IEEE,2021:1309-1314
[15]MAVRIDOU A,LASZKA A.Designing secure ethereum smart contracts:A finite state machine-based approach[C]//International Conference on Financial Cryptography and Data Security.Germany:Springer,2018:523-540.
[16]CHOUDHURY O,RUDOLPH N,SYLLA I,et al.Auto-Gene-ration of Smart Contracts from Domain-Specific Ontologies and Semantic Rules[C]//2018 IEEE International Conference on Internet of Things(iThings) and IEEE Green Computing and Communications(GreenCom) and IEEE Cyber,Physical and Social Computing(CPSCom) and IEEE Smart Data(SmartData).USA:IEEE,2018:963-970.
[17]GAO Y C,ZHAO B,ZHANG Z.Research and implementation of a smart automatic contract generation method for Ethereum[J].Journal of East China Normal University(Natural Science),2020,2020(5):21-32.
[18]ZHU Y,QIN B H,CHEN E,et al.An advanced smart contract conversion method and bidding contract design and implementation[J].Chinese Journal of Computers,2021,44(3):652-668.
[19]Rodin platform [EB/OL].http://wiki.Event-B.org/index.php/Rodin_Platform.
[20]BANACH R.Verification-led smart contracts[C]//Interna-tional Conference on Financial Cryptography and Data Security.Germany:Springer,2019:106-121.
[21]Remix [EB/OL].http://remix.hubwiz.com/#optimize=false&version=soljson-v0.4.25-nightly.2018.7.9+commit.c42583d2.js.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于Event-B的可靠智能合约自动生成方法

Reliable Smart Contract Automatic Generation Based on Event-B

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0