基于模型检测的区块链智能合约公平性形式化验证

2021-07-27肖美华周浩洋朱志亮

华东交通大学学报 2021年3期

肖美华，周浩洋，朱志亮，罗敏

（1. 华东交通大学软件学院，江西南昌 330013；2. 江西省计算技术研究所，江西南昌 330003）

自2009 年中本聪[1]引入比特币以来，分布式加密货币已经获得国内外学者的关注。加密货币由用户在其网络中公开管理，且不依赖于任何可信方，用户采用共识协议来维护共享的数据分类帐（区块链）。区块链[2]技术因为其去中心化的特性为人们所熟知，同时，基于区块链技术更广泛的应用被人们开发出来[3]，智能合约就是其中之一。

智能合约可以对其编程语言中表示的任何一组规则进行编码[4-5]，其与传统行业的结合可以提高该行业的效率以及安全性。肖谦等[6]研究中国分布式电力交易的实际情况，提出了一种基于区块链智能合约的分散式电力交易市场框架。徐美强等[7]基于区块链技术设计了变电站数字化配置的自动化方案，提高了效率和安全性。刘维扬等[8]基于智能合约技术提出一种电动汽车入网竞价机制，在实现电网负荷削峰填谷的同时，有效保障了用户、代理商和电力调度中心的利益。

由于智能合约应用便利，大量高价值数字资产利用智能合约进行存储和转移，容易受到攻击者的密集活动影响。随着智能合约安全受到越来越多的重视，国内外公司和研究机构也在致力于寻找智能合约安全性验证的方法。 Bhargavan 等[9]将Solidity代码和EVM 字节码转换成F*，然后使用F* 类型检查来验证智能合约内存在的重大漏洞，但是其并不能完整的转换Solidity 代码。 Nehai 等[10]将智能合约翻译成NuSMV 输入语言，然后使用模型检测器对智能合约进行验证，但是其转换规则并不适合复杂的智能合约。 Bigi 等[11]将博弈论用在智能合约形式化验证中，使用概率模型检测对智能合约进行验证，但是只能针对有不确定性人类行为的智能合约。 Luu 等[12]使用Oyente 工具可检测部分重要类型的漏洞，但不能涵盖所有已知类型的漏洞，检测出来的结果需要人工进行二次审计和确认。

智能合约作为部署在区块链系统的合同，其公平性是一个至关重要的属性，只有保证参与合约的各方都能得到自己应有的利益，才能使智能合约可信，从而使得智能合约可以被广泛应用。智能合约的公平性问题大多是由于合约内部的逻辑造成的，而每一个合约的内部逻辑都不相同，这使得此类问题的检测特别具有挑战性。

本文将智能合约间互相调用的过程抽象为主体间互相发送消息的协议，用进程表示主体，利用进程间通信模拟智能合约的互相调用过程。通过进程的并发执行来实现区块链环境中智能合约的并发调用过程，然后使用模型检测[13]方法对进程执行过程中的状态进行检测。从而发现智能合约调用过程中存在违反公平性约束的状态，进而根据模型检测器产生的反例来推出智能合约中存在的漏洞。

1 智能合约公平性验证方法

1.1 方法概述

智能合约是根据文本合同编写的可以部署的区块链上的可执行代码。智能合约从生成到被调用一共包括以下几个阶段。

合约双方或多方达成共识->文本合同->智能合约代码->智能合约字节码->调用执行结果。

需要解决的是，由于智能合约代码和文本合同之间的不一致导致其执行结果与合同参与方预期不一致，从而使其中的某一方或多方利益受损的问题。对智能合约进行形式化验证时，需要满足3 个条件。

1）根据智能合约代码所建立的形式化模型必须准确的描述合约代码的内在逻辑。

2）在刻画合约公平性时，需要根据合约文本来抽象出满足合约公平性的条件，不能直接从智能合约代码中对公平性进行抽象，因为可能存在智能合约代码本身的逻辑是与文本合约不一致的情况。

3）在对形式化模型进行验证时，需要考虑真实合约执行过程中所有可能出现的情况，例如变量值可能极大，极小，或者出现负值，合约的调用可能会并发执行等等。

针对上述问题，提出基于模型检测的智能合约公平性验证方法，将智能合约间的互相调用抽象成为主体互相传递消息的协议，将合约内在逻辑抽象成为一个状态迁移函数，同时对智能合约应该满足的公平性用线性时态逻辑[14]（linear temporal logic，LTL）公式进行形式化描述，通过对协议执行过程中各个主体的状态进行检测，发现违反智能合约公平性约束的状态以及对应的漏洞。具体验证过程如图1 所示。

