智慧合约——智能合约安全问题的AI解决方案

“一支穿云箭，千军万马来相见”。

在经历三个月“漫长熊市”后，从 4 月中旬开始，EOS 的一个拉升，形成了数字货币市场大牛市的壮观景象。可是在美链 BeautyChain（BEC）的智能合约漏洞被黑客利用、随意刷币，SmartMesh（SMT）智能合约再次爆出相同漏洞，并在 OKex 上出现大规模异常交易后，整个市场随即进入大幅震荡的情形。在了解事情经过后，我们不禁要问，为何小小的漏洞会引发如此大的动静？

智能合约的技术缺陷和解决方案

智能合约的 2 个缺陷

其实这件事情集中暴露了以以太坊为代表的区块链 2.0 技术的两个缺点：

• 智能合约不够智能；
• 智能合约缺少安全保障机制和安全工具。

区块链 2.0 的核心是智能合约，而当黑客能够轻而易举地利用智能合约漏洞为所欲为时，实质上相当于动摇了整个大厦的根基，因此造成数字货币市场的恐慌也在所难免。

加法溢出漏洞：一个加法带来的血案！

我们可以将 SMT 漏洞归纳为一句话：利用加法的溢出漏洞，规避安全检查从而获得巨额收益。首先看看这段代码，要害就在图 1 中的 206 行：

图1 SMT 漏洞代码

Etherscan**** 链接如下：

https://etherscan.io/tx/0x1abab4c8db9a30e703114528e31dee129a3a758f7f8abc3b6494aad3d304e43f

而黑客的攻击手法和成果如下：

Function: transferProxy(address _from, address _to, uint256 _value, uint256 _feeSmt, uint8 _v, bytes32 _r, bytes32 _s)

MethodID: 0xeb502d45

[0]: 000000000000000000000000df31a499a5a8358b74564f1e2214b31bb34eb46f（_from，转账转入地址）

[1]: 000000000000000000000000df31a499a5a8358b74564f1e2214b31bb34eb46f（_to，转账转出地址）

[2]: 8fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff（_value）

[3]: 7000000000000000000000000000000000000000000000000000000000000001（_value）

[4]: 000000000000000000000000000000000000000000000000000000000000001b（_v）

[5]: 87790587c256045860b8fe624e5807a658424fad18c2348460e40ecf10fc8799（_r）

[6]: 6c879b1e8a0a62f23b47aa57a3369d416dd783966bd1dda0394c04163a98d8d8（_s）

黑客获得财富为：

可以发现黑客的balances[_To] 凭空获得了巨额的财富，该数字在这一刻，超越了全球现有货币发行总量。美美的财富啊！但是带来的后果就是smartmesh 货币总量瞬间崩溃了。这笔财富瞬间超越了全部SMT 限定总额。

SMT 事件，可以简单概括为一句话：“一个加法带来的血案！”

乘法溢出漏洞：一个乘法引发的血案！

同样，BEC 的过程依然如此，图 2 代码的 257 行，存在一个巨型整数乘法溢出问题：

图2 BEC 漏洞代码

合约代码地址： https://etherscan.io/address/0xc5d105e63711398af9bbff092d4b6769c82f793d#code

黑客构造的攻击如下，转账记录如下：

https://etherscan.io/tx/0xad89ff16fd1ebe3a0a7cf4ed282302c06626c1af33221ebe0d3a470aba4a660f

瞬间，整个全世界都属于这个黑客的了。又是“一个乘法引发的血案！”。

由此看来，智能合约的安全性将会极大动摇整个区块链 2.0 的根基。

目前的智能合约，从用户角度来讲，实际上是一个无人值守、程序机械执行、具备自动担保的应用程序，只是当特定的条件满足时，能够自动释放和转移资金。智能合约从技术层面来讲就是一种网络服务，是通过区块链共识，完成特定的合约程序执行。由于是共识，区块链上的任意智能合约代码和状态必然都要公开，都要经受历史的考验；而任何一个黑客都可以从容淡定地审视每一行可能被屠杀的代码，就像丛林社会中那些凶猛的狮子总是在草原深处游荡，但偶尔会看看这些可怜的羚羊（合约）。即使合约被黑客吃干抹净，这些可怜的数据还耻辱地挂在那里，诸位看客们或怜悯、或嘲笑、或深深的叹息，或许还有一两个此间的少年来一句：“大丈夫当如是也！”。

