欢迎访问一起赢论文辅导网
本站动态
联系我们

手机:15327302358
邮箱:peter.lyz@163.com

Q Q:
910330594  
微信paperwinner
工作时间:9:00-24:00

博士论文
当前位置:首页 > 博士论文
基于纳什均衡的智能合约缺陷检测
来源:一起赢论文网     日期:2021-11-14     浏览数:401     【 字体:

 第4 卷第1 2 0 2 1 年1 月计算机学报C H I N E S EJ O UR N A LO FC OM P UT ER SVo l .4 4No .1J a n. 2 0 2 1基于纳什均衡的智能合约缺陷检测陈晋川n ’2)夏华辉”王璞巍^马纳波u王琪u李浩然”杜小勇&nC 中国人民大学信息学院北京1 0 0 8 72 )2)( 数据工程与知识工程教育部重点实验室( 中国人民大学) 北京1 0 0 8 7 2 )摘要本文研究区块链智能合约的缺陷检测问题, 即检测合约中是否存在部分合约方无论选择什么动作, 均无法避免损失的状态. 将智能合约问题转换成合约状态迁移图上的博弈策略选择问题, 提出了基于纳什均衡理论的合约缺陷自动检测方法, 以及为了提高检测效率, 提出了针对合约状态变迁图和博弈策略形式的一系列化简方法.最后, 实现了一个智能合约建模、分析和部署工具. 针对一组真实合同的实验表明, 该工具能自动发现部分合同缺陷, 化简方法提升缺陷检测效率的效果明显.关键词智能合约; 纳什均衡; 缺陷检测; 区块链; 博弈论中图法分类号T P3 1 1DOI 号1 0 . 1 1 8 9 7 / SP . J . 1 0 1 6 .  2 0 2 1 . 0 0 1 4 7De t e c t i ngSma r tC o nt r ac tL oo ph ol e sB as e do nN a shE qu il i br i umC H E N J i n Ch u an1 ) , 2 )XI AH ua H ui1 )WA N GP u W e i1 ) , 2 5MA N a B o1 }WA N GQ i1 )L IH ao Ra n15D UX i a o Y o n g1) ,2)1 :){ Sc h o o l o f In fo rma t i on  ? R e nmi n Un i v e r s i t yof Ch in a ? Be iji n g1 0 0 8 72 )2 ) ( Ke y La b o fDa ta En gi n e e r in ga n d Kn o wl e dg e En g in e e ri n g ? Min i s t ry ofE du ca t i on  ? R e nm in Un iv e r s i tyof Ch in a ?B e ijin g1 0 0 8 7 2 )Abs t ra ctI nr e c en tye ar s , b l o ck ch a i nh as a t tr a c t e dm an yi nt e r e s t s fo r m bo t ha c ad em i can dr e s e a r chcomm uni t ie s ,an d be ena p p li ed in c r yp t o cur r enc y ,f in a nc i a l te ch niq ue s , l o g is ti c s ,co p yr i ghtp r o t e c t io n e t c .B l o c k ch ai ni s b a s i c a l l yad i s t r i b ut e ds t o r a g e  s y s t em ,c o n s i s t i n go f  a s e to f s e r v e r so r n o d e s .I nb l o c k ch ai ns ys t e ms ,s mar tco nt r a c t s ar ew i d e l ya do p t ed a st h ec o d el a w s to b eo b e ye dbya l lp a r t i c i p a nt s .B e fo r e  s t o r i n gt h e d at a i t em in t o b l o c kc ha i n , e ac hno de  ne e ds t o v e r i fyt h ev a li di t y o fth i s o p e r at i o n b ye x e c ut i ng i t sco r r e s p o n di n gs ma r tc o n tr a c t s ,i . e .com p u t e rp r o g r a m s . N o t e d th a t,i n th i s p a p e r w e f o c us o nc l as s i c  sma r t co n tr ac t s ,i . e .com p u t e r  co de s f o rv e r i f yi ng , ex e cut i n g , o r di s s e mi na t i ng  co n tr a c t s i na ni n fo rma t i o na lma n n e r . S m ar t c o nt r a c th a sb e c om eo ne  o f th e  co r et e ch n i qu e s o f b l o c k ch a in , a nd i ti s v e r yim p o r t an tt o s t u dyh ow t od e t e c tl o o ph o l e s e xi s ti ng i nsma r tco ntr a c t s . H e r e ,t h e  te rml o o ph o l e do e s n o tm e a nb ug s i nt h e co nt r a c tco de s , b ut s om e ba do u t p ut s o fe x e c u ti n g t h eco nt r a c ts .Th e s e o u t p u ts ar eu nf a v o r ab l e to  s om eco nt r a c t p a r t n e r s . If a l lp ar t n e r s ar e r a ti o na l an dh av e com p l e t e  i nf o rma t i o na b o u tth e c o n tr ac t s ,t h e s e o u tp ut s c a nn o tb e a v o i d edn om a tt e rw h a tch o i c e s t h ep a r t n e r s c ho o s ed ur in g e xe cu t i ng t h eco nt r a c t s .T h e r e f o r e t h e s e c o nt r a c ts w i l l n o t be com e r ep e a t e dg a me s s in c es o me p a r t n e r s c a n no tb en e f i tfr omj o i ni n g t he co n t r a c t s .T h e s eki n do fc o n tr ac t s w il lb eo n e s ho tg a m e s a n d ar eh ar mf ult o b us i n e s s zo o lo g y .Wep r o p o s eame th o dt od e t e c t t h el o o pho l e so f f o rma l i z edsma r t收稿日期: 2 0 1 9 1 2 0 2; 在线发布日期: 2 0 2 0 0 5 2 3 . 本课题得到国家自然科学基金( U 1 9 1 1 2 0 3 ) 、贵州财经大学与商务部国际贸易经济合作研究院联合基金( 2 0 1 7 SW B Z D0 8 ) 资助. 陈晋川, 博士, 副教授, 主要研究方向为分布式数据管理和区块链.E mail :ed u. c n.夏华辉, 硕士研究生, 主要研究方向为区块链和智能合约. 王璞巍( 通信作者) , 博士, 副教授, 主要研究方向为服务计算和区块链.E ma il :w ang pu we i@ r u c .e d u . c n . 马纳波, 硕士研究生, 主要研究方向为分布式计算和区块链. 王琪, 硕士研究生, 主要研究方向为区块链.李浩然, 硕士研究生, 主要研究方向为服务计算和区块链. 杜小勇, 博士, 教授, 主要研究领域为数据管理技术、语义网技术、智能信息检索技术.1 4 8 计算机学报 2 0 2 1年N ak a mo t o S.B i tc o i n: Apeer to pee r ele c tr o n i c c a s h s y s tem.2 0 0 8. h t tp s : / / bi tc oi n. o rg / b i t co i n.  pd fE th er e u m. h t t p s : / / w ww . e t h er e u m. o rgI l yp erled ger Fa br i c , h t tp s : / / h yp erled ger fab r i c . r ead t hed o c s .  i oK a n t a r aIn i t ia t i v e, h t t p s : / / k a n t a r ai n i ti a t i v e. o rg技术也有了迅速发展.随着研究者对智能合约理解角度的不同, 智能合约的内涵逐渐泛化,一些研究者开始把智能合约广义地理解成“ 运行在区块链系统之上的一段计算机代码, 由共识机制确保代码的正确执行[2] ”. 在本文中, 我们关注的是S z a b o 所定义的经典智能合约:“ 以信息化方式验证、执行或传播合同的计算机代码随着区块链技术的发展, 智能合约变得越来越重要,现有的区块链系统都使用智能合约描述参与各方需要共同遵守的规则( 合同条款) . 例如, 在医疗数据共享领域, 通过智能合约来规范数据的产生者( 病人) 、数据的保管者( 医院) 以及数据的使用者( 数据分析公司) 三方的权责利; K a n t ar aI n i ti a t i v e④ 则试图将区块链和智能合约变成一种法律条款的数字撰写平台;2 0 1 6 年工信部发布的《中国区块链技术和运用1 引§智能合约( Sm ar t C o n t r a c t ) 的概念最早可以追溯到1 9 9 4 年, S z ab o 将智能合约定义为“一种可以实现合同条款的计算机程序[ 1 ]但是,一直到2 0 0 8 年区块链( B l o ck c ha i n ) 技术出现之前, 智能合约都没能得到广泛关注. 原因可能是很难找到一种合适的技术可以在非完全信任环境中保证计算机程序正确执行和不会被篡改. 区块链源自于“ 比特币? ”的底层技术, 是一种去中心化、不可篡改、多方共同维护的分布式计算和存储系统. 区块链网络中每个节点都是独立维护的, 通过一种分布式共识机制, 在没有权威中心节点的情况下, 确保各个节点数据保持完全一致. 研究者认为区块链系统非常适合为智能合约提供运行平台. 2 0 1 3 年后出现的以太坊? 和H y p e r l e dg e r Fa br i c? 都提供了图灵完备的编程语言用于编写智能合约, 可以支持各种复杂的业务逻辑. 至此, 智能合约开始得到了越来越多的应用, 其co nt r a c t s b a s e do nt h eN a s he qu ilib r i u mt h eo r y. I n s t e ad o f hi r i n gl a w ye r s t o ch e c kt heco nt r a c tt e rm s o n e by o n e, w ec a n n ow a ut om at i c a l l y fi n do utt h el o o p h o l e s o fc o n t r a c t s .Wep r o p o s eada t as tr uc t ur e , c a l l e d s t at e t r a n s i t i o n g r a ph , t od e s c r i b e  th e o u t p u t s f o r e a ch p ar tn e ro f c h o o s i n gdi f f e r e nt s tr at e g i e s o f e xe cu t i ng a c o nt r a c t .B a s edo nt h e s ta t e t r a ns i ti o n g r a ph ,w e  f ur t h e r d e f i n et h ep r o bl e mo fs ma r tc o nt r a c tg a m e, an d de f in e th e  lo o p ho le s a s a s p e ci a lkin do fN a s he qui l ib r iums,w h e r es om ep ar t n e r s w o ul d o b t ai n z e r oo r  n eg at i v e u tili t i e s  a nd th ey c a nn o t i mp r o v e t h e i r u t ili ti e se v e nif  th e y ch an g e t h e i r ow n s t r a t e g i e s . I nt h i sw a y ,w e a r ea b l e to a ut om at i c a l l y fi n do ut t h el o o p h o l e s b y com p ut i ng t h eN as he qu i l i b r i um s o fsm ar tco nt r a c t g a m e . H ow ev e r ,t h es t r a t e g yfo rm so b t a i ne df r omt h es t at e t r a n s i t io n g r a phma yb et o ol a r g edu et o s t at e exp l o s i o n .T h e r eco u ldb emil li o n so f a n de v en l a r g e r nu mb e r o f s t a t e s i na s tr at e g y fo rm ,w h i chc a us e s v e r ye xp en s i v e t im e co s t s o f co mp ut i n gN as he qui l i b r i um s . We t h e n p r o p o s e t w o r u l e s, i . e . St r a t e g ye qu iv a l en c e a n dN a s he qu iv a l en c er ul e s ,f o r s i mp li fy i ng t h es t a t e tr an s i t i o n gr a pha n ds t r a t e g yfo rm s , w h i ch c a ng r e a t l ycu tdow n t h e  ti m e co s t s . I no r de rt o  fu r t h e r cu tdow n t h e  t im e co s t so fco mp ut i ng N a s he qu i l i br i u m ,w ea l s op r o p o s eam e t h o dt ofi n do utt her e du nd a nts t r a t e g yco mb in a ti o ns a ndp r o v et h a tw ec a no b t ai nt h es a m eN as he quili b r i um s w h ent h e s es t r a t e g yco mb in a ti o ns a r er e mo v ed.B a s e do nt h e s eme t h o ds ,w e de s i g na n dim p l em en tat o o lf o rmo de l l i ng , a n a l yz i n g an dd ep l o yi n gs ma r tco nt r a c t s .Wea na l yz eas e to f r e a lco n t r a c t s c r a w l e dfr om t wo p r o f e s s i o n a ll aw y e r w e bs i t e s . T h e s e co n t r a c t s co v e r  th e ma i nco nt r a c t c at eg o r i e s li s t e di nC o n tr a c tL a wo fP eo p l e?s R ep ub li c o fC h i na . We d i s c us s s ome co n t r a c t l o o pho l e s de t e c t edb yt h is t o o l, an dev al u a t et h ea bi l i tyo f o u rp r o p o s edme th o ds t o im p r o v e t h ep e r f o r ma nc e .A sil l u s t r a t edb y th e  e xp e r i m en t a lr e s ul t s , o ur me th o ds  c a ng r e a t l yr ed uc e t h e s tr at e g yf o rm s a n dt h et im e c o s t s .K eyw o rdssm a r tc o n tr a c t;N a s h eq uili br i um ; l o o ph o l e de t e c ti o n ; b l o ck ch a i n ; g am e t he o r y①②③④陈晋川等: 基于1 期 纳什均衡 的智能合 约 缺陷检测 1 4 9发展白皮书》[ 3 ], 将智能合约解释为一种用计算机语言取代法律语言去记录条款的合约. 我们期待智能合约可以逐渐替代部分传统合同. 但是, 智能合约并没有统一的编程语言和运行模型. 这就使得程序员之外的管理人员难以理解和编写智能合约. 例如, 以太坊使用S o di U t y 编写智能合约, 将其实现为一种状态机?; H yp e r l edg e rF a br i c 智能合约被称为链码( C h ai n co de ) , 使用Go 语言编写, 没有全局状态, 对区块链的读写都需要经过链码来执行.接下来, 我们用一个非常简单的买卖合同例子分析智能合约编写面临的问题:“ 卖方发货, 买方将钱转账给卖方编写这样的智能合约, 我们首先遇到的问题是:如何构建一种与编程语言和平台无关的、易于理解的中间模型? 文本合同是由参与各方的管理人员( 律师) 用自然语言撰写的, 然而智能合约需要使用计算机编程语言实现, 因此又要由专业的程序员编写. 由于自然语言和程序语言之间的差别, 双方可能无法准确理解彼此的意图. 例如, 上述例子中没有明确说明“ 卖方什么时候发货”, 这给智能合约代码的编写带来困难, 他们之间缺少一种双方都能准确理解的中间模型( 类似数据库领域的E R 模型) , 这就是智能合约建模问题;此外, 我们还会面临第二个问题: 如何发现智能合约中存在的逻辑缺陷? 智能合约是由计算机代码构成的, 现有的一些方法提出使用检测工具对智能合约代码进行检测以找出其中存在的漏洞[2]. 然而,智能合约的一些重要缺陷, 其实不是代码漏洞, 而是逻辑缺陷. 例如, 前面例子中的买卖合同存在着一个对卖方不利的执行路径:“ 卖方发货, 买方不转账我们需要对智能合约进行分析以判断是否存在这样的逻辑缺陷, 这就是智能合约的缺陷检测问题.对于第一个问题, 我们之前提出了一种智能合约形式化模型[4]. 首先, 站在管理人员的角度, 采用多A g en t 领域的承诺( com mi t me nt ) 模型[5], 将智能合约看作是一组“ 承诺” 的集合. 承诺描述了参与各方要执行的动作; 其次, 站在程序员的角度, 将智能合约看作是一种基于承诺生成的状态机, 描述智能合约的执行过程. 在之前工作的基础上, 本文提出从承诺到状态机的自动生成算法. 但在这个生成过程中, 往往会遇到“ 状态爆炸”问题, 也就是会产生指数级的数量巨大的状态, 导致生成算法无法高效完成.为了应对这个问题, 本文又提出了一系列的化简算法, 可以极大地提高状态机的生成效率.对于第二个问题, 根据智能合约参与各方选择的动作不同, 智能合约将进人到不同的状态, 形成不同的执行路径. 我们提出把这种执行过程看作是一个多方博弈问题[6]: 各方将会从智能合约中获取或损失收益, 他们是理性的, 会以收益最大化为目的来选择如何执行动作. 智能合约中的逻辑缺陷实际上是指部分参与人会陷人到一种局面, 无论他们选择什么动作, 都无法避免收益损失. 我们提出用“ 纳什均衡( N a s hE q uili br iu m )” 思想来捕捉这样的缺陷.纳什均衡是博弈论中的重要理论, 对于参与博弈各方所能选择的策略, 存在这样的策略组合: 各参与方均不能通过单方面改变自己的策略来获取更好的收益. 例如, 考虑一个简单买卖合同, 卖方有两种可以选择的策略{ 发货, 不发货} , 买方也有两种策略{ 转账, 不转账} . 对于策略组合{ 卖方不发货, 买方不转账)?, 卖方和买方单方面更改策略都会面临收益损失: 如果卖方将策略改为发货, 买方还是不转账, 这会使得卖方出现收益损失; 同样如果买方将策略改为转账, 卖方还是不发货, 也会使得买方收益损失.这样的策略组合就称为纳什均衡点, 它体现了博弈的均衡状态, 在此状态下各个参与人都倾向于采取理性的行动.我们定义合同的逻辑缺陷就是特殊的纳什均衡. 如果合同的纳什均衡点中, 各参与人的收益全部为零, 或者收益有正有负, 那么这个合同就可能有逻辑缺陷, 因为部分参与人无法取得正收益, 他们将不再倾向于参与合同. 上述简单买卖合同例子中, 唯一的纳什均衡点就是{ 卖方不发货, 买方不转账} , 此时双方收益均为零. 原因在于该合同中没有对买方违约行为( 不转账) 进行约束. 那么理性的卖方在权衡得失之后, 将选择不执行合同. 这样的合同对双方都没有价值.对于简单的合同, 执行路径较少, 容易以人工的方式发现逻辑缺陷. 但是对于复杂的合同, 其执行路径将非常复杂. 即使受过专业训练的律师也可能难以发现合同中所有的逻辑缺陷. 当合同以智能合约的形式存在, 人工检测逻辑缺陷将更不可行.本文的贡献如下:( 1 ) 提出一种基于纳什均衡的智能合约缺陷分①E th er e u m.h t t p s :  // s o li d i ty , r ea d t h ed o c s . io / e n / v O . 4 . 2 1 /c o m mo n p at t e r n s , h t ml E s t at e m ac h i n e1 5 0 计算机学报 2 0 2 1年析方法. 形式化定义了智能合约的博弈问题、策略形式和纳什均衡; 将智能合约的缺陷检测问题转换成了纳什均衡计算问题, 通过对智能合约逻辑缺陷的分析, 可以将逻辑缺陷以及相应的收益情况反馈给用户, 避免因为智能合约的逻辑缺陷给用户带来损失;( 2 ) 提出了一种基于智能合约形式化模型的纳什均衡检测算法. 将形式化定义的智能合约转换为状态变迁图; 基于策略等价原则和纳什均衡等价原则, 提出了一系列状态变迁图的化简方法, 极大地避免了状态爆炸; 然后根据简化的状态变迁图, 提出了冗余策略的化简方法, 进一步提高计算纳什均衡的效率;( 3 ) 依据《中华人民共和国合同法》( 1 9 9 9 年3 月1 5 日颁布) , 常见的合同共有1 5 类. 我们参照华律网( 6 6 l a w . c n) 和合同帮( h e t on g b . co m) 的合同范本,对其中1 4 类合同进行了分析, 找出了其中真实存在的合同缺陷, 说明方法的有效性; 并通过实验分析了所提出的化简方法的效率.本文第2 节介绍智能合约建模和分析的相关工作; 第3 节介绍如何为智能合约建模, 以及智能合约的状态机生成算法; 第4 节介绍智能合约的博弈问题; 第5 节介绍状态变迁图的化简方法, 以及冗余策略组合的化简方法; 第6 节通过实验说明所提出方法的有效性和效率. 最后, 第7 节进行总结和对未来工作的展望, 本文工作并非提出新的智能合约, 而是将合同建模为状态机, 并基于此建模方法对合同进行分析.2 相关工作智能合约漏洞暴露出来的安全性事件一直层出不穷, 例如, 2 0 1 7 年发生的DA O ① 事件, 黑客利用智能合约的漏洞将面向公众筹集的大量以太坊代币转向自己的地址, 造成了巨大的经济损失. 因此, 智能合约安全性一直受到研究者广泛关注, 目前很多工作采用软件工程领域的代码检测方法来做智能合约代码漏洞检测. 2 0 1 6 年, H m n ? 提出将智能合约代码转换为A V L 树, 然后利用I s a b e l l e 定理证明器对A V L 树进行验证, 找出智能合约的代码漏洞.Y a ng 等人[ 7 ] 提出一种符号模型( S ymb o li c Pr o c e s sV i r t ua lMa c hi n e , FS PVM ) 用于刻画智能合约的执行流程, 然后基于H o ar e 逻辑验证智能合约代码的可靠性和安全性. B l g l 等人[ 8 ] 认为智能合约中参与人之间存在非合作博弈, 在假设他们是理性的前提下分析他们可能采取的策略, 在此基础上生成一种概率模型, 再检测智能合约的安全性. 上述这些工作目的是为了检测智能合约代码的安全漏洞. Bl g l 等人虽然提到了博弈论的概念, 但也只是为了分析合约参与人可能的行为, 并没有考虑合约公平性的问题.不同区块链系统有不同的智能合约运行模型.例如, 以太坊是公有链, 任意节点都可以加人参与交易. 它的智能合约用S o di Ut y 编写, 以字节码形式存储于区块中, 可以被各个节点执行. 智能合约在发布之后可以被多次调用, 每次调用均需从之前的区块中读取合约的状态和字节码, 而执行的结果也会存人新的区块中. 因此, 智能合约在以太坊上的执行可以看作是一个状态机, 每次执行将会从一个状态转移到另一个状态[9]_H yp e r l edg e rF a br i c 是使用最广泛的许可链, 节点需要经过授权才能参与交易. 与以太坊不同的是, 它的智能合约( 链码) 并不存储于区块, 而是一直运行在联盟节点的do c k e r 容器之中. 采用Go 语言编写, 对区块链数据的读写都要通过链码执行( 但链码本身不记录执行后的状态) . 需要注意的是, 智能合约是一个概念, 指一种可以实现合同条款的计算机程序, 本质上智能合约与区块链是独立的. 链码是H yp e r l e dg e rF a br i c 系统中实现智能合约的方式, 在发展过程中超越了传统智能合约的概念. 本文讨论的智能合约是一个状态机, 是程序化的合同条款, 我们将基于承诺模型来描述合同并自动生成相应的状态机.在多Ag en t 领域中, 承诺( com mi t me nt ) 模型通常用来研究多个主体之间的交互协议. S mgh 等A[5 a °] 形式化定义了承诺模型, 认为承诺是商业关系的基本抽象, 是商务合同的本质. 承诺是有状态的, 例如, 完成、违约和过期等. 对于每个承诺, 有操作( 动作) 可以触发其状态发生变化. 不同承诺之间存在相互影响关系, 多个承诺就构成了多个主体之间的商业协议[ 1 1 ]. 在承诺模型的基础上, Sn gh 等人[ 1 2  ̄] 又提出了商业合同公平性和健壮性等属性的检测方法, 基本思路也是判断各方是否都从合同中收益或者合同执行是否会进人非法状态. 这些工作没有考虑商业合同运行在区块链之上的情况, 本文①T h eD AO. h t t p s : / / g i t h u b . c o m/ s l o c k i t / DA O②I l i r a iY .F o r mal Ver i f i c a t i o n o f D eed Co n t r a c t i n E th er e u mN a me Se r v i c e ,2 0 1 9 .h t t p s : / / y o i c h i h i r a i . c o m/ d e ed , p d f離劑等I.霜1 期 于靖计禅衡的臂俱脅约缺陷錄 1 5 1提出在承诺模塑的基■础上构靡智能合约( 商业合同) 5 搏设计算怯从一组承诺_ 动生成运行隹型( 也就是狀态机模爾)? 然后在状态机模:型的基础上.动分析智能含约, 检测出可能存在的?辑缺陷. 在文献[ 1 1 ] 中, 也提出采用纳什均衡来分析合同的芷确性( iSt i池ct n es轉, 但其方機需醫'齋華博虐:树中所有可'能的路径. 役有做任何化简■■ 在敢率上与我们所实现的Ms&li n e 方法(雜8; , 中的SE 方法3: 相综上所述现有的智能合釣分析工作主驀还是进行代码漏洞分析, 缺少对费约中逻辑缺陷的分析?此外, 现有区块链系统的智能合约运行樓型各有不同, 缺少一种统一的、无关于编程谱有和平舎的智能合约模型* 甩于支持这种分析. 本文提出了一种易于痤解的、编程语言无关的智能合约模型以及基于纳什均衡理论提出了一种脅约缺陷检铡方法.3 智能合约的建模承诺模型在多Ag ent 领域被广泛用宁对跨组。织协议的建模¥9 1 2 ]. 本文提出智能合约建模首先_用户将合同条款以“ 承诺”的形式描述, 然后再基于用户书写的承诺自动构建智能合约. 本节介.绍如何定ic' 承诺' 以及如何儀T一组承诺_ 动构建智能合钓的状态机?3. 1承诺定义1 _承谱f eamm itm en t)?一个承谨是一个五兀组CC a s , _v ,|< , , 表市攀向_v 承诺, 見謹肅提条件K pr emi s e) 瘸足, 就#在k 规定的时间期限完:威K触t il t ) ?定义2 . 承诺的生命周期?一个承诺可能具有五种不同的状态* 其.生侖M 期可以用一个状态机表示, 如_ 1 所示.act ( l ) C(x, y,p, r ,tc )timeou tC (x, y,夕,r,false ) exp (A )p=true6as ( 2 ) C( x, y , true,r , £c)^meou,->C ( x^y,tn ie, r, fa lse ) vi o (5 )sat( 3 ) C (a:,3>,t rue,true,ic )图i 最if銳命屬_如图l 所示,一个承诺的生命周期内可能有五种不同的状态, 其中激活( 《戊1 是初始状态》终止状_纛蠢彳过期(:** #) fji:约), 病嚴:( 1 . ) 撒活(似) . 当前提户和结果f 的值都未知,并且^? 处于有效期/本文用数宇1 表示_( 2 ) 就:靖f办狀h 前攝户涂t ru e?零皋r米麵, 并且的^ 并未超出有效期? 此时则表示前撻f 已鐵达成, 等待结果的竞成。本文用数字2 表示._ 橋足C sfi d. 当一个:攀舉截T雜_之錄!_责任言工13成了绪:果"■承诺迸人满: ■£(:.?? ) 状态,毫示承诺完成. 本文用数字3_ 示.U) 过期( e:#, ) . 若承诺原本处于激活态* 但如果超出了时间约束, 师承诺进入过期状态. . 表;示承谱已羟失数, 本X用数字4 表示-违约( tA) . 承诺进入就绪态, 前提>已絰满足, 但衰任方' * 没有在规定的时间fr完成结渠r ,.则承诺迸人违约状态. 本文用数字5 表示.承诺的前提条件f 長一个逻辑表达式, 组成表:达式的每个文字( l i tem D可以是一个布尔条件, 表示某个承诺处于某个状鑫, 例姐若承诺C2 的前提>=表示必须G 的状态为之后, &才可以就绪. 前提的文字也可以是一个布尔函数形式的仲裁结果, 表示由第三方判定某个条件是否成立. 例如,在某运输合同中有一个承诺, 春出现自然灾害, 则承运方无衝^赔偿, 那么承诺的前提条件就应包括乂K 〇%e ( 自然戴害X 本文使思jWge 函数来表藏仲裁, 仲裁可以_ 智能脅约瑱育机cw ( 监控K 块链事件并能将监控结某发回智能合约) 或合同双方共同指麵愈第三方蠢成* 蠻藝證出, 预言机■ 第三方只鬱赛对所规定的事项作出仲裁, 而不是仲裁整个合同的执行状况.r 称为承诺的结果* 晕一组动作的合取式-时间雜索紀包'含两个部分, 即纪:= 如加瑪《山分别表示当承诺进人,或&? 之后, 承诺应该在或扛- 醜軸窟珙.例1.—个筒单翁购书合f'承谱在S 天内忖拿1 〇〇元, 3獻爾審收到书擊之B I 天为鼕赁,G ( 伊, 乙, 0 , |w iy( Z ,1,?: )* ( *3 ) ) ,C2 ( Z > ^^ 0% , s at ^de l i i <er(,bog k < ^ ) . ( 1 . 1 ) ) .承请戌的含X 是甲向乙承诺》在3 天内付款1 〇〇元. 法意此承诺的前提: 条件为空. 即不设前提?并且此承诺在前提满足之后3 天内必舊晃成动作pay i Zj  . 1 0 0 5 .承诺^ 的含义是, 当承诺C: 进人如状态( 即:甲在3 天内付款则乙承诺在i 天内发货? 注意该承诺的时间约束的.第一部分为;} 天, 含义是在合约签署3 天之后, 该承诺过期? 也就是说即使甲在3 天1 5 2 计導机攀报 :_1苹之后窟成承诺c\ , 乙也没有义务发货.3 . 2 智能合约定义3?智衝合釣Cfem stft「初n tr aM) .—个智能含约是一个确定性有穷状态机( DFA ) , 即S C :={, CCf S i S fs〇, A , r ):( 1 )CC = ! C! ,? ” 》.C;U 袭示一组承诺;( 2) 5 是字母表, 包括所有可触发CC 中一今或■个承诺谶慶状_ 的導件.一个審件可M ;叢一个动作, 某个仲裁的绪果, 或是某个承诺状态发生改变( 比如过期) ;_S= '! %,*>、, 心U 暴有|艮个状态的' 集合.s,.Ci= 〇,…, ? 》) 是一?个《维_ 量, 即S; 3 霉i —痛if,…,C? . s iUM^^(. stat eS?i〇. ct-: . sMiexp?ta o } )( 4)  5 a £ S 是初始状态, 若一个承诺的前提为壑, 贝丨1眞_ 絳中状态为feiq—施其截霧为d rf;( 5 ) ZbS其羞一# 綦状态较穆画数;j一个状态转^'(St <, : e) > -Sj£: Z \ if fCD* 和? 两个feftgfeg I 雜Jl的取值不區tA=1? ? ) . J=L?) : 依据G 的定义, 当事件e 6 5 发生, CA 的状态应从書为*! ■ ](: ?是一钽接受:的状_ c:馨态), v s, e , ,{s a l , e^xp. <'vio } ( k= l .图£中展示的是根据例1 中的承诺得到的智能合约? 如a2 所示, 合約的初始状态(. 裉,结点) 为( 2 , 1 S , 国为承诺c\ 前提为痊, M 此其初始状态为2 C &ax) . 图Pp 斑上最出了遽变含约狀态的書件, 比如在初始状态可以象:■寶个事件, f細e〇?lfey< Ci :) 和前春Ci 在进人Ws 之后:超时, 也雜倉祿翁歲:承诺违翁, 因此转变勤狀态C 5,1 ), 表示:■诺的拔态展2 (&?s ) 改变愈g tfei o:) .. 爵一个_件, 參示甲执行付款动作, 使得承诺& 从2 ( &? ) 改变为为进人到〇的前槔得到满足, :真状态售动从1 C财i :》变为2 (知功《菌此我们導到状處t3? 2 ) ? 洼參, 当一个擧诺:的翁禪变为tr ue? _状高將e^t imeoutjjas(Q )( 5〒1 )乙 C( 3,2 )e3=t imeout- ac t (p2)r?4= del ivep/,'C 5 ?4 )E( 3,3 )乙=ti meout_ ba s(C2  )( 〇,〇) ( 10,10 )F( 3,5 )(-10 0,10 0 )图2DF八形式的智能合约自动从1 变:更为2 *无醫颡外事# 触发? 寅此本文描述中都略去了从1 到2 的状态变化过程.3 . 3 由承诺生成状态机根据一组承诺, 我们可以有动构造相应的DFA.算法如卞.算法1 . 创建D FA .翁入t 一组承雷££:输ShKFA 的根鷄^1.n Q—i ni tR o o K CC) ; / /wQ 是DF八根结点2. H. f MsM n。); / / // 是一个堆栈, 存放状态结点3 .W H ILE C Hn ot emp ty)D O {4.n ^H. pop i );5.s —n. st a t e;6.FOR ( e a c hZ 满足( 5 , e )—5'£ d )D O {7.IF  (/ £ H)T HEN f/ /若该状态曾出现过8.c h d^{in d ( H ^sf);9.a d d Ch i l d ( w,c/ it〇;1 0.}1 1.EL SE { 巧新的状态结点1 2.c r ea t eCh il d ( n;1 3 .H. p ush e s'fc hd); }1 4.}1 5 . }1 6. R ET URNn〇;算法i 第一行初始化一个根靖点将:其存入到堆栈h 中. 当堆栈不.为壑, 读出栈顶的结点》以及该錯点的状态S . 箕法第6 行遍历所有可以改变当前状态的事件e , 算法7 ?1 3 行将孩子状态加到当前结点的孩予集合中? 第8 行从H 中读出已有的一个结点第9 行根据构造当前结点》的孩子. 第1 2 行根据Z 构造m 的一个新的孩子截獻回过头来分析例1 , 这是“一手交钱4一#交货”的经典交易模式? 然而, 显熬例1 是有问题的* 襄方_全珥以在收到货款之唇不发货? 在下一节>我们将从博弈论的角度淹对例1 进行分析, 并给出基于纳什均衡验测合同缺陷的方法,4 智能合约的博弈问题商业合W是一个典型的博弈过程, 合同参与人在合同的不同状态上可遞有不同的策略, 以凝得对自己最有利的结果- 举节将首弗定义智能合约的博弈问題, 再讨论如何基于博弈论的思想來負动分析合同的优劣.定义4 . 智能含约博弈. 智能合约博弈由下列陈晋川等: 基于1 期 纳什均衡 的智能合 约 缺陷检测 1 5 3部分组成:( 1 )一个参与人的集合N ;( 2 )— 个状态变迁图M =( S C ,《) , 其中S C 是状态机( 见定义3 ),《是参与人函数, 它赋给S C 中每个非终止状态 ̄■ 个参与人, 也就是指在非终止状态s 上只有《〇) 可以采取行动;( 3 ) 对每个参与人z'e w 有一个终止状态上的效用函数M, :R +. M,〇) 表示参与人i 在终止状态^ £ , 上的收益.图2 中的例子也是一个状态变迁图. 包含两个参与人 ̄={ 甲, 乙} . 每个非终止状态( 内部结点) 的行动人标在了结点旁边, 例如《( A )= 甲. 参与人甲的效用函数是 M!  ( D)=0 , M! ( E )= 1 0 , M! ( F )= 1 0 0 ;参与人乙的效用函数是m 2 ( D )=0, m 2 ( E )= 1 0,Mz ( F)=1 0 0 . 简略起见, 我们将两个参与人在一个终止状态的效用值写成一个向量. 在图2 中, 结点D、E和F 下方是两个参与人的效用值, 甲在前, 乙在后.定义5 . 智能合约博弈以,]^ ^ , “ ) 〉* ^ ,个参与人可以采取的策略集合是笛卡尔积a={e|  ( s , ,e )— s,eZ \ }_— 个策略组合是y= ( on ,…, (〇j v ) e x , e N f 3, , 其中(〇, e ft 是参与人z en 策略集合的一个策略, 即第z 个参与人在各个内部结点上所选择的动作.对于每个承诺《^ , 3 ^, ^ , 「, 化) , 责任方2 是发出承诺的一方. 那么对于C , 当前提f 为真时, :r 就有两个选项, 履行承诺或者违约. 当前提f 为假时,Z 只有一个被动的动作选项, 即让承诺过期.例如, 图2 中, 结点A 对应承诺6 ( 伊, Z , 0 ,f a_y ( Z , 1 0 0 ) , ( ⑵, 3 ) ) . 由于前提条件恒为真, 甲在结点A 上可以选择执行的动作为{ei ,e2 } , 即h?e 〇M i_6 a 5 ( C! ) 和f a_y ? 第一■ 个动作表亦甲在约定期限内不付款, 使得该承诺违约. 第二个动作表示甲选择付款, 履行承诺. 因此在结点A , 甲的策略集合是a= {ei ,e2 }. 类似地, 乙在结点B 可以执行的动作有{ e 3 } , 在结点C 可以执行的动作为{ e 4 ,e 5 } . 那么乙的策略集合是笛卡尔积a={ e 3} X{ e 4 ,e 5}={e3e4 ,e3e5 } ? 这里,e3e4 是乙的一个策略, 含义是他在结点B 时会做动作e3 , 在结点C 会做动作e4.参与人策略集合的笛卡尔积就是所有可能的策略组合集合. 例如, 根据甲和乙的策略集合, 有一个策略组合( 61 ,6364 ) , 其含义是: 甲在结点4 时会做动作^ , 乙在结点B 时会做动作e3 , 在结点C 时会做动作e 4 .对于每个策略组合7 , 在状态变迁图中都能确定并且唯一确定一条从初始结点到终止结点的动作序列. 例如, 对于策略组合( eu A q ) , 在图2 中A 是初始状态, 甲做动作Q , 合约状态将改变为状态B .按照策略组合的内容, 乙将在状态B 做动作e 3 , 合约将进人到终止状态D. 注意, 没有进人状态C , 因此乙也就没有做动作? 也就是说, 在一个策略组合中并非所有的策略都会真正执行.对于参与人来说, 他们的收益只与终止状态有关, 因此会关心动作序列的终止状态. 我们把动作序列表示为甲上乙:■ 〇, 其中D 是一个终止状态,甲J 表示参与人甲执行动作e i .定义6 . 智能合约博弈〈? , ]^ ^ , ( 叫) 〉的策略形式表亦为〈N , M ,) , ( m, ) 〉, 对于每个参与人有:( 1 ) a 是参与人z'e w 的策略集合;( 2 ) M l : X , e N [a — R+ 是参与人z 在策略组合上的效用函数. 任意一个策略组合V y e X a N a , 在状态变迁图m 中确定并唯一确定一条终止状态是s的动作序列, 因此有=〇) ( M ,〇) 是参与人i在终止状态s 上的效用) .由于例1 中只有两个参与人, 其博弈问题的策略形式可以通过效用矩阵表示( 甲是行参与人,乙是列参与人) , 如表1 所示. 注意, 每个策略组合对应矩阵中一个元素. 例如, 策略组合( e i ,e 3 e 4 ) 对应左上角的元素. 该策略组合在图2 中确定了一条唯一的动作序列甲二乙二D. 因为有叫( D )=0 和m2 ( D )=0 , 左上角的效用值为( 0 , 0 ) .表1 效用矩阵甲-乙e3e4e3 e50 , 0 0 , 0e21 0 ,1 0 l oo a o o定义7 . 纳什均衡? 智能合约博弈〈N ,M ,a,( Ml) 〉的纳什均衡是一个策略组合y*=U 『,…, 〇^ )ex i e N lQ , , 使得对每个参与人w e w 的策略a 有M,  (. CUt :CU ,  )M , ( (0 , 5(0 , ) .上式中表示策略组合, 中去掉参与人Z 的策略‘ 之后其他参与人的策略. ( 〇A , 〇0 表示动作人Z 选择任意策略, 其他参与人选择中规定的策略. 也就是对于任何一个参与者Z 而言, 当其他每个参与者都选择均衡策略时, 参与者Z 所有的策略产生的效用都不高于他选择策略W 所产生的效用.1 5 4 计算机学报 2 0 2 1年例如, 从表1 中可以看到对双方都有利的策略组合是0 2 ,e3e4 ) , 在图2 中对应着动作序列甲2 乙J e , 含义是甲付款, 且乙发货, 双方各自可以得到1 0 的效用值. 然而, 这个策略组合不是一个纳什均衡, 因为乙可以改变他的策略为e3e5 , 也就是不发货, 使得乙的效用值从1 〇提高到1 0 0 . 理性的乙在这种情况下会选择不发货, 因此甲付款且乙发货这样的理想局面无法出现. 根据表1 可以计算出只有一个策略组合是纳什均衡, 即右上角的( e i , e 3 e 5 ) .该策略组合在图2 中对应着一条动作序列甲1 乙iD , 含义是甲不付款, 且乙不发货, 双方的效用值都是〇. 这是一个纳什均衡, 因为双方都无法通过单方面改变策略来获得更多的收益: 如果甲将他的策略改变为e 2 , 他的效用值会从0 降低到 1 0 0; 如果乙将他的策略改变为e3e4 , 他的效用值保持不变, 依然是〇.根据纳什均衡理论H1 6 ], 如果所有参与人都是理性的, 完全了解效用矩阵, 并且存在纳什均衡, 参与人会选择进人到纳什均衡的局面. 这是因为参与人在做策略选择时, 当预计到可能会进人到非纳什均衡的局面时,一些参与人知道他们可以通过改变策略获得更多的效用值. 由于他们都是理性的, 他们会改变策略, 因此非纳什均衡这个局面并不稳定. 由于存在纳什均衡, 这些参与人策略最终会收敛到纳什均衡策略, 因此会进人纳什均衡局面. 例如, 在前面的例子中, 假设甲乙都是理性的, 他们也知道表1 的信息. 如果智能合约预计会进人到非纳什均衡局面0 2 ,6364 ) , 乙会将策略从6364 改变到, 因为他的效用值会从1 0 提高到1 〇〇, 但甲的效用值会从1 0 降低到 1 0 0 . 但智能合约预计又会进人到另一个非纳什均衡局面( e2 ,e3e5 ) , 甲又会将策略从& 改变到A , 因为他的效用值会从1 〇〇提高到〇, 处于纳什均衡局面( e i ,e 3 e 5 ) , 也就是甲乙都选择不合作.当然, 现实情况中, 可能由于参与人的非理性行为或者不了解效用矩阵, 会进人到非纳什均衡的局面. 但本文考虑的是智能合约本身的问题, 因此假设参与人都是理性和完全了解信息的. 在前面例子中,甲乙只有选择不合作, 显然这样的智能合约是有逻辑缺陷的.定义8 . 智能合约逻辑缺陷. 智能合约逻辑缺陷是一种使得参与人效用小于或等于零的纳什均衡fe, 也就是; 存在参与人en , 他从纳什均衡, 获得的效用小于或等于零, 即& ( , ) < 0 .基于状态变迁图, 我们可以通过计算纳什均衡来识别出智能合约的逻辑缺陷, 然后自动分析出智能合约的优劣. 然而, 状态变迁图存在组合爆炸的问题. 图中的结点数量与合同中承诺数量成指数关系.当合同承诺数量较多时, 将难以得到分析结果. 接下来, 我们将讨论如何提高计算纳什均衡的效率, 这主要通过简化策略形式来实现.5 策略形式的化简给定一个合约, 其策略形式本质上是状态变迁图中各个结点的策略集合得到的笛卡尔积. 因此, 对策略形式的化简, 首先考虑的是对状态变迁图进行化简. 此外, 我们还将讨论, 如何在生成策略形式时,避免生成冗余的策略组合.本节将首先介绍“ 等价策略” 合并原则, 在此基础上提出两个基于该原则的化简方法: 基于效用值相同叶结点的化简方法, 以及基于独立承诺的化简方法. 接下来, 我们将讨论一种新方法, 该方法可以突破等价策略的局限, 对状态变迁图进行进一步化简. 最后, 我们将提出一个发现冗余策略组合的方法, 避免一部分冗余策略组合的生成.5 . 1 等价策略合并原则在经典的博弈论理论中[ 6 ], 等价策略合并原则是最为常用的对策略形式进行化简的方法.定理1 . 等价策略合并原则.一个策略形式〈? ,]^ ,( 认),( ^0 〉, 若对于某参与人々£ ? 的两个策略(0丨和(0】,u ( co1^ co N )= u ( co1, CON ) ,M (t)tGO t ( i即给定其他参与人的任何策略, 分别与W 和W构成的两个策略组合, 这两个策略组合的效用值对于每个参与人均相等. 注意: 对于一个策略组合y=( CO ! ,? ? ?, CO N ) , M ( y )= ( M! (>〇,…, MN (>0 ) 是一个JV 维向量, 表示所有参与人在策略组合y 上的效用值.根据文献[ 6 ] , 若W 和W 满足上述条件, 则任何两个策略组合y 和y', 若K e y 且W e y', 则可以将7 和, 合并为一个策略, 而不影响纳什均衡的计算.当只有两个参与人时, 上述条件成立等价于效用矩阵中有两个相同的行或列, 因此也可以将其称为“ 行( 列) 相同合并原则接下来, 我们讨论利用这一原则对状态变迁图进行化简.離劑等I.霜1 期 于靖计禅衡的臂俱脅约缺陷錄 1 5 55 . 2 效用值相同叶结点合并方法定理2 . 效用值相同叶结点合并规则. 若多个叶结袁1 x4〃, 4 属T 同一个非终止状态靖京的孩子, 且这些叶锘点上每个参与人的效用^值都相等,》则将A, 心合并将不擧响纳什均衡的求解,M 明. 东鬼一般性, 设参与人为甲, 设〇,? ? ?,I 分别为从父结点转移到込,…. 4 的事件( 也是甲的动作.) ? vy e:1,…, 假设y, 和广为任鴦两个分别但當e, 和9 的策略摄合, 且y,■ 和A 除去e, 和A之外其余部:分完全相肩: , 即y, /e,=乃/ q ;若A 和6 在策略s 合中均不生效( 没肴包含在:对应的动作序列中) 和乃必然对应相同的执行路辏* 效用值相若為和¥有一个生效, 说明y; 和y, 对觀:的动作序列将到达U… 丄的父结点, 则私和&/都会生效.因此y, 和乃对處的动'作療細必錐霉ii: 于?和% 指向的叶结点, 效用値也相同, 因此y; 和y ,的效用值必然相等, 按等价# 略合并原则, 将y, 和7, 合并将不影响纳什均衡的计算证毕.依据定理L 我们可以将fl3 中左侧的两个叶结点予以合并.( 1 0, 10 )( 1 0, 1〇)( 1 0, 1 0 )图:s僮相同叶鐘查翁行化# 的树子定理3 . 内部勘i 会并规剔. 碁多个肉部緖点赞1,?  ? , ) &封盧歸一个參%人, 它似均只有一个幾子结点, 且它们的孩子结点为同一.个奸结点, 则a ,…,篇? 可以合同样不影响绡什均衡的求解,证明过程类似定理2 , 限T 篤幅, 略去细节?依据定:理t 我们可将图3 中右侧图中倒数第二层的两个结点手以合并,S.3 基于因果独立关系的化简方法1 因果囊系和眉果:独立根据前面的分析. 我们知道例1 的合约是存在漏洞的, 不利于建宜双方长期合作. 原因在于没有对乙的行为进行约束. 因此, 我们现在对例1 进行完:善: 仿照支付宝和以太坊的思路, 加人鸯金盟眷. 购书款先存人到合约地址, 当乙履行发货义务》才将购书款转给乙? 修改后的食钧承诺如下?例2 . 第二版购书合同. 甲承诺在3 天将书款1 0 0 元存人到合约账户; 乙承诺在甲付款1 天内发货; 甲承诺在乙发货7 夫内确认收货f Cb nt rwr t 承诺在甲确认收货1 天构将书拿转账翁K〇:nt r?t :素诺在; 乙违约( 不发货. ) 1 天内将书款逭. M 给味.法套'Co n t rac t 的讀作暴智能合對代碎规:窠的,一旦前提满足, 就必然会执行, 因此Co nt a c t 不会出现违釣.观察例2 中的承诺, 我们可以发现一些承诺之间存吞依赖? 比如. 承诺A 的前提包含了C\ , 因此必须等CV 进人终來态之薛才能判断Cr是杳可以进人6k 状态- 下面, 我们引人因.枭关系的概念来描述这种依赖关篆.定义9 .嵐果薦{ Car s s lG r ap h ) , 给定一组癒诺CC , 其相应的因果图G 定义如下:( 1)CC 中每一个承诺C,对座G 中一个顶京!( 2) 如果一个承诺q. 的前提中包含C; , 侧在G中有一条有:向边从猎向q ..圏4 麗示插是衡2 中承:诺斯对遽的面果斷C\ (^ ,3 ?0 ? d ep o s ilC Con lr a c L,1 0 0) , (〇〇,3 ) )C2^ y C\. sa i -,d e live r (. bo o k -,, ( 3 ? 1 ) )C3 (伊, 乙, 〇2 . 犯“ c ow/^r m( r e cei v e一b o o k) , ( 7,7 ) )C4 {. Con Lra c L . s a LyLr an sfe r i Z ^ 1 0 0s) ? ( 3 0? 1 ) )C5 C Con Lra c L^ ^y Cz . vi o^r efund ^1 0 0s),  ( 3 0,1 ) )定义1 0 .震果養系( Ca r :sal Re l a ti o n ) , 給定两个承诺C, 和CV 定义C, 和A #在因果潷系S 且仅当在因巣圈G 中存在至少一条路径连接CVf C,. 若G 和C,不存在因果关系s 我们称它们是國果独立Ccar gal hi<fcpe nd e nt ) 的, 或’筒称猶立?注倉, 随翁合约的执行,某些承诺的状态可能发生改.变s 若一个承诺G 进人某个绛止态, 我们须将&对应的顶点和与萁相连的边都从G 中删除. 西此, 可能存在C; 和原本存在西果关系, 姐当含约执行到某个状态时它们变成了独立. 如图4 所示,C4 和C5 本乘基_ 在因:襄蘇系韵, 但如蔑qr遊人了终态並腿'中驂去. 则c4 和&独愈:*1 5 6 计導机攀报 :_1苹g . 3 . 2 黧会状态转「移若在茵果固'中存在一条从G 到C, 的路径, 则G需要等待G 的执行结果才能发生状态改变, 但如果C; 和C, 是独立的. 则它们的状态改变可以以任意顺序发生. 例如. . 膜设莲前合约状态为h 弁痕设此时C, 和C, 都可以发生状态改变? 假谗事件使得承诺Q 发生致变S[ 起犹态转移& :gA )—幻, 使褥承诺々意生愈变, 并引起状态转移& :yt也就是说, 通过状态转移序列可将合约状_ 从S 转变到& ? 同理, 若我们先玫变Crrlf 政变C ,, 也就是执行状态转移序列& 及,一样可以将合约状态从|转变到上面的例予可K 看迅当相互独立的承诺发蛊状态敦变时, 我们可以将_ 个状态玫蜜含舞到一起, 避免腾开不必粟的状态转移序列_ _ 于状态变迁倒中一个结点只有一个动作人, 我们在合并状_韓_ a#慕求被合# 的状寒转黪由據一? 动作人发起.定义1 1 . 复賣栽态:转務tG 〇m bin;e4 T Tr aus i ti pu ! )',设合约状态为s , 给定一组两两独立的承诺Gm# f £; ?K俄k £) , 若參些承诺此时均能:翁生牧态改变. 不失一般性, 假设这些承诺依次改:变状态,产生的状蠢转穠# 列海蠢, in…, s:雜量终:得到合约状态且这些状态转移对应的事件分别为:C…S 6丄我们可以将这些状态转移合并为一个:ft合状翁转移咨?? [句:,為,…, em ] )? 这里,[ ?! , 咚,…] 袭示途:饥个参:件的任蠢排列?需栗指出对于彳A , e2,…, gj* !_任蠶'— 个序列因为这些事件可以在状态s 时独立发生, 其顺序不会影响结桌.虜5 的左侧展示了根据例2 承诺生.成的状态变迁图的一部分? 可K1看到当Cs 进人如状态之后, C4和CSl1f 以独立改变自己状菰当事件f mw/e r 发生, C i从2 歲靈到3; 当_ 件ii ?柳CG ) 发生>Gr从1 玫:变:蘭t 孤— 中苛以,看到, 这爾个攀件产生的苘个序列, _终得到相同的结果. 诨此, 我们可以将这两个状态转移合到右边的图.定理4 . 基于复合状态转移的化简原则. 当状态变迕画的锫点^ 存在一组两两独立的承诺■I  C!,…, 按窝义1 1 将t, 的多个状态转移路径合并太一个复合状态转本会影响纳什均衡的计算结果.证明. 设化简之前的状态变迀图为C; , 通过一个复合状态转移# 对G 进行化商之后的状态变迁图为G '. 设y 为任袁^-十由G ' 生成且包含的策略组合? 则y 在<3 中对愈唯■一■ 条动作:豫到j〇指向叶子结点夂其对应的效用?值为《■ ( /) ?设在G 上对应的事件f列集合为[ , ] ? 并设P 在6 上对应的路径菜合为P .若不在P 上> 则任何屬于[e?] 的事?:件序列都不会出现在任何一条P 的路径上.署s? 在p 上., 则麗于[ e?〕:的事秤零_ 都在,P 的某条路径// 上. P 和/ 的畦一塞别在复合状态转移部分, 它们将指向相同的叶结点? 也就是说, 包含这些序到的策略组合, 其效用值均为《( / ) .根据雩价策赂合并厳则可证.证毕.化简效果分析. 若一个状态S 包含A 个独立承讀, 那歲未化筒前的状霧变:迁围将产生H: 个状态翁移序列, 钽是化简之后, 这幻个序列( 路径) 将被合并为1 个. 因此. 窟遲4 可以大大减少状态变迀图.结点的数量, 也将大幅降低策略形式的数量.S. 4 基于纳什均衡等价的化简方法之前讨论的化简方法的?础都S等价策略( 行列相同1 贪并原则. 但是等价策略合并不是方能的■菌6 ( a) 的例子中, 结点C 、D 、E 结构非常类似: 有柑同的父结蟲A; 孩子結.点都是_F 和:G * 且转移到F或G 的夢件也相同. 我们着蓬将C、D 、£合# 为一个结点, 如图6 a) 所示.( a ) 原始图( b ) 化简图图S 我― 变t?=聲价图0 ( S) 的效用矩阵如表2 所示c羞中黑体部分为纳什均衡的策赂组合5 . ■ 我们分析其效用矩阵时, 发现并不存在相同的行或列? 无法适用S , 1 小节里的等价策略原则( 也就是行列合并原则) .離劑等I.霜1 期 于靖计禅衡的臂俱脅约缺陷錄 1 5 7表2 图6 (: a3 的效用矩阵乙甲ei % e3e4e5 ( C) e5  ( D )e5  ( E ) ( 40,4 0 ) ( 3 0, 3 0 ) ( 3 0, 3 0 ) ( 3 0, 3 0 )e5 ( C) e5  ( D )e6  ( E ) ( 4 0, 4 0 ) ( 3 0, 3 0 ) ( 3 0, 3 0 ) ( 5 0 ,5 0 )e5( C) e6 ( D )e5 ( E ) ( 4 0, 4 0 ) ( 3 0, 3 0 ) ( 5 0 ,5 0 ) ( 3 0, 3 0 )e5( C) e6 ( D )e6 ( E ) ( 4 0, 4 0) ( 3 0, 3 6) (5 0 ,5 0 ) (5 0 ,5 0 )e6( C) e5 ( D ) e5 ( E ) ( 4 0, 4 0) (5 0 ,5 0 ) ( 3 0, 3 0) ( 3 0, 3 0)e6( C) e5 ( D )e6 ( E ) ( 4 0, 4 0) (5 0 ,5 0 ) ( 3 0, 3 0) (5 0 ,5 0 )e6( C) e6 ( D ) e5 ( E ) ( 4 0,4 0) (5 0,5 0 ) (5 0,5 0 ) ( 3 0,3 0)e6 ( C) e6  ( D )e6  ( E ) ( 4 0,4 0 ) ( 5 0,5 0 ) ( 5 0,5 0 ) ( 5 0,5 0 )但是我们规察化筒图的敏用矩阵, 发现一个有趣的现象.首先,,虽然不能适用行( 列)相減会弁原则, 但是在: CDU 二个總獻乙采取的策略是變金:相同的:选择则到达F , 选择e6 则到达G .其次,在化筒腾中得到两个策略组合<_ 中黑体标识)? 如_3 所示> 其中左上角的策略组合!e 5 邊}与表2 左上角的策赂组合相同? 在表2 中该組合也齿傭什雄衡点. 右Tfl 的策略組# : :, 炫| e3| | e4 }其他部分保特,不变. 例如化简图中路径甲^1^ 乙上G, 对座原图三条路径, 甲J 乙上G, 甲上乙上G 和证明.( a ) 设基于定理5 的化简图计算得到纳什均衡点y , 且/ .在化简' 图中对虛播径(〇. 将p 中可翁翁作集%I I…1 1 ? 拆开., 可锝到原? 中的路径集合八〈亨表示任翥动作序列) ? 既然I I…lk?:k) 满足纳什均衡条件, V 丨e U 严,_), y,=亨. e I:;e丨也必然橋足.(> 4=)V / I?i2 61 1 ?. ^<*, m, \y , i=fe a e]是纳什均衡處# 注意'y.aFe丨和; 2e) 是__京妒之后才分开, 不■ 妨假设的动作人为甲, 对乎甲在h 的策略集, 其他人的最优策赂就基版棋? 而和私》氣别仅银隹:擎私在敏点?>?来取了《n , 而5% _爾点采敢了《, 2.g 为甲的焉詹动作均为它们的敏甩值是一样的, M 此, 7, 3也必然是纳什均銜点? 这样我们就得到, ll .- '. m },含置:暴寧在eg 、a 或e 4 中任遨一个, 乙始终通择ft.可以遂一验证, 这个策略翁含与表2 中标为黑体盆價綠CJfl , 5 0 ) 的1 2 个筆略龜合=:是一致齒? 比如!e 6 ( Q 物为甲选择了吟, 乙昀會—动作_梟e6 ( S';), 也榦是:斑可歇筒化为1 e6, % }.表3 图6 ( b3 的效用矩阵乙甲^1eze4它5 (4 0,4 0 ) ( 3 0,3 0)它6 ( 4 0, 4 0 ) ( 5 0 ,5 0 )最后, , 我们观察: ^ jbI 04  1■ 所对应的执行路径( a 中加粗的箭头所示) , 该路径在遠图中对虛三条执行路径 <同_遍加耝— 决_獻5 f餐身:讓征? 这三条路ft对處的策路组合均为纳什均街点.基于以上观察, 我们提出以下基于纳什均衡等价的化简方法.定理5 . 塞于纳什均衡等价的化简规.则. 若结處参合,?  ? ? :s% Cw> 1 ?:有_一个父拿_:蟲到,4= 1,… 的动作分别为e,: ; V 泛U ,…, 稱} ,v潘翁乎_嚴_:合均为% ,?  _ * ;, 4( 叶结處》,: 铒到j(j=1 、…, _ 动作为? 且焉. 餘潘作执行人相隊? 厕可将W 费并为一个绪点1? 到》的:动作为fti I…| |u, 到孩子象歲的儀作为g f说明: 依据定理5 进行化筒, 我们将得到包含可选动作》例如趦卜, k 的执行路径,,其在原图中对应坊个路轻? 即将奐I…| |?拆开成单独的动作, 而7,= 砰#;, 这些策略11 合要么都是纳什均衡点■. 么都不是纳什均衡点.若:策略癒脅藤ty,=f&ejU =1 , ?抑!■:中每一个者I是纳什均衡虚, 容S曼出y=9? t% 丨丨…I  ?? > *: 丨也必然满足纳什均衡条件,若策略组含集i y,= - U= 1 ,…, w ) 都不是纳什均衡点遍依据( 4 )猶遨否金题:, y=Y ( e i| |…I e,?  ) e;'也不'可能是纳什均衡点,证毕.讨论:? 经过上述化简, 状态转移图的规模大大缩小, 但是在基于状态转移图求纳什均衡的过程中依然遇到了很大问。题. 原因.在于求策略褒式过程中,_票做两次笛卡命积. 揍下来, 我们将从另一个角度来简化策略形式, 即在'构建策略组合时* 避免生成宂余'餘麗合.S. S 冗余策略形式化简依据策略形式的'定义, 我们瓣笋计算一个参与人在所有内部緒点的动作集合的笛卡尔积, 以得到谀参■ 与人所有策略. 例如獨甲的所有策略为'! 衛色% 過% ,1■, 即甲_< 4 的翁作:寒翁'!  ?J, e2}嵐?'冗余乘略藤式雛子1 5 8 计導机攀报 :_1苹与他在S 的动作集合;, e4 } 做笛卡尔积.从画? 中我们发现, 如果甲在锫点A 选# 3*e2 , 那么參作释., 《* 必然不舍!生敏* 囡此■ : 可能是冗佘的? 基T 此观察, 我们提出卞肩的化筒方法?BS意到一个动作《实:顯对處狀盡变迁图隨一蠢斑, 为了便子播:述不翁设?■ 的源爾il为( <? ) , 目标翁森海定理6 . 菪某动作人在:不同错点有两个策略為和暴抓(4 ) _ 祖先, 且,不在以rf st ( e a )为根的矛树中, 则所有:同时& 貪( 和4 的倉略缀合都是冗佘的.证明. 假设一个策略親■含7 同时包含 ̄和% .着a 生、效, 说明y 对虛的路轻将经过边‘ , 由于巧不在以办> 为根的子树中, 则今不可能生效.那么y 可以被另一个吏短的策略组合y / ,替代.若%4 效, 说明y 对应的路径将经过边峰, 则也不可能生效? 那么y 可以被另一个策略组合y / c眷代?着私和4均不生效, 则y 可以被另一个策略组合y /'! 蜷% 》餐代.综上所述. 任何同时包含& 和% 的策略组合都是冗余的.证毕.实际应用中, 策略组含的数量可能非常大, 难以在短时间内全部构,造. 出来. 上述定:理:可以帮助我们避免& 成不必要的策略组令, 而不是在:生成所有策略_合之唐再你筒,6 系统实现和实验分析本节将首先介绍:我们开发的一个用于智能合约建模、分析以及部.署到K块链平台的工具, 接下来介靖我们对一组真实合同分析的结果, 以及我们所提出方隹在性能提升方面的表现.6 . 1 系统介绍我饤开崖了一个用于智能合约建模、分析及自动部署的工具. a& 是部分截画? ( a ) 麗示T一个合约的编辑界面, 用户可以输人合鈞的承诺、系统会自魂屣现承诸之间的依赖关系( 因果依赖围h( b*) 展.示的是将一个合约負动部署到Fab ri c 平台的运行错果1(e ) 是合约分析界.面《■ 用户可以看到根据合约承诺自'动构建的状态变迀图, 在输人效用值之后, 还可以S 动分析合约的纳什均衡点, 其中黑色文字樞胰示了合约的一个执行路径? 我们的工具还可以自动稂据状态变迕图生成智能合约的代码, 例如H y-per l edg et  F ab r i c 链码, 爾户:?其中鄯勢动作函数补充完*:之后, 就可以使用我们的工具将含釣部署到Faliric 半舎上?tr vc,  tc ken-:? cy 3-6 Cc *j ?l J r J *I l' f. :5lni !cC I 5 :J< p !r 〇l ] 9 .?yn e Kt OJL OC T ai- Ns Cii ! :? CA V H l J: jD i' <W t *l 5 f V 2 ?t f Z Z rV :i in f> 3 Jn h ift Z S l'JIk iH Z3 l 5 l r,3 v b 〇LH C t J*2C lp rfa i d ira r jn vj V T r n M f r.  *<m i i'; i vrf n n /ft? x_'> n ? . n j*_/ n i - 14jn i i rCi i ii K iM'}( a ) 合约编辑 ( b ) 合约部署我们采用了经典的Lemk e - Ho wson 算法[1 5] 来6. 2 有效性实验求解纳什均衡.依据《中华人民共和国合同法》( 1 9 9 9 年3 月1 5 日隊膂_ 雩?.基于靖什埒衡的脊鱗脅舞缺騎翁興 IS  1 期 9颔布h 常见的合同课有異卖含苘、供用杳同、赠与1合同等I S 粪? 我们参照华律网( 6 6 k w. ci i ) 和食同帮(上etoii g b . C DlA) 爾,个网站齡合:_審本# 使爾我们'开衆的工具.#其中14 类合同迸狞了建模和分析?A有居间合If厨愈渉及到参方參与f 暂时不变持.我们总计对1 4 大类.SQ 个合同进行了建模和分析. 弁裉据分析结杲将这些含而分为H个等级?暑^个纳什均衡点*秦与各方敏用( 收益:) 掬为'零, 我们称为全零^奢参与备#效用均为正, 称为全定| 蓉有述有负, 称为fi负; 这三舞之外的|3iv其你?如菌& 所每V在合同范本中s 大部分含同质?量是合格的, 其中有3 5 % 的食两达到了优秀? 这些食同中, H 为只有全攀和全正的纳什均衡点r參与#方会优先考虑'?'双赢”的博弈策略,? t 纳什瑜衡正mwi_聋s什均翁蟲麟鱗纖織崩I 会? 分析_*姐我们也看到., 有4 1 °4 的含同存在丨可题. 这些含词中, 大部分是風存在全零的纳什均衡点? 此时,參与.方在综食利弊之启, 将裉可能选择不參与博也就最不执行合屑.下面我们分析一个评分为4差” 的合同.合同实例: 清费寄托合_C,< 申: 乙,, gv寄物品Hftf寄托蠢>(7 ,i>:)02 ( S? C, .a?j? (,m , 1 3  iGrf;£* 甲, 〇s , j?, 薇用:青托物, C〇8? S D XJ"( 乙, _?忍: ..》#&寄托满和天)!? 退速: r? ))潸费寄托食同: 的含义是寧方将货物寄托在乙方处, 弁支付寄托金* 乙方可以在:寄托期间便用部分寄托物品( 比如煤炭八隹是靖寄托期满, 乙方必摩f 补足IS有物品數蒸#妇还给甲方?上雄合约的含X慕; 甲方将物品寄托铪乙方并且付给.乙方s偏〇■ 焉會托费fd.乙方决定备费爱颔寄托物( cy . 乙言可以自由消费寄托物( c& ) ,姐是必须.在寄托时间到期C* : / ?#e 爾数调用预盲机实现) 后将脊.托物全额返.还给甲方.如果一开始甲方'就将物品寄托_ 乙方, 直方受?均为〇. 或者审方想要将物潘寄托给&方是乙方木受领寄托物, 双方受益也均为0 . 但是S寄托物一旦成功寄ffi it s 乙方苜以自_ 选择聲否执行?承诺c4 ? 如皋乙方违约, 不将寄托物返还给甲方, 这能使乙方自H 获傳更高的收益?輿此? 上述合同R有全零的纳什均衡点, ¥如果逸择寄托物品, 那么作为理性的博弈参=¥人, 乙将选择使g 己收盘鱟大的策路^违纨那么审在分析利弊之唐*最好的对策甚?不哿托物品- 也就意味:#脅同根本本'蠢裱执行? 意獅奮獅到f5緊方麓S健乘蕾要指出的是, 我们通过自:动分析,发现很多僉同范本都存在上述问题?jt有对某参省方的违约行为予以惩罚? _ 么含同是杏:顺利执行可能A有取决于该参与方的通禳水平或街律泝费? 从商务合阏的原则来看, 这显潘是不合理的?可以_ 出, 我们撻m 的建镇方法賓m'对现实中大多数合同进行建模旦,基于傳弈论对合同自箭分析能够黛;现潛在雷逻辑缺陷(不公平的* 匣.6 . 3 效率实验我们按状态靖處数薫将合同分为吗类馮京载量分别为[ 1 *孩〇] , [ 51 , 10 0 ] , [ 11 11, 2〇£ 1 _ 茇[ 2: 0 1si# .状态緖点的数量讓本反腴了合词的复杂1程度.我们1对比了迪类:方法t( 1 〕DF A 方:法<奉用靈本的智能合约建模方法s末做任何化简.(2 3 SE方钹. 暴f策略尋费( StrategyEgt ii va:-l e fi&e.?, SE )原则对状态变.迂图进行化简.⑶ SE + N £方法. 莱用了SE 方法和纳什讀衡馨价攛则tl% s h Ecjuiml?iiee-; tM U) 封状盡变迁: 圈化简.f 43 SE +W E + R S 方法? 采用以上商:类化简方祛碁機上屈編用了55南策略紙会化筒方掛CR edu nd a ntSt iat e gy?R S ) *下W我们分规从状态结處个数、策略级合个数以及计算纳什均衡时隊三t 方爾验te我们靳提出方麵有象性,IQ 对比:了D FI SE :和S E + SE 这三种方'法在四类合同中产生的状态緖点数量, 可见随着合闻趋宁复杂, 化简友法效果越明適. 特别地e 爵杳同较为复杂, 化崎之后的结滅:栽量R 有化筒前的约1 射.翁宁#后一种化筒方铢( R s y并不会减少状态録点个数, 我们没t 在菌1〇中列出来.接下_1 , 我们猓人分折3种化简方法在计算纳什均衡过程中的效果《由子I5F A 方法.只能计算出1 6 0 计導机攀报 :_1苹1 0s1 0*1 031 021 01极少数_ 常简攀費同的纳什均衡, 在窟綴分析中, 不再列出DF A 方法的结果?厲'1 1对比了SE: 、SE+KE和SE + NE+RS 这三种方法:在四类合同中产生讷策略组合数量( 对数藥标> , 可以明显看到,嚴如了冗佘策略化简之.S ?策略组合数量明显下降, 对于复杂的合同, S E+ .KE+RS 方法的策赂组合数比S E + JfE 方:法少了6 个数量钣, 而S E 方法将会产生极多的策略组合, 以至f根本不能在有敢时向内计算出纳什均衡.[ 0, 5 0 ][5 1,1 0 0][1 0 1 , 2 0 0][2 0 1,■?]图1 0 狀态结啟个数1 〇2。。1 〇1 5 01 0?1 05。10°□SE■SE+ NE□SE+ NE +R SH-][0, 5 0 ][ 5 1, 1 00 ][1 0 1 , 2 0 0][ 20 1 ,° °]丽:11 翁略组脅个数圈1 2 巖示了晦簾合同中SE、S E + NE 和SE+J I E+R S 这兰种方法在计箅纳什均衡耗时的对比( 对数垄标可以看到, 疊加了冗余策略化简之后,计算纳什均衡的效傘同样大幅提升. 对于一些非常复杂的合同, S E + NE 方法_要趙过一小时籴求纳什均衡, 而SE+N E+R S 方法只需要几秒, 我们在该:实验中设置的最长时间为l h , 因此对宁S E 方法,其实际需要的时间远超过图中的数据.以上结果雇明, 我们所提出的化简方法. 可大幅度縮减计算纳什均衡所需的时间.7 总结和展望区块链使用智能合约描述参与各方需要共同遵守的规则.一旦合约中存在漏洞问题, !?往就会'带来巨大的损失, 因此智能合釣缺陷检测成为了受到广泛关注的研穷向題■ 然而, 现在区块链的智能合钧并'没有统一的编程语言和运行模型f一般看寒由不檀计算机编程语言的管理人员负賣智能合约的创建和樟测? 针对这个问题, 我们之前的‘工作提出了一种编程语i 无关、易于:理解的智能合约模型/本文中, 在这个合约模複的基础上, 我们琅式化.定义了智能合釣的博弈问题, 然后提出基f纳什均衡的漏洞检测方法〖并提出了一系列的策略濟式化简算法, 实前高效的缺陷检测. 此外, 我们实现了一个图琅化的工具, 可以对智能合约进行建模、分析和部署. 最后通过实II 对方法的可,厨性和效率进行T 验it*末来我们将进一歩完德建模方法, 京持更复杂的语义. 也会研究基于机器、学习来求解纳什均衡的方法, 以支持實:为'复杂的合同参考文献[ 1 ]Sz ab o N. Sma rt  co ntr a cts :Buil d ing  b l o cks f o r d i g it a l ma rk et s .EX TRO PY : The Jo u r n al  o f Tr an s hum ani s t Tho u g ht, 1 9 9 6,1 6 :[2 ]Lu u L , Chu D -I I , O li cke l I I , et a l . Ma ki ng s mar t co nt r a ct ssm ar te r / / P r o cee d i ng s  o f t heACM SI GS ACCo nf er e nce o nCo mp u t er  and  Co mmu n i ca ti o n s Se cu r i ty  ( CCS’1 6 ). Vi enna,Au s t r i a ,  2 0 1 6 :2 5 4 - 2 6 9[3 ]Minis t r y o fI nd u s t r yandI nf o rm a tio nTec hno l o g y . W hiteP a p er o nChi n a?sBl o ck cha i n Te chn o l o gya ndAp p l i ca t i o nD ev e l o pme nt,O ct o b er  2 0 1 6 ( i n Chi ne s e )(工信部. 《中国区块链技术和运用发展白皮书》, 2 0 1 6 年1 0 月)[4 ]W ang P u-W ei , Yang I l a ng-Ti a n , Me ng J i , e ta l . Fo rma ld e fi ni ti o nf o r  cl a s s i ca l sma r tco n tr a ct s a nd r ef e r ence imp l e?m ent a tion. Jo u r na l o f So ft wa re , 20 1 9,  3 0 ( 9 ) : 2 6 08-2 6 1 9 ( i nChi nes e)(王璞巍, 杨航天, 孟佶等. 面向合同的智能合约的形式化定义及参考实现. 软件学报, 2 0 1 9,  3 0(9) : 2 6 0 8-2 6 1 9)[5 ]De s ai N, Cho p ra AK ,  Si ng hM P. Re p r ese nti ng  and r eas o ni nga b o u t co mmi tm ent s  in b u s i n es s  p r o ces s es / / P r o cee di ng s  o f t he2 2 nd  AAAI Co n fe r en ce o nAr tifi ci a l  Int el li g e nce. Va nco u ve r ,Ca na d a ,  2 0 0 7 : 1 3 2 8-1 3 3 3陈晋川等: 基于1 期 纳什均衡的 智能合约缺 陷检测 1 6 1[ 6 ]O s b o r neM J , Ru b i ns t ei n A. ACo u r s ei nGa meTheo r y .USA : MI T P r e s s,1 9 9 4[ 7 ]Yang Z , Le i I I . Fo rma l p r o ces s v i r tu al ma chi nefo r sma r tco nt r a ct s v e r i f i ca ti o n. I nt er n at i o na l J o u r na l o f P e r fo rm ab i l i tyEng i ne er i ng ,2 0 1 8,1 4 ( 8 ) : 1 7 2 6- 1 73 4[ 8 ]Bi g i G, Bra cci al i  A, Me acci G ,et  al.Val i d at i on o f d ecent ra l iz edsma r t c o nt ra c t s t hr o u g hg a me t heo r y  and f o rma l  met ho d s //Bo d e i C ,Fer r ar i  G, P r i am i C ,e d s . P ro g r a mmi ng La ng u a g eswi t hAp p l i ca ti o n s to Bi o l o g y a nd Se cu r i t y , Le ct u r e No te s i nCom p u t er  Sc i en ce 9 4 6 5 .C ham : Sp r i ng er, 2 0 1 5 ; 1 4 2 - 1 6 1[ 9 ]Mav r i do u  A *La s z kaA. De s i g ni ng s e cu r eEt he r eum sma r tco ntr a ct s : Afi ni t e s t at e ma chi ne b as ed a p p r o ac h/ /P r o cee d i ng sof t he 2 2 nd I nte r na ti o nal Co nf er enc eo nFi nanci a l Cr y p to g r ap hyand D at a Se cu r i t y ( FC2 0 1 8 ) . Ni e uwp o o r t, Cu r a ca o,  20 1 8:5 23- 5 4 0[ 1 0 ]Ga o X , S i ng hM P .Ex tr a ct i ng no rm at i v er e l a t io ns hi p s  fr o mb u s i nes s co nt r ac ts / /P r o cee d in g s o f t he I nt er nat iona l Co nfer enceon Au t o no mo u s Ag ent s  a nd Mu l t i a g en t Sy s t ems  ( AAMAS ) .Pa r i s , Fr a nce , 2 0 1 4 : 1 0 1-1 0 8[ 1 1 ]Si ngh MP , Cho p r aAK. Cl o u s eau : Gener ati ng co mmuni cat io np r o to co l sf r o mco mm i t men ts // P r o c ee d i ng so ft he3 4 thCo nfe r e nceo n Ar t ifi ci al In te l li g e nce ( AAAI ) .NewYo r k,USA ,  2 0 2 0[ 1 2 ]De s ai N * Na r e nd r a NC , S i nghMP .Chec ki ng  co r r ec tn es s  o fb u s i ne s s co nt r a ct s v i a co mmi t me nt s 一/P r o ce ed i ng s  o ft he 7 t hI nt e r na ti o na l J o i nt Co nf er e nce o nAu t o no mo u s Ag e nt s a ndM u l t i ag e nt Sy s t em s ( AAMAS2 00 8 ).Es t o r i l , P o r t u g a l ,2 0 0 8 : 7 8 7- 7 94[ 1 3 ]Cho p r aAK , O r en N , Si ng h MP ,e t a l .Ana l y zi ng  co nt r a ctr o b u s t ne s s t hr o u g h am o d el  o f co mm i tm ent s // P r o ce ed i ng s  oft he 1 1 t hAAMAS In te r na ti o nal W o r k s ho p o nAg ent O r i e nt edSo f twar e Eng i ne er i ng ( AO SE) .Be r l i n, Germa ny , 2 0 1 1 : 1 7- 3 6[ 1 4 ]Ad l er J , Ber r y h i l l R , Ven er i s A ,e t a l .As t r a ea :Ad e ce n?t r a l i ze d b l o c kcha i n o r a cl e/ / P r o ce ed i n g so f t he2 0 1 8 I EEEI nt e r na ti o na l Co nf er e nce o n I nte r ne t o f Thi ng s ( iThi ng s ) a ndI EEE Gr ee nCo m p u ti n ga ndCo mm u ni ca t i o ns  ( Gr ee nCo m )a nd  IE EECy b er,P hy s i c al  and  So ci a l Co mp u ti n g ( CP S Com )a nd  IE EES ma r t D at a ( Sm a r tD at a ) . Ha l i fa x, Cana d a, 2 0 1 8:1 1 4 5 - 1 1 5 2[ 1 5 ]S hap l ey  LS.A no te o n t heLe mke-I Io ws o na l g o r i t hm/ /Ba li ns kiMLed . Pi vo ti nga ndExt e ns io n :Ma t hema t i ca lP r o g r a mmi ng  St u d i e s ? v o l1 . Be r li n , Ge rma ny : Sp r i ng e r ,2 0 0 9[ 1 6]S u r ek a A, W u rm anP R . Us i ng Tab u  b e s t-r e s p o ns es e a r cht ofi nd p u r e s t r at e gy Na s h e q u ili b r i a i n no rma l fo rm g a me s / /P r o ce ed i ng s o f th e4 t hI nt er nat io na lJoi nt Co nf er e nce o nAu t o nom ou s Ag en ts  and Mu l t i ag ent  Sy s t ems  ( AA MAS2 0 0 5 ) .U tr ech t , TheNe t her l a nd s * 2 0 0 5 : 1 0 23-1 0 2 9CHE N Jin-C h uan , Ph. D. ,a s s oci a t ep rofe s so r.His ma inr es e a rc h i nt e re s t sin c lud e dist ri bu t ed  da t a mana g eme nt  an db lo ck c h a in.XI AHu a-Hu i, M.  S.c an di da t e.H isma in r e s ea r c hin t e re s t s in cl u de b lo c kc h a in  an ds ma rt c o nt r a c t s.WANGPu -We i, P h .D. , a s so ci a t ep ro fe ss o r.H is ma inB ackgr oundTh i s wo rk fo cu s e so n th e p ro bl emof mod e ll in ga ndana l yz in gs ma r t c o nt r a c t s . Re c e nt y ea r s , s ma r t co n t ra c t s a ndbl oc k c ha i nb e c ome a h ot r e se a r c ht o pi c in d i s t r i b ut ed co mp u?tin g ,in for ma ti on  s e cu rit y , d a t a b a s e, a nds e r vic e  co mpu ti nge t c. Mo st wo r ks  re ga r d s ma rt  c on t ra c t  a s c omp ut er pro gr amsru n nin go n bl oc k c ha i n sy st ems. H en c e th es e s ma rt  co n t ra c t sha v e no th in g tod owi th “co n t ra c t s O ur wo r kt r i e s t obr i dge th e g a p be twe e nb us in e s sc on t r a ct s an dco mp ut e rco d es.Mor eo v er,int he mul ti- a ge nt co mmun it y th er e ha veb ee n man ywor ks o nmo de ll in g bu sin e s sc o nt r a ct s, orin t e r- or ga ni za t i o npr oc e s se s .Mo st  of th e s ewor ks a r e b a s edon th e com mi tme n tmo de l . Th e yt r yt od es c r i b eb u si ne s sco n t ra c t s withfo rma l mo de l s,an a ly z e th e c orr e c tn es s o fth epr op os e dmod el s,a nd d is cu s s ho w t outi l iz e th emod e ls t osimul a t e th epr oc e s s es of e xe c uting b usi ne s s co nt ra c t s.r e s ea r c hi nt er e s t si nc l ud e s er vic ec om pu tin ga nd bl oc k c ha i n.MA Na-B o , M. S.c andi d at e. His ma in re s ea rc hin t er es tsi nc l ud e dist ri b u t e dc omp u tin gan d bl oc k ch a in.WANGQi,M.S. c an di da t e. He rma i n r es e a rc h  in t e re s ti sb lo c k ch a i n.LI Hao- Ran, M. S .cand i da t e. Hi smai nr es ea rc h in t er es tsi nc l ud e s er vic ec om pu tin gan d bl oc k ch a i n.DU Xi ao -Yong , Ph . D. , pr ofe s s or. His ma in r es e a rc hi nt er e st si nc l ud e dist ri b u t e dd a t a mana g eme nt t e ch n ol ogy .Di ff er e nt fr omt h es e wo rk s , th e emp ha s i s  of th i sp a p eri s a bo utho wt oan a ly ze  th e lo op ho l es o f co nt r a c t s . Forth i s pu r po s e,we pr op os e ame tho d t oc omp ut e th e Na s he qu ili b riu mso ffo rma liz e d co nt r a ct s an d a s erie s of t e ch ni qu est os p e ed u pt hisp ro c e ss. T oth e be s t  of o ur k no wl ed g e,th iswo rk isth e fir s t o ne  tha ti l lu s t ra t e sap ra c tic a l p ro c e ss tode t ec t  lo op h ol e s of b us i ne s sc o nt r a ct sb a s e do n G ame th e or y.Th i s i s th e n ewe s t re s u lt o f ou rr e se a r c h. Pr ev i o us wor ks onth is t o pich a v e be e n p ub lis h ed i nICSE , T PDS , J ou rn a lo fSo ftwa re  ( in Ch in e s e )e t c.Th is wor kiss u p po rt e d b ythe Na ti on a l Na t ur a l Scie nc eFo un da t i on  of Ch in a ( No. U1 9 1 1 2 0 3 ) , and th e jo in tp rojec t sfro m Gu i z ho uCol l eg e ofF in anc e  and Ec on omi c san d Chi ne s eAca d emyof In t e rn a ti o na l T ra d e an dEc on omic sCoop e ra ti on( No. 2 0 1 7 SW B ZD 0 8 ) .

[返回]
上一篇:基于知识线记忆的多分类器集成算法
下一篇:基于句法语义依存分析的中文金融事件抽取