一种基于UPPAAL的智能合约属性形式化验证方法_张取发.pdf

收稿日期:2022-11-21基金项目:江西省教育厅科技重点课题(GJJ220302，GJJ210307，GJJ2200303，GJJ2200304)资助项目通信作者:王昌晶(1977)，男，江西丰城人，教授，博士，博士生导师，主要从事可信软件、智能化软件与智能化教育的研究 E-mail:wcj jxnu edu cn卢家兴(1976)，男，江西九江人，副教授，主要从事软件形式化方法、模型检测方面的研究 E-mail:003484jxnu edu cn张取发，王昌晶，左正康，等 一种基于 UPPAAL 的智能合约属性形式化验证方法 J 江西师范大学学报(自然科学版)，2023，47(1):45-51ZHANG 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)，2023，47(1):45-51文章编号:1000-5862(2023)01-0045-07一种基于 UPPAAL 的智能合约属性形式化验证方法张取发1，王昌晶1，2*，左正康1，卢家兴1*，廖云燕1，王渊3(1 江西师范大学计算机信息工程学院，江西 南昌330022;2 江西师范大学管理科学与工程研究中心，江西 南昌330022;3 江西师范大学软件学院，江西 南昌330027)摘要:针对智能合约的属性验证问题，该文提出了一种基于 UPPAAL 的智能合约属性形式化验证方法 首先定义了 Solidity 基本语句的操作语义及其到时间自动机的转换，将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性，再使用模型检测工具 UPPAAL 验证智能合约的属性;最后对购物合约进行了建模与验证，验证了该方法的有效性关键词:智能合约;UPPAAL;时间自动机;安全性;活性中图分类号:TP 311文献标志码:ADOI:10 16357/j cnki issn1000-5862 2023 01 060引言区块链是一种安全共享的去中心化的数据账本，智能合约是部署在区块链网络上的计算机程序1，当满足必要条件时，它就会自动执行 早在1994 年，N Szabo2 就提出了智能合约的概念，他指出“一个智能合约是一套数字形式定义的承诺，包括合约的参与方可以在上面执行这些承诺的协议”随着具有去中心化和公开透明等特性的区块链技术出现，智能合约的信任问题得到了有效解决目前，以太坊3 已成为主流的智能合约开发和运行的平台 智能合约包含了区块链的众多特性，使得区块链与智能合约技术在许多领域都得到了广泛的应用尽管智能合约发展迅速，但智能合约的执行代码不能保证绝对安全，且智能合约运行时往往会伴随着大量数字资产的存储和转移，一旦遭到攻击，将会造成巨大的损失4-6 模型检测7 是验证智能合约正确性的根本途径 文献 8 对 Solidity 智能合约的语法和语义进行了形式化描述，提出了一种可以从 Solidity 程序生成 promela 模型的转换函数，然后使用模型检测工具 SPIN 来验证合约的性质 文献 9 提出了一种由不同实体开发和控制的交互式智能合约组成的系统验证方法，使用了模型检测工具NuSMV 来验证智能合约的功能属性 这些研究并没有系统地验证智能合约的属性 并发系统的属性包括安全性和活性10，智能合约作为一种并发系统，需要满足安全性和活性目前已有研究使用模型检测工具 UPPAAL 对智能合约进行验证 比如文献 11 提出了一种智能合约的逆向实时模型检测方法，手动地对投票智能合约进行建模并使用 UPPAAL 验证了智能合约的一些性质，但该研究没有具体地给出智能合约转换为时间自动机网络的方法;文献 12 提出了智能合约的 5 种时间约束模式，使用模型检测工具 UP-PAAL 对智能合约带时间约束的性质进行了验证，但该研究仅仅是针对了智能合约带时间约束的性质，没有系统地对智能合约的属性进行验证本文基于模型检测技术实现自动化验证，首先定义了 Solidity 基本语句的操作语义及其到时间自动机的转换，将智能合约转换成一个完整的时间自第 47 卷 第 1 期江西师范大学学报(自然科学版)Vol 47 No 12023 年 1 月Journal of Jiangxi Normal University(Natural Science)Jan 2023动机网络;然后系统地描述智能合约的安全性和活性，并使用模型检测工具 UPPAAL 验证智能合约的属性;最后对购物智能合约进行建模与验证，验证了该方法的有效性1智能合约文献 13 使用 Solidity 语言编写以太坊中的智能合约，该智能合约先通过编译器编译成字节码，然后在以太坊虚拟机(EVM)上运行14 Solidity 智能合约的主题内容由 contract 开始，在 contract 声明中主要包括变量、结构体、事件和函数 其中变量包括全局变量和局部变量;结构体由关键字 struct 声明;事件是由 EVM 提供的一个便利接口，由关键字event声明;函数由关键字 function 声明，函数描述的是智能合约具体的功能，是智能合约的核心一个智能合约的函数可以表示为function functionName(datatype dataName)external/internal payable modifierName()re-turns(datatype)，其中 datatype dataName 是函数的输入，returns 是函数的输出，若函数无输入输出，则该参数可省略 ex-ternal/internal 为函数的可见性，external 函数可以被其他的合约调用，而 internal 函数只能在本合约内部运行 payable 表示允许该函数接收以太币 modifer-Name()是函数的修饰器，可以改变函数的行为 下面是一个简单的拍卖智能合约，定义了构造函数constructor()和竞拍函数 bid()pragma solidity 0 8 4;contract SimpleAuction address payable public beneficiary;/受益人地址uint public auctionEndTime;/结束时间address public highestBidder;/最高竞价人uint public highestBid;/最高竞拍价格mapping(addressuint)pendingeturns;constructor(uint biddingTime，address payable be-neficiaryAddress)/构造函数beneficiary=beneficiaryAddress;auctionEndTime=block timestamp+bidding-Time;function bid()external payable /竞拍函数require(block timestamp auctionEndTime);require(msg valuehighestBid)if(highestBid!=0)pendingeturns highestBidder+=highestBid;highestBidder=msg sender;highestBid=msg value;2时间自动机网络模型2 1模型检测工具 UPPAALUPPAAL15 是一种基于时间自动机的模型检测工具，可以有效地对实时系统建模和自动验证，特别适合对实时系统的安全性和有界活性进行自动验证 此外，它还可以用于算法分析和协议验证等UPPAAL 采用一组带有整型时钟变量的时间自动机对实时系统的行为进行建模，用分支时序逻辑(computing tree logic，CTL)来描述系统的性质，使用其工具可对性质进行验证UPPAAL 验证器使用 CTL 语言来描述系统的性质，包括安全性和活性 其 BNF 表示语法为Prop:A p|A p|E p|E p|p imply q，其中 A p 表示在所有的路径上所有的状态都满足p;A p 表示在所有路径上未来都有 1 个状态满足p;E p表示至少存在 1 条路径，在该路径上所有的状态都满足 p;E p 表示至少存在 1 条路径，该路径未来都有 1 个状态满足 p;p imply q 表示若系统满足 p，则它也满足 q2 2时间自动机定义 1一个时间自动机可以定义为一个 6 元组(L，l0，C，I，E)其中 L 是所有位置的集合;l0是初始位置;是迁移的动作集;C 是时钟的集合，B(C)是时钟约束的集合;I 是每一个位置上的时钟约束不变式;EL B(C)2CL 是有向边的集合定义 2一个时间自动机的语义模型是一个迁移系统 T=S，s0，SL ZC表示所有状态的集合;s0=(l0，u0)表示初始状态;S Z S 表示迁移关系，其中 Z0定义 3一个由多个时间自动机构成的网络可以表示为 Ai=(Li，l0i，C，Ii，Ei)设 l0=(l01，l02，l0n)为时间自动机网络的初始位置向量，I(l)=ni=1Ii(li)为组合位置的公共不变量，该时间自动机网络的语义模型是一个迁移系统 T=S，s0，S(L1L2 Ln)ZC是状态集;s0=(l0，u0)是初始状态;S S 表示迁移关系图 1 展示了一个台灯系统的时间自动机网络左边的时间自动机表示台灯时间自动机 Lamp，描述了台灯的行为;右边表示用户时间自动机 User，描述了用户的行为 台灯共有 3 种状态:off(关闭)、low64江西师范大学学报(自然科学版)2023 年(弱亮)、bright(强亮)，台灯的初始状态为 off;用户只有 1 个 Idle 状态;2 个时间自动机之间通过一个信道 press 来进行同步通信 用户可以随时按下开关(press!)，台灯收到按下开关的信号(press?)时将状态变为 low，并且将时钟 x 置为 0;当台灯的状态为low，且用户在 5 个时间单位内(x 5)再按 1 次开关时，则台灯将会处于 bright 状态;如果用户超过 5 个时间单位(x5)按下开关，则台灯的状态将会变为off 当台灯的状态为 bright 时，如果用户按下开关，则台灯的状态将变为 off;如果用户在 50 个单位时间内(x 50)都没有按下开关，则台灯将会一直处于 bright 状态;如果用户超过 50 个单位时间都没有按下开关，则台灯状态将会变为 off图 1台灯系统的时间自动机模型2 3智能合约的语义及其转换在 Solidity 中常见的几种语句有赋值语句、条件语句、transfer 语句和循环语句 为确保智能合约可以完全正确地转换为时间自动机网络模型，对 So-lidity 几种语句进行形式化定义 表 1 给出了在转换后的时间自动机模型表 1Solidity 基本语句的操作语义及转换Solidity 语句操作语义时间自动机赋值语句sdo_S，ss条件语句:if(Con 1)if(Con n)Con，s trueif_Con_do_S，sS;if_B_do_S，sCon，s falseif_Con_do_S，sstransfer 语句:msg sender transfer(sum)(transter，s)truedo_S，sstransfer，s falsess循环语句:while(Con)SCon，s turewhile_Con_do_S，sS;while_B_do_S，sCon，s falsewhile_Con_do_S，ss3智能合约的属性在并发系统中，一个属性被看作是执行的集合，其包含的元素是满足该属性的执行16 一个智能合约可以看成一个并发系统，如果智能合约系统满足一个属性，那么该智能合约