[1]张取发,王昌晶*,左正康,等.一种基于UPPAAL的智能合约属性形式化验证方法[J].江西师范大学学报(自然科学版),2023,(01):45-51.
　ZHANG Qufa,WANG Changjing*,ZUO Zhengkang,et al.The Formal Verification Method for Smart Contract Properties Based on UPPAAL[J].Journal of Jiangxi Normal University:Natural Science Edition,2023,(01):45-51.
点击复制

一种基于UPPAAL的智能合约属性形式化验证方法()
分享到：

《江西师范大学学报》（自然科学版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2023年01期
页码:
45-51
栏目:
高可信与智能化软件
出版日期:
2023-01-25

文章信息/Info

Title:
The Formal Verification Method for Smart Contract Properties Based on UPPAAL
作者:
张取发1; 王昌晶1; 2*; 左正康1; 卢家兴1*; 廖云燕1; 王 渊3
(1.江西师范大学计算机信息工程学院,江西 南昌 330022; 2.江西师范大学管理科学与工程研究中心,江西 南昌 330022; 3.江西师范大学软件学院,江西 南昌 330027)
Author(s):
ZHANG Qufa1; WANG Changjing1; 2*; ZUO Zhengkang1; LU Jiaxing1*; LIAO Yunyan1; WANG Yuan3
(1.School of Computer and Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 2.Management Science and Engineering Research Center,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 3.School of Software,Jiangxi Normal University,Nanchang Jiangxi 330027,China)
关键词:
智能合约;  UPPAAL;  时间自动机;  安全性;  活性
Keywords:
smart contracts;  UPPAAL;  time automata;  safety;  activity
分类号:
TP 311
文献标志码:
A
摘要:
针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型; 然后定义并描述智能合约常见的安全性和活性,再使用模型检测工具UPPAAL验证智能合约的属性; 最后对购物合约进行了建模与验证,验证了该方法的有效性.
Abstract:
Aiming at the problem of smart contract property verification,the formal verification method of smart contract properties based on UPPAAL is proposed in this paper.The operational semantics of Solidity basic statements and its transformation to time automata are defined,and smart contracts are transformed into time automata network models.The properties of smart contracts include safety and activity.The common security and activity of smart contracts are defined and described.The model checking tool UPPAAL is used to verify the properties of smart contracts.The shopping contract is modeled and verified,which proves the effectiveness of the proposed method.

参考文献/References:

[1] TOLMACH P,LI Yi,LIN Shangwei,et al.A survey of smart contract formal specification and verification [J].ACM Computing Surveys,2021,54(7):1-38.
[2] SZABO N.Formalizing and securing relationships on public networks [J].First Monday,1997,2(9):1-21.
[3] DANNEN C.Introducing ethereum and solidity:foundations of cryptocurrency and blockchain programming for beginners [M].Berkeley:Apress,2017.
[4] MEHAR M I,SHIER C L,GIAMBATTISTA A,et al.Understanding a revolutionary and flawed grand experiment in blockchain:the DAO attack [J].Journal of Cases on Information Technology,2019,21(1):19-32.
[5] HESSENAUER S.Batch overflow bug on ethereum ERC20 token contracts and safe math [EB/OL].[2022-09-16].https://blog.matryx.ai/batch-over flow-bug-on-ethereum-erc20-token-contracts-and-safemath-f9ebcc137434.
[6] 倪远东,张超,殷婷婷.智能合约安全漏洞研究综述 [J].信息安全学报,2020,5(3):78-99.
[7] DEBBI H.Counterexamples in model checking:a survey [J].Informatica,2018,42(2):145-166. [8] OSTERLAND T,ROSE T.Model checking smart contracts for Ethereum [J].Pervasive and Mobile Computing,2020,63:101129.
[9] ALQAHTANI S,He Xinchi,Gamble R,et al.Formal verification of functional requirements for smart contract compositions in supply chain management systems [EB/OL].[2022-09-22].https://aisel.aisnet.org/hicss-53/os/blockchain/2/.
[10] 张广泉.形式化方法导论 [M].北京:清华大学出版社,2015.
[11] 李书霞,王国卿,庄雷.区块链智能合约安全的逆向实时模型检测方法 [J].小型微型计算机系统,2020,41(10):2030-2035.
[12] 赵颖琪,朱雪阳,李广元,等.智能合约的时间约束模式及其形式化验证 [J].软件学报,2022,33(8):2875-2895.
[13] WOHRER M,ZDUN U.Smart contracts:security patterns in the ethereum ecosystem and solidity [EB/OL].[2022-09-19].https://ieeexplore.ieee.org/document/8327565/.
[14] VUJICˇIC' D,JAGODIC' D,RANC'IC' S.Blockchain technology,bitcoin,and Ethereum:a brief overview [EB/OL].[2022-09-13].https://ieeexplore.ieee.org/document/8345547.
[15] BENGTSSON J,LARSEN K,LARSSON F,et al.UPPAAL:a tool suite for automatic verification of real-time system [EB/OL].[2022-09-19].https://brics.dk/RS/96/58/BRICS-RS-96-58.pdf.
[16] CHAUDHURI K,DOLIGEZ D,LAMPORT L,et al.Verifying safety properties with the TLA+proof system [EB/OL].[2022-09-19].https://members.loria.fr/SMerz/papers/ijcar2010.pdf.
[17] CHRISTIAN R.Simple open auction [EB/OL].[2022-09-23].https://learnblockchain.cn/docs/solidity/solidity-by-example.html.

备注/Memo

备注/Memo:
收稿日期:2022-11-21
基金项目:江西省教育厅科技重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ2200304)资助项目.
通信作者:王昌晶(1977—),男,江西丰城人,教授,博士,博士生导师,主要从事可信软件、智能化软件与智能化教育的研究.E-mail:wcj@jxnu.edu.cn
卢家兴(1976—),男,江西九江人,副教授,主要从事软件形式化方法、模型检测方面的研究.E-mail:003484@jxnu.edu.cn
更新日期/Last Update: 2023-01-25