如何将区块链生态建立在信任之上

我是顾荣辉，哥伦比亚大学计算机科学系助理教授，CertiK联合创始人。很多朋友曾问我这些问题——或许在座的很多人也经常被问起：比特币的价值在哪里？以太坊的价值在哪里？为什么区块链如此受欢迎？

我认为，答案在一个词中：信任。

区块链生态建立在信任之上。有些人称其为“共识”，有些人称其为“信仰”。

然而，由于一些程序漏洞，搭建这些区块链生态的代码是脆弱且难以被完全信赖的。

一旦漏洞被黑客所利用，所造成的不仅是数字资产的损失，更是信任的崩塌。对一个健康的去中心化社区的发展十分不利。

在过去的几年间，我们见到了很多黑客利用这些系统漏洞，价值十几亿以上美金的数字货币被盗。

区块链生态系统比我们想象的还要脆弱，智能合约安全问题不容小觑。

那么，我们该怎样避免这些程序漏洞？有没有任何解决方案？比如说，是否可以寄希望于程序测试、白帽黑客？

很遗憾，答案或许是：不。

Edsger Dijskstra曾说过：测试可以被用来证明漏洞的存在，但并不能证明程序不存在漏洞。

白帽黑客和程序测试方法确实非常有用，并且被行业所需要。然而遗憾的是，他们由于自身的局限性，无法满足区块链所有的安全需求。

那么我们还能做些什么？

在座的你们也许已经知道答案——形式化验证才是最终的解决方案。

根据 NSF 2016的报告显示，为了达到程序系统的绝对安全，形式化验证是唯一值得信赖的方法。

通过形式化验证，我们使用数学模型去验证代码确实符合给定的规范。

你们心里或许会有这个疑问：形式化验证的概念已经被提出了数十年之久。既然这么厉害，为什么这个方法还没有被广泛应用？为什么如今的代码中还是有这么多的程序漏洞？

——在大多数的实际案例中，完全的形式化证明的实现非常困难。

2015年，耶鲁大学计算机科学系主任邵中教授和我提出了“深度规范”的概念，我们发现，形式化验证真正的瓶颈并不在“如何去证明”，而是在“如何更好地表达程序设计的意图（或规范）”。

“深度规范”最强大的地方是可以证明“复杂系统的正确性” ，这类系统在之前被认为是很难证明的。

区块链的公链就是一个典型的复杂的分布式系统。

利用这套技术，我们可以把一个复杂系统（并发的或者分布式的）进行分层、整合，实现完备的智能合约验证。

目前，“深度规范”的概念已经被广泛学习和讨论。除了耶鲁大学和哥伦比亚大学，还包括来自普林斯顿大学，宾夕法尼亚大学，麻省理工大学等高校的学者。已经举办了三次深度规范学术研讨会和两次暑期学校。

在2016年，我们利用“深度规范”实现了CertiKOS——世界第一个被完全验证了的并发式操作系统内核。这个系统已经被部署到了未来机器人Landshark等对安全要求非常高的领域，当时验收方请来了由谷歌工程师组成的黑客团队进行评测，其报告评价CertiKOS是“无懈可击”的。

在2017年，我们开始将这个技术运用到区块链领域中。软件安全公司CertiK应运而生。

上图是运用“深度规范”保护智能合约的例子：对于非常复杂的智能合约，（比如像我们的稳定币客户TrueUSD的合约）我们首先用标签的形式写下合约的规范，（部分规范也可以被自动生成）。之后，我们将将复杂的智能合约拆分为较小的可验证的模块，在不同的抽象层进行证明。最后，我们将经过证明的模块合并到一起，生成整个合约正确性的证书。

上图是CertiK如何检测到美链（BEC）的智能合约漏洞的例子。我们先用标签的方式把规范添加到智能合约中。一旦某个模块的验证失败，该模块的程序漏洞——也就是V神所说过的“程序实现与程序员意图之间的区别”——就能被检测出来。

同时，我们的技术也可以找到触发程序漏洞的方法，当所有程序漏洞被修复并通过验证后，CertiK即可生成智能合约“不存在漏洞”的证明。

这个“不存在漏洞”的证明，是其他比如程序测试和白帽黑客技术无法实现的。

我之前提到过，有些规范（或标签）是可以被自动生成的。这项技术叫做“智能标签”，由CertiK团队独立研发而成。

基于“智能标签”技术，CertiK在几个月之前发布了安全漏洞扫描引擎CASE。

CASE可以扫描已部署在区块链系统中的智能合约。通过智能标签技术生成合约规范，并对合约进行安全验证。

在最近一次耗时数小时的扫描中，我们发现，币值前500的智能合约中有超过50个智能合约存在安全漏洞，包括3种高危漏洞，2种中危漏洞，和11种低危漏洞，涉及到的总币值高达四千万美金。

从2018年五月开始，我们开始了和NEO的合作，共同为NEO的生态系统建立形式化验证平台，这个项目目前已经如期启动，并且预计会在今年陆续发布相关产品和资料。

我们在大约一年前上线了代码安全验证服务。迄今，我们完成了超过160份代码安全审计，累计大约九万行代码。守护了价值超过12亿美金的数字资产。

一年来，我们的服务已经被区块链领域的主流机构所承认和采纳——CertiK是唯一同时被币安、火币、OKEx等全球主流交易所所认证的安全服务商，也是全球顶级公链平台如NEO、Waves、本体、ICON、Qtum、Quarkchain的安全合作伙伴。

同时，我们也为诸多业内知名项目如Crypto.com，TrueUSD，Celer，IoTex等提供了安全审计、定制化安全防御、渗透测试等一站式安全解决方案。

现在让我们把目光放到一个新的研究项目上——DeepSEA Blockchain。

我们已经讨论了如何检测已部署合约的程序漏洞，而更加重要的问题是：我们是否可以从最开始直接开发出没有程序漏洞的，可完全被信赖的智能合约？

为了探索这个问题的答案，我们开始了DeepSEA项目。

我们计划引入DeepSEA函数式编程语言，并为包括IBM超级账本、EVM等平台提供无漏洞的DeepSEA编译器。

——也就是说，如果源代码是正确的，那么被编译之后的机器码也是正确的。

同时，我们可以从DeepSEA源代码中将程序规范导入Coq证明辅助器，然后在Coq中对程序进行手动或者半自动证明。

DeepSEA Blockchain项目致力于构建跨平台的，可信赖的智能合约框架，由CertiK，哥伦比亚大学和耶鲁大学共同合作推进。我们已经获得了来自IBM、以太坊基金会和Qtum基金会的科研奖金，也诚挚地希望可以得到更多社区的支持，帮助我们将该框架理念发展到下一个阶段。