我们知道，开源代码大致每 1000 行就含有一个安全漏洞，表现最好的 Linux kernel 2.6 版本的安全 bug 率为每一千行代码 0.127 个。而智能合约作为新生事物，对应的程序员没有经过严苛训练与考验，其代码可靠性可想而知。我们对 2018 年 1 月到 4 月，以太坊全部部署的全部 8000 多个合约，其内部函数调用情况统计结果如表 1 所示。

表 1 以太坊智能合约函数调用情况统计

函数

频次排序

Functions

调用总次数

函数频次排序

Functions

调用总次数

1

transfer

12230

16

increaseapproval

1510

2

transferfrom

11034

17

decreaseapproval

1509

3

approve

10494

18

receiveapproval

1505

4

balanceof

9830

19

mint

1292

5

allowance

8834

20

_transfer

1255

6

oraclize_query

4708

21

owned

1135

7

totalsupply

4621

22

safeadd

942

8

transferownership

3356

23

safesub

905

9

add

2915

24

safemul

862

10

sub

2887

25

safediv

805

11

mul

2866

26

burnfrom

781

12

div

2777

27

acceptownership

773

13

approveandcall

2636

28

transferanyerc20token

654

14

ownable

2174

29

finishminting

651

15

burn

1685

30

withdraw

628

可以看到，加减乘除采用安全函数的合约只占少数，实现转账功能的基本每个合约都有。从大概率上讲，黑客的好日子还在后头，数字货币市场出现安全动荡的情况，一定比大姨妈还要准时。目前的以太坊只是一个记录 DApp 执行结果的区块链，本身并没有提供加密货币复式记账所需的 UXTO 模型。以太坊自身的以太币也是通过 balance 来表示账号余额，这实质就是最原始的古代单式记账方法。而看过类似《天下粮仓》电视剧的，都知道这种基于财务做账的难于发觉之处。

那么我们要怎样才能改变这一现状呢？鲁迅先生讲过：“真的猛士敢于直面惨淡的人生”，作为区块链的从业者，我们坚定的认为智能合约是一个跨越时代的思想，但现有的实现方式的确需要改变。

智能合约面临的 3 个挑战

现有的智能合约需要解决三个问题：

• 安全性问题；
• 可靠行问题；
• 易用性问题。

可靠性问题与易用性问题，我们可以依托人工智能以及其他相关技术解决，本文重点谈谈安全性怎么解决。

智能合约的解决方案——智慧合约

要想真正解决智能合约的安全性问题，就必须设计一套完整的综合防护体系，并能不断完善，具体包括：

• 事前防护：代码编写过程中的规范化与代码发布的漏洞检测；
• 事中验证：在智能合约虚拟机中完成代码的执行与动态安全检测；
• 事后弥补：对智能合约执行结果进行审计，确保执行不会出现偏差，执行结果在可信范畴。利益关联方能够及时发起申述，并进行裁决。

我们将这种支持具备完整安全防护体系的智能合约称为智慧合约。

如果 BEC 与 SMT 采用智慧合约的方式部署，将得到多重防护，从而获得多次“上天再给我一次重来的机会”。典型的机会包括：

• 代码定型与发布时的验证与检查。无论设计者是否愿意，每个发布的代码将接受自动规则验证检查，从而确保静态代码审查通过，那些典型的溢出漏洞规则将无处藏身；
• 节点在执行合约中的动态验证。该动态验证将涵盖本合约、关联合约的验证，并对执行过程中的状态进行审查，从而实现各种执行漏洞进行弥补，即使黑客造出漏洞，各个合约执行者也会严密审视，并挂起可以执行操作；
• 合约执行完毕的合理性判断。合约执行完毕的结果将通过一定的规则进行评判，同时引入人工智能，对合约执行的合理区间进行分析，从而决定最终的结果输出；例如对账目进行复式审查或更高维度进行审查；
• 相关利益方的申诉机制与自动判决技术。在智慧合约部署的节点上，每个节点都内置基于规则的判决机制以及人工智能审核机制，支持自动投票表决，从而保证一定的机会挽回损失。