图1 验证过程Fig.1 Verification process

1.2 静态分析

在对智能合约进行建模之前，首先对智能合约代码进行静态分析，以排除直观的错误。可以对照如表1 所示的目前已知的智能合约中常见的漏洞，如时间戳依赖、错误的异常处理、整数溢出等。这些都可以通过对代码静态分析发现。

表1 智能合约常见漏洞Tab.1 Common vulnerabilities of smart contract

1.3 Solidity 语义分析

为确保所建模型准确的描述智能合约代码的内在逻辑，需要对Solidity 编程语言的语义进行分析[15]。由于通过静态分析已经剔除了那些如整数溢出、错误的异常处理等漏洞，所以建模时主要对合约的控制语句进行抽象，对Solidity 语言的控制语句进行形式化定义，定义如下

对于if 语句，B 表示语句的判断条件，σB，σM则分别表示存储在区块链上的全局变量和存储在智能合约内部的局部变量，如果判断条件为真则执行操作O，↓表示判断条件为假时，不做任何操作。对于while 语句，若判断条件为真，则执行循环体内部的操作语句然后再进行判断，若条件为假，则不做任何操作。在使用Promela 进行建模时，需要将Solidity 中的控制语句转换为Promela 语句。定义转换规则如下

在对变量进行转换时，为Solidity 中的每个全局变量定义一个对应的Promela 变量，对于Solidity中的局部变量，则定义对应的主体名前缀的全局变量来标识。

1.4 合约调用过程抽象

由于公平性都是相对而言，所以在对智能合约调用过程进行抽象时，需要描述参与合约执行的全部主体。用主体间发送消息来模拟智能合约间互相发送交易的调用过程，消息内容包含交易信息以及交易所携带的金额。抽象后的主体间交互过程如图2 所示。

图2 主体间交互抽象Fig.2 Interaction abstract between agents

以太坊中的智能合约可以看作是一个随着执行交易状态不断变换的有限状态机。所以在对智能合约的公平性进行验证时，把参与合约执行的主体看作一个整体。即智能合约的执行过程中是这个整体从一个状态到下一个状态的迁移过程。本文借鉴Bai[16]中对智能合约的形式化定义并对其简化，将智能合约执行过程定义如式（7）所示的4 元组

式中：S 为整体的当前状态，包括参与合约执行的全部主体状态，S＝（SA，SB，…）；T 为智能合约发送和接收的所有消息集合，T＝（T1，T2，…）；A 为智能合约主体所做的动作集合，包括Send（Ti）和Receive（Ti），A＝（a1，a2， …）；F 为参与合约执行的主体内部函数的集合，F＝（FA，FB，…）。将主体的内部逻辑抽象为一个函数，函数的输入为当前状态和所做的动作，输出为下一个状态，即SAi+1=FA（SAi，ai）。

虽然区块链上的所有计算都是确定性的，但是由于交易本身之间的竞争（即由矿工为给定的区块选择哪些交易），仍然会发生一定数量的不确定性。这里使用Promela 语言中进程的并发执行来达到这个目的，使动作的执行顺序在一定的规则下存在随机性，以模拟智能合约真实的执行环境。

1.5 交互过程Promela 建模

Promela 是一种描述并发系统的建模语言，用于有限状态机系统建模，是模型检测器SPIN 的输入语言，使用Promela 进程间通信的方式对智能合约间互相调用的交互过程进行建模。在Promela 中，主体间传递消息并不是直接发送消息给对方，而是发送方将消息发送到消息通道内，接收方从消息通道内取出消息。建立消息通道格式如式（8）所示

式中：ca 为通道名称；[0] 为通道内可以存放的消息数量。如果是同步消息传递，则通道内可以存放的消息数量为0，异步传递则可以设置通道内存放的消息数量。{ }为消息内容，包括消息数据类型的定义以及数据项的数目。通道内发送消息和接收消息如下

式（9）表示向通道ca 内发送一条消息，消息的内容包括x1，x2 两条数据。式（10）表示从通道cb 内接收两条消息，并将其分别赋值给变量x1，x2。Promela 消息通道中还有一种用于判断的操作，如式（11）所示

式（11）表示从通道cb 内接收一条消息，如果第一项数据等于x1，则把第二项数据赋值给变量x2，否则丢弃这条消息。

