对话哥伦比亚大学教授——带你深入了解形式化验证技术

在智能合约框架下，事先检查合约本身是否存在机制漏洞，是解决其安全问题的关键。

而形式化验证（Formal Verification）正是用数学方法验证程序的正确性，为智能合约和区块链应用提供安全服务的技术。

9月2日晚8点，Unitimes成功举办第二期区块链技术与应用AMA活动。我们有幸邀请到了CertiK联合创始人、哥伦比亚大学教授顾荣辉为大家带来了主题为“带你深入了解形式化验证技术”的分享。

本次AMA分为两个环节：

• 固定问答环节

• 自由问答环节

固定问答——

顾教授从形式化验证的概念说起，图文并茂地介绍了CertiK是如何使用这项技术来为智能合约和区块链应用保驾护航的。此外，他谈到了CertiK团队的情况及其社区建设的计划。最后，顾教授还对形式化验证技术的学习和研究者提出了寄语。

以下为具体内容：

顾：大家好，我是顾荣辉，现在是哥伦比亚大学CS助理教授。2011年本科毕业于清华大学，2016年博士毕业于耶鲁大学。致力于软件系统形式化验证的研究，联合创建了CertiK项目，致力于通过深度规范技术，构建可靠安全的区块链生态。

CertiK的另一位联合创始人邵中教授，是耶鲁大学计算机系系主任、终身冠名教授，是形式化验证领域的世界级专家。2016年，我和邵中教授一起设计并开发了首个经过完全验证的并发操作系统内核CertiKOS。

CertiK有16位工程师，大多是之前Google、Facebook的资深工程师。我们目前有三位科研人员，我和邵教授在耶鲁与哥大的实验室也会为CertiK持续提供科研成果，光邵教授的实验室就有20位左右的博士生、博士后以及访问学者。

顾：简而言之，“形式化验证”就是通过数学的方法证明程序是“正确的”。这里的正确性，指的是，程序的实现，与程序员的设计或意图（我们称作规范）是相符的。

V神说过，所有程序的bug，都是由“程序的实现，与程序员的意图之间有区别”导致的。形式化验证，就是希望通过数学方法，证明没有这种“区别”。

我这里举一个例子：

假设左边的是程序员的意图，实现一个算(x+1)的平方。右边是一段程序，完成了指定的计算。普通的安全测试，就是找几个输入，看看输出是不是相符。例如：

比如x = 0, x= 1。

如果不相符，立刻就可以找到bug。可是即使所有测试都满足，也未必说明是正确的。例如，下面这个错误的程序也满足所有测试。

形式化验证，是试图证明，在所有情况下，两者都相符，证明的过程如下：

先用数学上的“结合律”，然后提取公因式，然后交换律，再提取公因数，最后根据平方的定义，可证。

形式化验证，看起来很cool，但是实际非常困难。之前大家普遍认为“一个像并发式操作系统内核那样复杂的系统，是很难甚至无法完全形式化验证的”。

2016年，在OSDI16（顶级计算机会议）上，我和邵中教授一起展示了CertiKOS，第一次让大家确认并发式操作系统内核是可以被完全形式化证明的。

顾：首先，操作系统内核，可以被看做当前计算机系统的基础，它的地位相当于区块链世界的公链（或者虚拟机）。安全性的保证至关重要，传统的安全测试无法满足要求。

可是，对于多核的、并发的操作系统内核，因为太过复杂，之前一直无法通过数学的方法被完全证明。像我刚才所说，很多科学家认为“一个像并发式操作系统内核那样复杂的系统，是很难甚至无法完全形式化验证的”。

2015年我和邵中教授一起提出了“深度规范”的概念，大概的想法是“形式化验证”的瓶颈，不是在“如何证明”，而是在“如何写出好的意图（或规范）”。

利用这套技术，我们可以把一个复杂系统（并发的，或者分布式的）进行解构、分层，从而更加自动化的进行证明。

我们利用深度规范，实现了CertiKOS，最后被部署到了一个未来机器人上。当时验收方请来了由谷歌工程师组成的黑客团队进行评测，给出的报告对CertiKOS的描述是“无懈可击”。