实际上，智慧合约必须由以下几类技术，才能完成基础框架：

• 基于规则知识库的语法检查
• 基于语义分析的交易模型识别与安全检查
• 基于 AI 的形式验证的智能合约安全性检查
• 基于深度神经网络的动态验证和安全性优化

MATRIX 智慧合约的先进技术实现

MATRIX 是区块链 + 人工智能技术的倡导者和领导者，团队拥有 AI 科学家邓仰东教授、芯片科学家时昕博士和 CTO 李庆华等大量专业人才，在人工智能与区块链基础链研究上，做出了大量的基础性研究工作，并取得了大量突破性进展和技术专利；在 MATRIX 的共识算法上创新性地使用了“虫洞网络”来保证 MATRIX 在未来可以支撑百万级 TPS 的商业级应用的同时还能保障系统的安全性。

智慧合约则是 MATRIX 另外一个重要特性。下面将简单从技术实现的角度介绍 MATRIX 在智慧合约上的研究进展，并给出当前智能合约各种缺陷的对策。

基于规则知识库的语法检查

核心原理是将原始编码文件，通过内置编译工具，将对合约构建一棵基于 BNF 范式基础上的抽象语法树（AST），通过该语法抽象树，便可以对合约内容展开语法识别，进行简单的合约安全识别。目前建议按照递归下降分析的方法，对语法抽象树进行基于知识规则库的检查，从而确定是否存在安全隐患。

虽然一般的智能合约描述均为图灵完备，在抽象语法树可以表现为多样性，但很容易发现：安全的智能合约实际应该是一个典型的闭合自洽描述，具备有限状态空间或确保能够检测终止的有限状态机。因此可以通过检测的语法抽象树的平衡和闭合性，确定智能合约是否具备基本安全性。

典型的例子包括：

• 对所有的条件选择语句进行完备性补足，防止由于条件不完善导致合约执行缺陷的；
• 对所有 public 成员与函数进行引用对象分析，确定合约对外暴露的危险等级。
• 交易步骤完备性检查，确定每个合约交易方的条件动作描述完备。

基于语义分析的交易模型识别与安全检查

基于语法的安全检查规则仅能静态识别合约缺陷，而基于语义分析的交易模型识别与安全检查，则主要通过上下文相关审查，确定智能合约中不满足规则或者不安全的操作。目前支持的安全检查包括：

• 类型检查，具体包括检查合约中需要对外暴露的对象与方法，审查其动作的必要性以及潜在的缺陷。
• 控制流检查，具体包括检查合约中各种选择分支或者针对 ORACLE 的处理是否完备，并确定合约被调用时，是否存在其他异常处理等。
• 一致性检查，具体包括同一个合约条件，出现在不同的选择组合中；各种分支出现组合覆盖等，避免由于分布式执行出现由于矿工调用顺序不同，导致的合约异常。

通过上述静态语义分析，能够基本排除由于人为书写智能合约带来的各种表层的逻辑缺陷，但尚不能解决动态执行过程中出现的各种逻辑问题。这些问题包括：

• 书写代码不精确、不完备导致的合约组合条件情况处理的缺失；
• 个人合约设计目的与真实编写代码之间存在较多的差异；
• 由于合约执行采用分布式执行，各个节点对代码的执行顺序存在差异，导致当本合约出现异常时，其他合约能够调用或更改本合约的各种状态，出现各种非安全性问题。

MATRIX 的核心是人工智能辅助计算，各个层级上均内置 AI 能力，因此在合约验证上，采用基于 AI 辅助的形式验证以及动态约束检查的方法，解决上述安全问题。其核心思想包括：