1.6 智能合约公平性刻画

对于智能合约公平性的定义，不同的合约会有不同的描述。例如，一个简单的买卖合约，如果买方先付款，卖方后发货，就需要有对卖方不发货这种情况的惩罚性条款，否则对于买方是不公平的。在一个拍卖合约中，如果存在几个投标人私下串通然后再出价的情况，则会对其他投标人不公平。总的来说，智能合约的公平性是指在合约执行过程中，可能出现的所有情况内，每一位合约参与者都能获得自己应有的利益。

在对具体合约安全性进行描述时，需要结合文本合约以及所建的形式化模型来抽象出与公平性相关的变量。使用各个变量间的关系来表示公平性。在对公平性进行描述时，要首先对智能合约执行流程进行分析，规定在一些特定的状态时，与公平性有关的单个或多个变量应该满足怎样的关系。然后使用LTL 公式描述满足公平时变量之间的关系。

例如对于一个简单的转账操作中的变量之间的关系，公平性可以描述为转账前后，转出方和接收方两人的余额之和是恒定的。使用LTL 描述如式（12）所示

[]（balance［sender］+balance［receiver］）（12）

2 Puzzle 合约公平性验证

Puzzle 是一个在区块链上很常见的奖励合约。合约的主要功能是对向智能合约提交问题正确答案的用户发放奖励。这个合约的逻辑是首先智能合约向区块链网络中广播寻求问题解决答案的交易信息，交易内包含问题描述以及赏金的金额。然后用户节点向智能合约发送提交答案的交易。智能合约在收到答案后，会对答案的正确性进行验证，若正确则向用户发放奖励，否则终止交易。同时智能合约的拥有者可以向智能合约发送修改奖励金额的交易，智能合约收到交易后会验证交易的发送方地址，如果是合约拥有者，则会将之前存放在智能合约的奖励金额返还给合约拥有者，并将拥有者发来的交易中携带的金额设置为新的奖励金额。经过静态分析修改后的Puzzle 合约的核心代码如下：

2.1 Puzzle 合约抽象

参与Puzzle 合约交互的主体有3 个，分别是智能合约（contract）、合约拥有者（owner）和提交答案的用户（user）。在区块链网络中交易信息是公开的，所以可以简化加解密以及身份地址认证等操作，直接使用点对点通信的方式来表示交易信息的发送和接收，这样能够简化模型，避免模型检测过程中状态空间爆炸的问题。 Puzzle 合约主体间交互过程如图3 所示。

图3 主体间交互过程图Fig.3 Interaction process diagram between agents

智能合约执行过程中的状态定义如式（13）所示

关于状态定义中每个变量的意义如表2 所示。关于消息、函数及动作集合的定义将在下一节中使用Promela 进程来说明。

表2 变量名称及意义Tab.2 Name and meaning of each variable

2.2 Puzzle 合约Promela 建模

在对Puzzle 合约交互过程抽象以后，可以发现有两对主体互相发送交易，分别是合约和用户以及合约和合约拥有者，通过定义两条一对一通信的消息通道来对进程间通信建模。为了便于解释下边的消息通道定义，需要先说明有限名称集的定义，如式（14）所示。

mtype question，answer，update；pay，payback；contract_reward；user_data；owner_balance; （14）

前5 个名称对应主体间发送消息的类型，分别是发送问题，提交答案，修改奖励金额，支付赏金以及退回奖励金额，后3 个则对应消息中的变量。消息通道定义如式（15）所示。

chan ca1=［0］ of ｛mtype，mtype｝；chan ca2=［0］ of｛mtype，mtype｝（15）

通道ca1 用于提交答案的用户和智能合约进行交互，通道ca2 用于合约拥有者和智能合约进行交互。因为定义的通道是一对一的，所以在消息内部不需要再表明消息的发送者和接收者。

2.2.1 user 建模

使用进程proctype user（）来定义向智能合约提交答案的用户进程，在proctype user（）中主要对user_balance，user_reward，user_data0，user_data1 这4 个变量进行操作。 user 进程主要做出的动作如式（16）所示。

user 进程的内部逻辑则通过Promela 语言中的控制语句以及消息通道内的判断操作来实现。这里将user 进程内部的逻辑抽象为一个状态转移函数，函数的输入是user 的当前状态以及所做的动作，输出为下一个状态。例如user 的初始状态Suser0如式（17）所示。

Suser0（user_balance，user_reward，user_data0，user_data1）＝（0，0，1，2）（17）