顾：CertiK的目标是构建完全可信的区块链生态，我们正在做的事情有如下几件：

1）最简单的，我们可以帮助项目方，验证智能合约，保证安全性。

2）其次，我们正在开发一套新的智能合约语言，DeepSea。在9月8日香港举行ETHIS上，我们的首席科学家Vilhelm Sjöberg会第一次展示这个语言。DeepSea可以帮助开发者开发更加安全高效的智能合约，并且通过我们设计的被完全验证过的编译器，被编译成bytecode的过程，也是正确的。

3）我们可以与公链合作，保证公链生态的健康发展。比如我们和NEO、星云链、量子链、本体、ICON、Waves等的合作。以星云链为例子，他们开发了一套基于Javascript的智能合约语言，我们帮他们也实现了一个形式化验证框架。

4）与交易所的合作。大家可能知道，我们是币安孵化的。同时已经与各大交易所进行了安全合作，比如火币、OKEx、Fcoin、Gate、KuCoin、币信等。

顾：绝大部分的智能合约都可以被安全验证，因为相对而言，它的执行模型比较简单。CertiK曾经率先发现了很多智能合约的问题。

上面这个图，是利用CertiK的引擎检测出EduCoin的Bug。之前我们还发布了关于美链等的Bug检测的消息。

昨天，我们发布了CertiK的第一代自动验证引擎（CASE），可以自动扫描并定位智能合约里的漏洞。

顾：自动引擎CASE，会首先根据智能合约的类型、代码、注释等信息，自动生成标签“label”，这个过程，我们叫做“smart labeling”。然后CertiK会将这套标签转化成“规范（specification）”。

CertiK会利用形式化验证技术，试图证明规范与实现之间是相符的。任何不符之处，都会以bug的形式，爆出。这套系统化是完全自动化的，可以为企业级客户进行24小时不间断的扫描，从而提前发出安全预警。

但是自动扫描的安全保证，是要弱于有人工干预的形式化验证的。在目前CertiK的半自动验证服务中，我们会请专家为智能合约“手写”规范，这个规范更加详细，更加全面，更加可靠。剩下的所有工作仍然是全自动的。

当然在找到问题后，我们的专家也会与客户沟通，帮助他们修复漏洞。

顾：这个问题很好。刚才我提到的，大概的想法是“形式化验证”的瓶颈，不是在“如何证明”，而是在“如何写出好的意图（或规范）”。

基于这个研究，2015年我和邵中教授一起提出了“深度规范”的概念。目前这个概念已经被广泛学习、讨论。目前DeepSpec社区，除了耶鲁大学和哥大。还包括普林斯顿、宾大、MIT等。

已经举办了三次workshop，两次暑期学校。上次暑期学校，V神也有邀请来讲课，大家讨论了深度规范与以太坊结合的可能性。

深度规范最强大的地方，是可以帮我们证明“复杂系统的正确性”，尤其是“并发式的或者分布式的”。这类系统之前被认为是很难证明的。比如区块链的公链，就是一个典型的复杂，分布式系统。

2016年，在OSDI16（顶级计算机会议）上，我和邵中教授一起展示了用深度规范（DeepSpec）构建的CertiKOS，第一次让大家确认并发式操作系统内核是可以被完全形式化证明的。两年过去了，我们的科研团队仍然是唯一拥有这项技术的。

我们认为，区块链系统，比如EVM，是至少与并发式操作系统内核同等复杂，甚至是更加复杂的。所以，相比较于其他团队（包括其他顶级科研单位比如MIT、普林斯顿等），CertiK可能是距离这个目标最近的。

顾：我们竞争对手有如下几类：

1) 传统的安全公司，这类公司对区块链安全有一定的保障能力，尤其是超级节点等（传统安全擅长的范畴）。可是无法满足区块链时代新的要求。

2) 其他提供形式化验证服务的公司。根据我刚才的描述，其实大家可以看出来，形式化验证的局限性很大，目前可以证明并发式或者分布式复杂系统的团队，只有CertiK，这个在学术界都是比较公认的。所以其他竞争公司，对我们的影响比较小。