• 利用模式匹配获得用户真实需求约束：基于语义分析形成的合规语法抽象树进行基础模式匹配，获得用户可能的交易基础模型。该方法能够以静态手段获得大部分语法抽象分支的局部匹配。MATRIX 根据具体的匹配度，确认候选模型或模型组合，从而根据模型添加交易约束与交易断言。
• 对静态语义分析形成的抽象树，按照 MATRIX 的 AI 引擎——贝叶斯分类器进行模型分类，确定树中的各段分支属于对应的类属。而在 MATRIX 中，针对每个交易类属，均具备对应的静态与动态约束。
• 根据模式匹配结果和人工智能分类结果，获得当前合约的全部静态与动态约束，基于该约束即可生成合约代码的断言，并基于该结果进行形式验证和动态验证。

对于模型匹配失败或者分类失败的合约，MATRIX 将提出不可靠安全告警，并在执行过程中进行更严苛的边界检查。

MATRIX 支持 Bytecode 级别的语义审查，核心还是进行反汇编，然后生产语法抽象树，然后进行利用 AI 进行语法树匹配。

基于 AI 的形式验证的智能合约安全性检查

MATRIX 使用形式验证技术对智能合约的安全性进行自动化检查。其中，形式验证模型使用 F* 函数程序语言（functional programming language）建立，该语言整合了 Z3 SMT 求解工具，拥有丰富的类型和条件检查功能，已经被用于多种软件和加密程序的验证。

图3 智能合约的形式验证

智能合约形式验证流程图如图3。形式验证工具链能够处理源代码级的智能合约，其中源代码被翻译为等效的F* 函数程序；也能够处理编译为字节码的智能合约，此时需要对字节码进行反编译，同样形成等效的F* 函数程序。Matrix 区块链平台的智能合约语法结构以及相应函数程序语法结构如图4。对于用户自行编写的智能合约，我们还可以对源代码模型和编译代码模型进行等效检查，从而发现编译器的错误或者不良副作用。

在建立基于函数编程语言的模型之后，形式验证的基本手段是针对模型定义需要满足的安全属性（即property，例如对send() 函数的返回值是否进行了检查），然后使用定理证明工具或可满足性工具寻找是否存在反例使得以上条件不成立。然而，即使对专业智能合约程序员来说准确定义完备的安全属性集合都是极端困难的事情，对一般用户来说则几乎是不可能的。

MATRIX 的一个关键特色是使用人工智能方法自动识别程序语义并发现其中的典型模式，从而根据模式自行产生为了满足安全要求而需要的属性。当用户提供智能合约代码或编译后的执行代码后，MATRIX 的 AI 引擎将自动完成代码的局部相似性匹配和全局相似性匹配，从而推测代码的行为模型。根据 AI 获得行为模型，生成对应的形式验证约束，从而进行深层次的行为验证，实现代码安全性。

由于使用函数程序编程语言作为内部验证的形式化表征，MATRIX 还可以对 Ethereum 现有开源合约进行模式挖掘。这些模式可以表现为语义或者结构（以及两者的组合）的形式，前者一般是特定语法和函数特征，后者则是语法结构特征。

基于深度神经网络的动态验证和安全性优化

表 2 列出以太坊智能合约在高级编程语言、字节码和区块链三个层次上的脆弱性、当前主要的攻击方式以及相应脆弱性在受到攻击时表现出的特征。

表 2. 以太坊智能合约的脆弱性

层次

脆弱性

针对脆弱性的攻击方式

收到攻击时的表现特征

Solidity

Call to the unknown

1. The DAO attack

调用堆栈快速增加、余额不断减少

Gasless send

2.“King of the Ether Throne”

Gas 快速消耗

Exception disorders

2.“King of the Ether Throne”

3. GovernMental

调用堆栈快速增加、Gas 快速消耗、数据堆栈快速增加

Type casts

N.A.

Reentrancy

1. The DAO attack

调用堆栈耗尽、gas 不断减少

Keeping secrets

4. Multi-player games

代码和字节码表现形式

EVM

Immutable bugs

3. GovernMental

