Computer Science

Computer Science ›› 2023, Vol. 50 ›› Issue (10): 343-349.doi: 10.11896/jsjkx.220800134

• Information Security • Previous Articles     Next Articles

Reliable Smart Contract Automatic Generation Based on Event-B

ZHU Jian1, HU Kai2,3, WANG Jun1, LI Jie2,3,4, YE Yafei3, SHI Xiyan5   

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

PDF (PC)

1205

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

CLC Number: 

  • TP311.5
[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.
[1] TONG Fei, SHAO Ranran. Study on Blockchain Based Access Control Model for Cloud Data [J]. Computer Science, 2023, 50(9): 16-25.
[2] ZHAO Mingmin, YANG Qiuhui, HONG Mei, CAI Chuang. Smart Contract Fuzzing Based on Deep Learning and Information Feedback [J]. Computer Science, 2023, 50(9): 117-122.
[3] 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.
[4] 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.
[5] 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.
[6] LIU Zerun, ZHENG Hong, QIU Junjie. Smart Contract Vulnerability Detection Based on Abstract Syntax Tree Pruning [J]. Computer Science, 2023, 50(4): 317-322.
[7] CHEN Ruixiang, JIAO Jian, WANG Ruohua. Smart Contract Vulnerability Detection System Based on Ontology Reasoning [J]. Computer Science, 2023, 50(10): 336-342.
[8] 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.
[9] 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.
[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.