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

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

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

1

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

智能合约的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所示。

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

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

智能合约面临的3个挑战

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

• 安全性问题；

• 可靠性问题；

• 易用性问题。

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

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

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

• 事前防御：代码编写过程当中的规范化与代码发布的漏洞检测；

• 事中验证：在智能合约虚拟机中完成代码的执行与动态安全检测；

• 过后弥补：对智能合约执行结果进行审计，确保执行不会出现误差，执行结果在可信范畴。利益关联方可以及时发起申述，并进行裁决。

咱们将这种支持具有完整安全防御体系的智能合约称为智慧合约。

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

• **代码定型与发布时的验证与检查。**不管设计者是否愿意，每一个发布的代码将接受自动规则验证检查，从而确保静态代码审查经过，那些典型的溢出漏洞规则将无处藏身；

• **节点在执行合约中的动态验证。**该动态验证将涵盖本合约、关联合约的验证，并对执行过程当中的状态进行审查，从而实现各类执行漏洞进行弥补，即便黑客造出漏洞，各个合约执行者也会严密审视，并挂起能够执行操做；

• **合约执行完毕的合理性判断。**合约执行完毕的结果将经过必定的规则进行评判，同时引入人工智能，对合约执行的合理区间进行分析，从而决定最终的结果输出；例如对帐目进行复式审查或更高维度进行审查；

• 相关利益方的申诉机制与自动判决技术。在智慧合约部署的节点上，每一个节点都内置基于规则的判决机制以及人工智能审核机制，支持自动投票表决，从而保证必定的机会挽回损失。

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

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

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

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

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

2

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

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

• 基于对抗网络的安全验证；

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

基于GAN的安全验证

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

 图4. 智能合约代码生成

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

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

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

交易合约顺序攻击

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

基于时间戳依赖的攻击

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

误操做异常和可重入攻击

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

3

结束语

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

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

本文做者：MATRIX CTO 李庆华

如下是咱们的社区介绍，欢迎各类合做、交流、学习：）