智慧合约-智能合约安全问题的AI解决方案
作者：MATRIX CTO 李庆华
“一支穿云箭，千军万马来相见”。
在经历三个月“漫长熊市”后，从4月中旬开始，EOS的一个拉升，形成了数字货币市场大牛市的壮观景象。可是在美链BeautyChain（BEC）的智能合约漏洞被黑客利用、随意刷币，SmartMesh（SMT）智能合约再次爆出相同漏洞，并在OKex上出现大规模异常交易后，整个市场随即进入大幅震荡的情形。在了解事情经过后，我们不禁要问，为何小小的漏洞会引发如此大的动静？
智能合约的技术缺陷和解决方案
智能合约的2个缺陷
其实这件事情集中暴露了以以太坊为代表的区块链2.0技术的两个缺点：
（1）智能合约不够智能；
（2）智能合约缺少安全保障机制和安全工具。
区块链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 以太坊智能合约函数调用情况统计
可以看到，加减乘除采用安全函数的合约只占少数，实现转账功能的基本每个合约都有。从大概率上讲，黑客的好日子还在后头，数字货币市场出现安全动荡的情况，一定比大姨妈还要准时。目前的以太坊只是一个记录 DApp 执行结果的区块链，本身并没有提供加密货币复式记账所需的UXTO模型。以太坊自身的以太币也是通过balance 来表示账号余额，这实质就是最原始的古代单式记账方法。而看过类似《天下粮仓》电视剧的，都知道这种基于财务做账的难于发觉之处。
那么我们要怎样才能改变这一现状呢？鲁迅先生讲过：“真的猛士敢于直面惨淡的人生”，作为区块链的从业者，我们坚定的认为智能合约是一个跨越时代的思想，但现有的实现方式的确需要改变。
智能合约面临的3个挑战
现有的智能合约需要解决三个问题：
（1）安全性问题；
（2）可靠行问题；
（3）易用性问题。
可靠性问题与易用性问题，我们可以依托人工智能以及其他相关技术解决，本文重点谈谈安全性怎么解决。
智能合约的解决方案——智慧合约
要想真正解决智能合约的安全性问题，就必须设计一套完整的综合防护体系，并能不断完善，具体包括：
（1）事前防护：代码编写过程中的规范化与代码发布的漏洞检测；
（2）事中验证：在智能合约虚拟机中完成代码的执行与动态安全检测；
（3）事后弥补：对智能合约执行结果进行审计，确保执行不会出现偏差，执行结果在可信范畴。利益关联方能够及时发起申述，并进行裁决。
我们将这种支持具备完整安全防护体系的智能合约称为智慧合约。
如果BEC与SMT采用智慧合约的方式部署，将得到多重防护，从而获得多次“上天再给我一次重来的机会”。典型的机会包括：
（1）代码定型与发布时的验证与检查。无论设计者是否愿意，每个发布的代码将接受自动规则验证检查，从而确保静态代码审查通过，那些典型的溢出漏洞规则将无处藏身；
（2）节点在执行合约中的动态验证。该动态验证将涵盖本合约、关联合约的验证，并对执行过程中的状态进行审查，从而实现各种执行漏洞进行弥补，即使黑客造出漏洞，各个合约执行者也会严密审视，并挂起可以执行操作；
（3）合约执行完毕的合理性判断。合约执行完毕的结果将通过一定的规则进行评判，同时引入人工智能，对合约执行的合理区间进行分析，从而决定最终的结果输出；例如对账目进行复式审查或更高维度进行审查；
（4）相关利益方的申诉机制与自动判决技术。在智慧合约部署的节点上，每个节点都内置基于规则的判决机制以及人工智能审核机制，支持自动投票表决，从而保证一定的机会挽回损失。
实际上，智慧合约必须由以下几类技术，才能完成基础框架：
基于规则知识库的语法检查
基于语义分析的交易模型识别与安全检查
基于AI的形式验证的智能合约安全性检查
基于深度神经网络的动态验证和安全性优化
MATRIX智慧合约的先进技术实现
MATRIX是区块链+人工智能技术的倡导者和领导者，团队拥有AI科学家邓仰东教授、芯片科学家时昕博士和CTO李庆华等大量专业人才，在人工智能与区块链基础链研究上，做出了大量的基础性研究工作，并取得了大量突破性进展和技术专利；在MATRIX的共识算法上创新性地使用了“虫洞网络”来保证MATRIX在未来可以支撑百万级TPS的商业级应用的同时还能保障系统的安全性。
智慧合约则是MATRIX另外一个重要特性。下面将简单从技术实现的角度介绍MATRIX在智慧合约上的研究进展，并给出当前智能合约各种缺陷的对策。
基于规则知识库的语法检查
核心原理是将原始编码文件，通过内置编译工具，将对合约构建一棵基于BNF范式基础上的抽象语法树（AST），通过该语法抽象树，便可以对合约内容展开语法识别，进行简单的合约安全识别。目前建议按照递归下降分析的方法，对语法抽象树进行基于知识规则库的检查，从而确定是否存在安全隐患。
虽然一般的智能合约描述均为图灵完备，在抽象语法树可以表现为多样性，但很容易发现：安全的智能合约实际应该是一个典型的闭合自洽描述，具备有限状态空间或确保能够检测终止的有限状态机。因此可以通过检测的语法抽象树的平衡和闭合性，确定智能合约是否具备基本安全性。
典型的例子包括：
（1）对所有的条件选择语句进行完备性补足，防止由于条件不完善导致合约执行缺陷的；
（2）对所有public成员与函数进行引用对象分析，确定合约对外暴露的危险等级。
（3）交易步骤完备性检查，确定每个合约交易方的条件动作描述完备。
基于语义分析的交易模型识别与安全检查
基于语法的安全检查规则仅能静态识别合约缺陷，而基于语义分析的交易模型识别与安全检查，则主要通过上下文相关审查，确定智能合约中不满足规则或者不安全的操作。目前支持的安全检查包括：
（1） 类型检查，具体包括检查合约中需要对外暴露的对象与方法，审查其动作的必要性以及潜在的缺陷。
（2） 控制流检查，具体包括检查合约中各种选择分支或者针对ORACLE的处理是否完备，并确定合约被调用时，是否存在其他异常处理等。
（3） 一致性检查，具体包括同一个合约条件，出现在不同的选择组合中；各种分支出现组合覆盖等，避免由于分布式执行出现由于矿工调用顺序不同，导致的合约异常。
通过上述静态语义分析，能够基本排除由于人为书写智能合约带来的各种表层的逻辑缺陷，但尚不能解决动态执行过程中出现的各种逻辑问题。这些问题包括：
（1） 书写代码不精确、不完备导致的合约组合条件情况处理的缺失；
（2） 个人合约设计目的与真实编写代码之间存在较多的差异；
（3） 由于合约执行采用分布式执行，各个节点对代码的执行顺序存在差异，导致当本合约出现异常时，其他合约能够调用或更改本合约的各种状态，出现各种非安全性问题。
MATRIX的核心是人工智能辅助计算，各个层级上均内置AI能力，因此在合约验证上，采用基于AI辅助的形式验证以及动态约束检查的方法，解决上述安全问题。其核心思想包括：
（1） 利用模式匹配获得用户真实需求约束：基于语义分析形成的合规语法抽象树进行基础模式匹配，获得用户可能的交易基础模型。该方法能够以静态手段获得大部分语法抽象分支的局部匹配。MATRIX根据具体的匹配度，确认候选模型或模型组合，从而根据模型添加交易约束与交易断言。
（2） 对静态语义分析形成的抽象树，按照MATRIX的AI引擎——贝叶斯分类器进行模型分类，确定树中的各段分支属于对应的类属。而在MATRIX中，针对每个交易类属，均具备对应的静态与动态约束。
（3） 根据模式匹配结果和人工智能分类结果，获得当前合约的全部静态与动态约束，基于该约束即可生成合约代码的断言，并基于该结果进行形式验证和动态验证。
对于模型匹配失败或者分类失败的合约，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.以太坊智能合约的脆弱性
为解决上述问题，MATRIX准备开发两类安全工具，以解决上述问题，具体包括：
（1） 基于对抗网络的安全验证；
（2） 基于分布式并发的动态模型验证。
基于GAN的安全验证
怎样设计在充满不确定性的分布式环境下仍然能够正确、安全运行的智能合约代码呢？Matrix平台只需要使用者以脚本语言 方式说明合约意图（输入、输出和交易条件等），然后使用基于神经网络的代码生成技术把脚本转换为智能合约代码，如图5所示。继而采用类似对抗网络的方法，即一方面使用代码生成网络产生黑客代码极其攻击条件，一方面对现有代码进行变型和优化，同时在模拟区块链网络上对上述代码进行对抗和性能评估，直至产生足够安全的智能合约代码。
我们将逐渐过渡到直接使用自然语言描述合约
图5. 智能合约代码生成
图5的智能合约代码生成流程使用基于递归神经网络的代码生成工具把脚本转换为智能合约代码，其中的递归神经网络需要使用现有智能合约程序及其输入和输出结果作为训练样本。
基于分布式并发的动态模型验证智能合约的攻击手段和防护手段在前面已经详细论述，MATRIX还提供了基于分布式并发的动态模型验证，对如下的手段进行防护：
（1）交易合约顺序攻击
出现合约顺序攻击的本质是智能合约的执行是异步的，且可以动态更改。即使合约本身是静态安全情况下，也无法防止此类动态攻击，除非合约本身设计为动态不可更改。对于MATRIX智能合约，则通过AI的动态保护，包括对矿工执行合约集的进行整体关联性审查，通过环路发现，找出基于此类的关联合约交易。另外，MATRIX提供基于多节点执行的异步模拟器，通过对设立多个节点（当前为5个节点）采用乱序并发方式，异步执行合约，通过对每个执行序列的观察，确定是否出现异常来排除交易合约顺序攻击。
（2）基于时间戳依赖的攻击
时间戳依赖的本质是矿工自主权过大，因此MATRIX通过AI动态审查时间戳依赖或者随机数依赖，可以避免在合约中出现相应的依赖行为。MATRIX还额外设计了二阶段随机数机制和对应的智能选举方案解决。
（3）误操作异常和可重入攻击
上述攻击实际上是合约调用过程中，触发异常状态。MATRIX将通过深度学习，找出此类行为特征的编码方式，获得类似黑客作案手法的码本特征库，并进行代码库静态与动态审查。其中动态审查则是基于形式验证中的约束，动态生产特征向量，并针对性的测试发现缺陷。
结束语
而且随着市场竞争的激烈，各种需求急剧变化，每种新技术的生命周期很短。站在区块链行业发展的角度看，数字合约是一个“激流世界”，下一刻没有人知道会发生什么。但我们知道，对付“激流世界”的核心手段就是在变化的世
界中找出不变的东西，从而从容面对时刻发生的挑战，而基于人工智能和经过传统金融考验的安全风控方法——智慧合约，正是核心解决之道。
李庆华介绍：
国内顶级芯片设计专家，拥有多项芯片专利，他作为主设计师，设计了国内第一款WiFi芯片。同时作为总工团队成员和基带项目总工程师，设计了中国首个大型水面舰艇的通信调度指挥系统。个人主导设计了多款量产商用芯片，并多次获得省部级科学技术奖励。著有《通信IC设计》一书，京东同类书籍销售排行榜第一名，被北邮等一流高校采取为研究生芯片设计课程的教材。
