原文标题： 基于纳什均衡的智能合约缺陷检测
原文作者： 陈晋川，夏华辉等
原文机构： 中国人民大学信息学院
原文地址： 10.11897／SP.J.1016.2021.00147
发表日期/期刊：V0l.44 No.1 Jan. 2021/计算机学报
笔记整理：doxbwx@163.com
本文是基于形式化表达智能合约的工作之上对智能合约的逻辑缺陷进行检测的算法效率进行提高，文本旨在解决这些问题：
- 如何构建一种与编程语言和平台无关的，易于理解的中间模型
- 如何发现智能合约中存在的逻辑缺陷
本文的解决方法分别为：
- 基于之前文章的智能合约形式化模型提出了从承诺到状态机的自动生成算法，而为了进一步解决该过程中可能会产生指数级的数量巨大的状态问题，提出了一系列化简算法。
- 将多方参与执行智能合约的过程看作是一个多方博弈问题。将智能合约的逻辑缺陷定义为特殊的纳什均衡，也就是在纳什均衡点中，各参与方的收益全部为零，或者收益有正有负，则说明该智能合约可能存在逻辑缺陷。
智能合约建模
??例. 一个简单的购书合同．甲承诺在3天内付款100元，乙承诺在收到书款之后1天内发货。C1 (甲，乙，?，pay(乙,100)，(∞,3))，C2 (乙，甲，C1.sat，deliver(book,甲)，(3,1))。承诺C1表示甲向乙承诺，3天内执行pay(乙,100)操作，前提为?。承诺C2表示乙向甲承诺，当C1进入就绪状态时，乙会在1天内执行deliver(book,甲)操作，但此承诺约束为3天内。
确定性有穷状态机(DFA)形式的智能合约为下图所示
状态1为act表示激活，状态2为bas表示就绪，状态3为sat表示满足，状态4为exp表示过期，状态5为vio表示违约。
下图为从承诺到状态机的自动生成算法
策略形式的化简
??策略形式的本质是状态变迁。参与人使用的策略集合都是其在所有内部节点的动作集合笛卡尔积，要先考虑对状态变迁图的化简。
??基于效用值相同叶节点的化简方法和基于独立承诺的化简方法是在等价策略的基础上进行化简，有一些策略集合不适合用等价策略所以提出了一个基于纳什均衡等价的化简方法。
-
效用值相同叶节点合并方法.如下图所示化简。
-
基于独立承诺的方法。当相互独立的承诺发生状态改变时，可以将多个状态改变合并到一起。如下图所示从同一节点发出的多个状态转移路径可以合并为一个复合状态转移。如下图所示。
-
基于纳什均衡等价的方法。若节点集合有同一个父亲节点，且这些节点的动作执行人相同，则可以将这些节点集合合并为一个节点。
冗余策略形式化简
??正常的策略形式化定义，需要计算一个参与人在所有内部节点的动作集合的笛卡尔积，以得到该参与人的所有策略集合。但是实际上这样的策略组合数量过大，需要简化一些不需要的数据。若某动作人在不同结点有两个策略e_α和e_β，src(e_α)是src(e_β)的祖先，且e_β不在以dst(e_α)为根的子树中，则所有同时包含e_α和e_β的策略组合都是冗余的。例如下图所示，当选择了e_2时，就不应该出现e_2 e_3，e_2 e_4这样的组合，所以将这种冗余情况去除。
有效的实验及结果
??从图可以看出，在使用了上述等价策略、纳什均衡等价策略和冗余策略化简方法之后，所得到的时间效率以及最后得到的结果集数量都有了指数级别的优化。