顾：我这里简要介绍一下，首先我们之前已经建设了深度规范社区，已经初具规模，并且都是由各大国际名校的博士生构成的，这个也是CertiK开发社区的主要贡献者。

其次，我们在与各大公链、交易所、矿池进行合作。我们的合作机构有交易所（币安Labs、OK、KuCoin、Gate等），加密货币基金（FBG、节点、Kenetic、NGC、SigNum等），传统VC（光速中国、经纬中国、丹华等），矿主（比特大陆、嘉楠耘智旗下基金等），以及各大公链平台（NEO、星云链、量子链、本体、ICON、Waves等）。这也是我们构建社区的重要一环。

顾：区块链世界坚信“Code is Law”以及“In math, we trust”，但是代码本身，是会有bug的，很多时候是“不可信”的。希望大家可以拥抱形式化验证，拥抱深度规范技术，真正地去构建“可信代码”。

自由问答——

固定问答环节结束后，参与此次AMA的成员可以自由提问。以下为Unitimes从群成员的提问中精选的几个问答：

顾：DeepSea首先会帮开发者避免犯一些低级错误。但是功能正确性，还是需要进行单独的验证。不过DeepSea开发的智能合约，CertiK可以更加简单快速的验证。

顾：这个问题很好。传统软件项目，相对而言都比较复杂，形式化验证难度很高，很多对安全的要求却没那么高，大家可以注意到CertiKOS是2016年才开发出来的技术，是很新的技术。在传统软件领域，我们已经开始与无人车进行合作。

顾：很好的问题。目前形式化验证，包括深度规范，主要的目的是“证明代码没有bug”，在这个过程中，可以顺带找到系统的漏洞。它的目标与传统安全领域的“找bug”不同。但是我们确实没办法自动修复bug，只能提供触发漏洞的方式，以及代码定位，帮助开发者修复bug。

顾：我们首先需要知道（或者定义）这个函数的前置条件，比如x的范围等。然后定义函数的后置条件，比如y与x的关系以及y应该满足的性质（比如永远不可能为0等）。最后证明在前置条件符合的情况下，后置条件满足。

顾：1) 是的，对于不同的需求需要有不同的规范描述。我们有一套智能写规范的系统，目前可以用于像智能合约这种简单的程序。对于复杂系统，还是需要专家来书写规范。当有了规范，引擎是用来证明代码满足规范的。2) 会的，我们会推出第三方库。目前应该是会先推出DeepSea的第三方验证库。

顾：这个问题很好，现在的安全验证成本确实更高。CertiK的引擎是完全自动化的，这已经减少了很多人力成本。目前CertiK绝大部分的人力成本，是手工书写“规范”。这也是为什么我们一直在致力于自动化的辅助添加标签，再把标签转化为规范的技术。希望可以大大减少人力成本。

顾：我觉得潜在的安全危险，还是在“公链的安全”上。现在大部分的公司都是在关注“智能合约的安全”，说实话，是因为简单，门槛低。但是公链局限性或者是安全性，是更大的挑战。

顾：CertiK的很多产品都会陆续开源。比如我们的深度规范技术系列，不仅很多都开源了，我们还开了课程（在耶鲁），甚至是公开课（暑期学校）。DeepSea也会马上开源。我们智能合约的验证引擎，会在适当的时候开源。

顾：一是公链提供的编程语言，Solidity确实还是有很多不足。很多公链都在尝试。但是需要注意的一点是编译器，这些高级语言的编译器是否是安全的呢？这也是我们再大力推广的。

二公链的实现本身。很多公链确实很复杂，虽然经过了很多测试，但也很难保证完全的正确性。这点需要进一步的验证。很多公链上的实现，比如plasma，设计上是跨越了多层抽象层，相对较为复杂。这块的安全验证需要重视。最后是局限性，比如如何更好的实现“随机数”。

顾：好问题，函数式语言的优势在于，不容易犯低级错误，以及更加容易被安全验证。DeepSea也是函数式语言，所以我们也可以为这些公链提供服务。