5. Rubixi

代码和字节码表现形式

Ether lost in transfer

N.A.

接收地址为“孤儿”地址

Stack size limit

3. GovernMental

调用堆栈快速增加

区块链

Unpredictable state

3. GovernMental

6 .Dynamic libraries

数据堆栈快速增加、访问被删除或更新的库模块

Generating randomness

N.A.

代码执行过程中结果的随机分布

Time constraints

3. GovernMental

调用堆栈快速增加、合约余额不断增加、时间戳变化

为解决上述问题，MATRIX 准备开发两类安全工具，以解决上述问题，具体包括：

• 基于对抗网络的安全验证；
• 基于分布式并发的动态模型验证。

基于 GAN 的安全验证

怎样设计在充满不确定性的分布式环境下仍然能够正确、安全运行的智能合约代码呢？Matrix 平台只需要使用者以脚本语言 [1] 方式说明合约意图（输入、输出和交易条件等），然后使用基于神经网络的代码生成技术把脚本转换为智能合约代码，如图 5 所示。继而采用类似对抗网络的方法，即一方面使用代码生成网络产生黑客代码极其攻击条件，一方面对现有代码进行变型和优化，同时在模拟区块链网络上对上述代码进行对抗和性能评估，直至产生足够安全的智能合约代码。

图5. 智能合约代码生成

图5 的智能合约代码生成流程使用基于递归神经网络的代码生成工具把脚本转换为智能合约代码，其中的递归神经网络需要使用现有智能合约程序及其输入和输出结果作为训练样本。

基于分布式并发的动态模型验证

智能合约的攻击手段和防护手段在前面已经详细论述，MATRIX 还提供了基于分布式并发的动态模型验证，对如下的手段进行防护：

（1）交易合约顺序攻击

出现合约顺序攻击的本质是智能合约的执行是异步的，且可以动态更改。即使合约本身是静态安全情况下，也无法防止此类动态攻击，除非合约本身设计为动态不可更改。对于MATRIX 智能合约，则通过AI 的动态保护，包括对矿工执行合约集的进行整体关联性审查，通过环路发现，找出基于此类的关联合约交易。另外，MATRIX 提供基于多节点执行的异步模拟器，通过对设立多个节点（当前为5 个节点）采用乱序并发方式，异步执行合约，通过对每个执行序列的观察，确定是否出现异常来排除交易合约顺序攻击。

（2）基于时间戳依赖的攻击

时间戳依赖的本质是矿工自主权过大，因此MATRIX 通过AI 动态审查时间戳依赖或者随机数依赖，可以避免在合约中出现相应的依赖行为。MATRIX 还额外设计了二阶段随机数机制和对应的智能选举方案解决。

（3）误操作异常和可重入攻击

上述攻击实际上是合约调用过程中，触发异常状态。MATRIX 将通过深度学习，找出此类行为特征的编码方式，获得类似黑客作案手法的码本特征库，并进行代码库静态与动态审查。其中动态审查则是基于形式验证中的约束，动态生产特征向量，并针对性的测试发现缺陷。

结束语

而且随着市场竞争的激烈，各种需求急剧变化，每种新技术的生命周期很短。站在区块链行业发展的角度看，数字合约是一个“激流世界”，下一刻没有人知道会发生什么。但我们知道，对付“激流世界”的核心手段就是在变化的世界中找出不变的东西，从而从容面对时刻发生的挑战，而基于人工智能和经过传统金融考验的安全风控方法——智慧合约，正是核心解决之道。

李庆华介绍

国内顶级芯片设计专家，拥有多项芯片专利，他作为主设计师，设计了国内第一款WiFi 芯片。同时作为总工团队成员和基带项目总工程师，设计了中国首个大型水面舰艇的通信调度指挥系统。个人主导设计了多款量产商用芯片，并多次获得省部级科学技术奖励。著有《通信IC 设计》一书，京东同类书籍销售排行榜第一名，被北邮等一流高校采取为研究生芯片设计课程的教材。

[1] 我们将逐渐过渡到直接使用自然语言描述合约