则经过执行动作a1 后得状态Suser0为：Suser1＝Fuser（Suser0，a1）=（0，5，1，2），鉴于篇幅原因，这里不再列出user 进程的Promela 代码。

2.2.2 contract 建模

使用进程proctype contract（）来定义智能合约进程，智能合约主体完成3 个操作。

1）向区块链网络广播消息，来请求问题答案。

2）接收来自答案提交用户的交易信息，对答案验证后，按照最新的奖励金额向用户发放奖励。为了简化模型，省略了对答案验证的过程。

3）接收来自合约拥有者的修改奖励金额的交易信息，将之前的奖励金返回给合约拥有者，然后将合约拥有者发来的交易中携带的金额设置为新的奖励金额。

使用两条发送语句模拟向网络中广播交易。智能合约主体的动作定义如式（18）所示。

智能合约主体内部函数的定义则使用Promela进程中关于通道内接收消息的判断操作以及控制语句来实现。智能合约主体内部逻辑核心代码如下所示。

2.2.3 owner 建模

使用进程proctype owner（）来定义向智能合约提交答案的用户进程，在proctype owner（）中主要对owner_balance，owner_reward 这2 个变量进行操作。owner 进程主要做出的动作如式（19）所示。

在这里假设合约拥有者在收到请求信息后，直接向合约发送修改价格的交易信息。 owner 进程内部逻辑为，在收到请求信息后，将其中携带的奖励金额的数量减少1，作为新的奖励金额发送给合约。

2.3 Puzzle 合约公平性刻画

在对智能合约的公平性进行刻画时，需要考虑智能合约是否完美的实现了它的功能且没有出现任何不允许出现的状态。在Puzzle 合约中，要达到的目的就是提交答案的用户和合约拥有者能够公平的完成交易。因为省略了答案验证以及地址验证等操作，所以要公平的完成交易，就需要满足以下3 点。

属性1 提交答案的用户在提交正确答案后，最终能够收到他接收问题时所观察到的奖励金额。即总是存在以下3 种状态中的一种：

1）用户还没有发送答案。

2）用户发送了答案但是还没有收到钱。

3）用户收到了他应该收到的奖励。

使用LTL 公式描述如式（20）所示。

属性2 合约拥有者在发送了新的奖励金额给智能合约后，安全的收到智能合约返还的奖励金额，且与他所观察到的修改前的奖励金额相等。使用LTL公式描述如式（21）所示。

属性3 合约在向用户发送完奖励以后，合约内一定存有正确的答案。这里使用user_balance!=0 来表示合约向用户付款成功。即contract_data 一定在user_balance!=0 变为真之前为真。使用LTL 公式描述如式（22）所示。

2.4 验证结果分析

将上述模型在SPIN6.4.9，Ispin 1.1.4 中运行，验证结果表明在搜索深度为33 时，公平性约束被违反，查看深度33 时各个变量的值如表3 所示。

表3 搜索深度为33 时各个变量值Tab.3 The value of each variable at depth 33

在深度33 时owner_balance 与owner_reward相等,即拥有者的公平得到了保证，但是当user_data0=0，即用户提交了答案以后，用户最后得到的奖励与他接收问题时所观察到的不同，user_balance 不等于user_reward，即用户的公平性没有得到保证。查看违反公平性时的消息序列如图4 所示。当公平性被违反时，主体间交互过程如图5 所示。

图4 公平性违反时消息序列Fig.4 Message sequence graph for fairness violation

图5 主体间交互过程Fig.5 Interaction process between agents

为了更加细致的分析造成公平性被违反的原因，需要根据主体间的交互过程来刻画智能合约的状态迁移序列。 Puzzle 合约状态迁移如图6 所示（*标记值发生变化的变量），这里仅列出与公平性有关的变量。

图6 Puzzle 合约公平性违反时状态迁移图Fig.6 State transition graph for fairness violation of Puzzle contract

由此可知Puzzle 合约不满足公平性是因为用户和合约拥有者两个主体同时发送交易调用了智能合约，由于同一区块内交易执行顺序的随机性，导致用户接收的奖励是被合约拥有者修改以后的奖励金额。即用户没有收到他接收问题时所看到的奖励金额。结合文献[12]中对交易顺序依赖漏洞的分析，Puzzle 合约中存在交易顺序依赖漏洞，对提交答案的用户是不公平的。通过上述实验证明，发现Puzzle 合约中存在公平性漏洞，证明了本文中提出方法的可行性。