区块链技术重大挑战（二）：智能合约安全的曙光

先上个调查，看看大家兴趣决定做不做：

这是一个昨天没写完的小follow up短文章。

昨天的文章里面，给大家重点介绍了区块链安全是多么的重要，附送了一个真实发生的杯具。相信大家已经认识到了智能合约安全性是一个非常严重的投资系统性风险。

那么这个风险有救么？

老董认为是有救的。

之前老董把智能合约程序比做了深空探测火箭，一发射就失去了控制。其实这个比喻适合于任何飞行器，比如民航飞机。

不知道大家每次在登上飞机的时候，潜意识中有没有一丝丝的惴惴不安？我小时候总会想，飞机要掉下来怎么办（敲桌子）。但其实查查历史数据就会发现，飞机出重大事故的概率是四百万分之一，被雷劈的概率大概是多少呢？三百万分之一。之前有Powerball超级彩票大奖，我和几个朋友几个人凑了300块钱来买，我们中奖的概率是多少呢？两百万分之一。

大家登机的时候应该都看过舰桥里面的控制板面：有几百个按键和控制杆，整个飞机有数万个机械构建。一个飞控程序系统要配合飞行员控制所有这些复杂的部件，同时面对复杂的空中状况。

我们不禁要问：飞机飞机你为何如此牛b？

我们知道，人肉写的复杂的程序是无法避免漏洞的。工业界的平均水平大概是每1000行代码中，有15-50个漏洞 (Seve McConell, Code Complete)。但是飞机自动驾驶的程序是真的是不能有漏洞，这怎么整？好好写测试？

这事儿搞不定，因为测试程序永远无法覆盖复杂程序的所有可能输入和所有执行路径。

所以搞航空航天软件的这帮人就开始用一个比写测试牛逼很多的方法：形式验证(formal verification)。

说的简单一点呢，所谓形式验证是由如下两个步骤组成：

第一步：定义Invariant （不变式）：其实就是称需要永恒满足的条件，简单的比如“我的程序里面永远不会由除法除数为0的情况出现”，复杂的可以是：“自动驾驶的高度变量的内存区域永远不会出现溢出而变成负值，飞机就栽了”

第二步：把你的程序代码变成一个形式验证模型。通过对这个形式验证模型的静态分析（不执行程序本身），检查对于所有可能的程序初始状态所形成的等价超空间，不变式的恒定性，并查找不满足不变式的等价超空间以及空间转换函数序列。

好让我来用人话重说一遍：用非常牛逼的算法，检查所有程序的输入值和所有的可能执行逻辑，确保整个程序是没有bug的，如果有，立刻指出bug在哪里。

我请大家好好体会一下这个东西有多牛逼，对于一个复杂的程序，这个数学模型要check几万亿种可能的输入，上千万种可能的执行路径，来让程序猿说一声：我们的目标是？没有bug！

一般听上去太牛逼的事儿，都不太靠谱。形式验证也是一样的。随便应用到任何程序的话，形式验证的算法复杂度是EXPTIME。说人话就是：超级超级超级难，根本搞不了。但是通过各种特殊化，在一些特定的情况下，形式验证是可以使用的。形式验证这种东西目前大量的使用在航空航天，芯片制造等正确性至关重要的领域，一些新兴的网络公司也在做网络系统的的特殊化形式化验证，来确保网络中没有bug，比如这家公司 veriflow.net

扯远了，说回到智能合约。想必说了这么多，大家也明白老董说的曙光是什么了：就是智能合约形式验证。智能合约的形式验证还是很初级的阶段，未来如何发展还很不确定，但是鉴于智能合约是直接跟钱打交道的，老董认为形式验证一定是将来智能合约技术栈中的关键一环，负责对一些DAPP中的关键和核心的模块提供安全性保证。当然现在也有新的区块链平台在推崇所谓的“correct by construct”，就是直接提供一个“可验证”的上层编程语言。因为老董设计利益相关，并且不提供投资建议，就不指名道姓了。

但形式验证永远无法解决所有的程序正确性问题，因为不仅验证的过程是超级难，当程序逻辑本身复杂的时候，定义针对程序的特定不变式也成了一个非常困难的问题。

老董认为要彻底解决智能合约安全性问题，需要站在一个更高的角度，从程序设计与工程实践的“人”的角度去入手。

这涉及到老董区块链技术研究俱乐部的一个成员正在做的：一个不破坏智能合约自治性的的漏洞修复的系统框架。因为是比较cutting-edge的东西还不太成熟，老董这里就不细讲了。

---

作者简介：

老董（BS'12, PhD' 17），UIUC计算机科学系博士，主要研究领域：高速低延迟广域网数据传输系统，网络安全与形式验证，博弈论，企业软件定义数据中心架构，分布式系统。

博士期间作为创始成员加入网络安全初创公司Veriflow，现担任核心算法与系统架构技术团队负责人，同时兼任大客户管理和一部分市场运营的工作。

在业余时间，老董是区块链技术爱好者，区块链技术全栈工程师。