建立值得完全信賴的智能合約和區塊鏈生態系

建立值得完全信赖的智能合约和区块链生态系统

我是顾荣辉，哥伦比亚大学计算机科学系助理教授，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的安全合作伙伴

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

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

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

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

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

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

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

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

区块链游戏以太坊智能合约区块链是什么意思区块链应用智能合约证券骗局区块链的中国骗局区块链投资骗局区块链怎么赚钱区块链技术区块链是什么通俗解释区块链dapp区块链是什么智能合约是一段代码