对于大部分不了解区块链的人来说，区块链代表着一种大胆、果敢和纯粹的互联网新浪潮。

这种描述在一定程度上算是比较贴切的。

但现实是，想要达到区块链融入全民生活的愿景，这个领域还有很长的路要走。

CertiK的联合创始人，哥伦比亚大学的顾荣辉教授在哥大校友活动上发表了讲话，他谈到了区块链的安全问题，形式化验证如何帮助解决这些问题，以及CertiK为建立可靠的区块链系统所做的工作等内容。

区块链之美

区块链，具体而言指的是：使用图灵完备的脚本语言的区块链。这是一项非常先进的技术。

区块链具备巨大的潜力，也许未来可以从根本上改变我们目前的信任关系和交易方式。

传统交易，例如交换两种资产，要求必须有诸如银行或托管账户等人们信任的第三方机构来代表交易双方进行交易。

而有了区块链技术，在交换两种数字资产时不再需要第三方参与，这就是我们所说的去中心化。用户只需要信任区块链上的一个小程序，也就是智能合约，相信它具有正确的交易逻辑编码即可。

人们深信去中心化的概念，比起相信第三方的管理系统和执行事务能力，用户更信任客观的程序。

但是，如果这个小程序或者说智能合约本身是错误的呢？

区块链的阴暗面

与其他计算机程序相似，智能合约也容易出现漏洞。造成这种现象的本质原因是程序员的设计意图和代码的实际实现之间产生了不匹配。

区块链世界中bug丛生，其中最具有代表意义的是导致了价值5000万美元密码资产损失的TheDAO“double-spend”攻击，。

2020年初，dForce DeFi智能合约中的一个漏洞导致2500万美元的损失。

根据福布斯进行的一项研究，仅仅在2019年上半年，就有超过40亿美元的密码资产被盗，这是多少家庭一辈子的资产总和？

因此在区块链的安全道路上，还有很长的一段路要走。

那么，如何才能防止这些智能合约漏洞的产生，以及避免由此导致的经济损失呢?

可证明软件正确性的测试

区块链领域的安全解决方案其一就是不断地测试。

然而，正如Edsger Dijkstra（图灵奖计算机科学家）所说，程序测试只能用来显示bug的存在，但永远不能证明它们不存在。

如果你是一个程序员，你的意图是为了计算以下内容：

然后你按照规范执行下列代码：

要测试这个程序，只需使用特定的输入运行程序，并将实际输出与预期输出进行比较。

在这个例子中，运行x=0且结果为1的程序。

然后在x=1时运行程序，结果为4。

看起来很简单，对吧？但是，这只是展示有限的测试用例列表，并不能保证整个程序的正确性。如果在程序的实现中，开发人员犯了一个错误，并且在不知情的情况下决定实现代码呢？如下图：

回想一下，规范（或程序员的本意）是：

那么这个漏洞百出的程序仍然可以通过测试。因为在x=0和x=1的情况下，即使程序是错误的，得出的结果也是正确的：

这就是目前测试方法的基本局限性。

那么除了测试以外，还有什么更好的办法避免区块链中的安全隐患呢？

形式化验证：可以更彻底地验证正确性

很多人，包括CertiK联合创始人，哥伦比亚大学的顾荣辉教授和耶鲁大学的邵中教授，都提到了形式化验证（关于形式化验证，请见参考链接1以及参考链接2中的内容）。这是“保证系统没有编程错误的唯一已知方法”。

在前文分享的例子中，测试方法导致了一些错误。

而在形式化验证中，是使用数学方法来证明一个程序符合程序员的设计意图或设计规范。从代码开始，就可以应用数学方式来分解和重新构建代码，以证明它符合设计规范。

下面的例子将一步步展示证明过程：

即使是这样一个简单的程序，形式化验证时也需要相当大的工作量。想象一下用这种方法验证复杂系统会有多难，比如验证现代处理器、OS内核和分布式区块链系统等。

因此有一部分说法认为，对这样的系统进行形式化验证是不可能完成的。

具备深度规范的形式化验证综合系统

为了应对复杂系统形式化验证的挑战，顾荣辉教授和CertiK技术团队假设：形式化验证的瓶颈不在于证明技术本身，而是在于开发人员为形式化验证编写规范的方式。

因此，团队开发了一种名为深度规范（Deep Specification，简称DeepSpec）的新技术。该技术允许用户编写可对话的规范，并创建证明和验证模块。通过这种方式，可以将原本极其繁琐的验证过程分解为许多更小、更容易解决的代码片段，从而减少了证明负担，并使复杂系统的形式化验证成为可能。

利用深度规范，顾荣辉和CertiK技术团队构建了世界上第一个完全经验证的多处理器操作系统内核——CertiKOS，它已被证明是无漏洞和防黑客的。

正如你所看到的，这一项工作已在许多顶级学术会议上被讨论过，并且被广泛认为是形式化验证方面的真正突破。

深度规范这种技术在2015年被命名。这项技术后来被NSF Expedition项目和各大社区进行研究和宣传。

使用DeepSpec保护智能合约

Deep Specification是如何帮助解决区块链中存在的安全问题？

有了DeepSpec技术和CertiK专有技术的结合，可以通过多种方式来确保智能合约的正确性。

假设现在有一个非常复杂的智能合约，它有许多相互依赖关系。下面是形式化验证智能合约的可视化表示：

第一步是通过添加标签作为智能合约的规范来注释源程序。

接下来，将智能合约的规范分解为各个抽象层的许多小组件，可以在其所属的层验证每个组件。

然后，开发人员可以进一步将所有经过验证的组件组合成一个有保证的、经过验证的智能合约，这样验证就完成了。

它将自动生成机器可检查的证明对象，也称为机器可检查的证书。用户可以在自己的机器上运行这个程序并检查证明。由CertiK验证的智能合约称为认证智能合约。

想要知道详细的CertiK形式化验证引擎演示过程，可直接跳转到本文视频中的13分40秒查看。

CertiK的起源与发展

2018年，CertiK在纽约成立。其使命是使用这种DeepSpec技术使区块链系统真正值得信赖，旨在使用数学的方式来保护加密世界。

CertiK的标志整体是一个盾（象征保护和安全），同时里面看起来像“倒着的A”的符号，在数学中的含义是“所有”（For All）：即隔绝所有的危险，同时保护所有（财产）的安全。

CertiK自2018年推出形式化验证服务以来，公司已经服务了超过150家企业客户，覆盖范围的行业和类型的项目包括加密货币交易所、稳定币、公链、去中心化金融、智能合约、钱包、块生产、体育和游戏类应用。

到目前为止，CertiK已经验证了超过60亿美元的加密资产，凡是经由CertiK验证的项目至今还从未被攻击者入侵。

但是抛开所有这些成就，区块链网络安全仍然是一个大问题。

那么问题在哪呢？为什么还没有找到解决这些安全问题的方法？

• 市场的成熟和安全需求

首先，尽管CertiK持续在为区块链安全做出贡献，但帮助的客户和保护的加密资产只是整个市场的一小部分，而整个市场的规模还在呈指数级增长。

目前没有可行的方法核实区块链市场上所有项目的安全性。

其次，智能合约只是区块链技术栈中的一层。编译器、虚拟机、共识协议、layer和节点都值得担心。栈中的任何漏洞都可能危及整个系统，并导致代币丢失。

区块链在不断发展。它目前的发展阶段与依赖ISPs为电子邮件地址的互联网时代相平行。

随着越来越多的公司和项目加入区块链领域，并见证整个市场价值的增长，人们可能会看到更多独特和复杂的用例，它们会带来更多并且更高标准的安全需求。

解决方法：CertiK的技术栈

出于保护加密世界的这个愿望，CertiK认识到需要一个端到端的解决方案来解决这个问题，在技术堆栈的每个级别上提供安全保障，从而保护所有的内容。CertiK技术团队已经开始建立CertiK技术栈。

团队在哥伦比亚大学和CertiK建立的一系列的产品和技术，包括:

1. DeepSEA工具链

2. CertiK Chain

3. NoOps：区块链的CertiKOS

• DeepSEA工具链

DeepSEA工具链（详情请见参考链接3）将有助于在开发阶段上防止出现错误。甚至不需要任何形式的验证或测试方法来证明程序的正确性，因为正确性是程序语言本身所固有的。

DeepSEA是第一种用于编写可靠的智能合约的编程语言，它在编程语言级别上减少了区块链程序的安全隐患，并使用强大的检查器进行加密，以帮助减少开发期间的bug。它自带有一个验证引擎，这意味着开发人员可以在开发软件时一边编写规范，一边运行形式化验证，不必等到合约部署后才验证。工具链还有一个经过验证的编译器，以保证编译阶段不会引入bug。目前，Github上（详情请见参考链接4），已经有了DeepSEA的v0.9版本。

DeepSEA由哥伦比亚大学，耶鲁大学和CertiK合作开发。由哥伦比亚- IBM区块链中心（详情请见参考链接5）、哥伦比亚数据科学研究所和其他哥伦比亚研究所支持。也得到了以太坊基金会和Qtum基金会等其他组织（详情请见参考链接6）的支持。

我们的目标是用这个工具链提供能够跨越超分类账、以太坊、CertiK Chain的值得信赖的智能合约，并帮助建立可靠的区块链生态系统。

• CertiK Chain

在区块链系统层面，CertiK开发了CertiK原生区块链：CertiK Chain。这是首个以安全为核心的公链，于2018年首次推出，第一个测试网于2019年11月推出，完整的测试网已于2020年3月推出。

CertiK Chain提供了CertiK虚拟机(也称为CVM)，能保证智能合约正确执行设计意图。因此，如果用户有由CertiK的验证引擎验证，并由CertiK的编译器编译的DeepSEA智能合约，那么这个智能合约的字节码就是正确的。

即使用户已经使用了正确的程序，但也需要确保虚拟机正确地执行字节码。CVM将确保这最后一步的可信度。

CertiK Chain还可以作为其他区块链平台的安全飞地。假设运行在另一个区块链上的智能合约得到了认证，那么可由机器检查的证书或证明可以存储在CertiK Chain上。这样一来，用户就可以检查想要调用的智能合约是否正确及安全。

• NoOps：区块链的CertiKOS

这个堆栈的底层提供的最后一项服务是NoOps。可以把它想象成区块链系统的CertiKOS。

前文描述过CertiKOS是世界上第一个完全经过验证的、无漏洞且防黑客的多处理器操作系统内核。

一旦有了NoOps，就能在区块链世界中部署CertiKOS，帮助保护所有节点和区块生产者。它为这些节点提供了最高级的保护，能确保大多数节点不会被黑客攻击，并且可以以良好的方式持续生成块。

可以通过访问【散养孩子也能上北大？NoOps新型节点运营产品神助攻】来了解更多关于NoOps的内容。也可以直接复制以下链接到浏览器查看NoOps产品官网：

https://noops.certikpowered.com/

CertiK未来发展计划

CertiK希望为区块链世界提供端到端的网络安全解决方案，通过提供有价值的产品来修复或支持生态系统中的每一个在哥伦比亚大学的实验室里制造出来的组件。

CertiK团队有30多名研究人员和工程师，以及20多名商务和市场运营人员。总部设在纽约，目前在西雅图、北京和首尔均设有分部。在不久的将来，会继续将分部设立在世界各地。

CertiK团队中的许多成员是哥伦比亚大学的校友，他们在本科、硕士甚至博士毕业之后加入了CertiK。还有很多团队成员来自耶鲁大学和其他著名大学以及其他高科技公司。

在CertiK，每一个人都相信端到端解决方案、形式化验证技术、深度规范技术和产品将是构建值得信赖的区块链系统的关键。

CertiK正在为团队补充新鲜血液，如果你想加入这个专业的团队，为区块链安全奉献出每一份力量，那么你可以访问以下链接查阅CertiK招聘及职位信息：

https://jobs.lever.co/certik/

中国区的职位申请也可以通过邮件联系我们：

商务（BD）、技术及产品职位申请，请发送简历到：yu.chen@certik.org

其他职位申请请发送简历至：beidi.jiang@certik.mobi

期待你的加入！

文中参考链接

1.https://certik.io/blog/technology/an-introduction-to-formal-verification

2.https://www.jinse.com/news/bitcoin/288836.html

3.https://certik.io/deepsea-blockchain/

4.https://github.com/CertiKProject/deepsea-preview

5.https://certik.io/blog/announcements/certik-co-founder-recieves-ibm-blockchain-grant-to-further-research-on-deepsea-framework-at-columbia-university

6.https://certik.io/blog/announcements/ethereum-foundation-awards-grant-for-deepsea-research-by-certik-yale-and-columbia-to-create-safer-smart-contracts

了解更多

General?Information:?info@certik.org

Audit?&?Partnerships:?bd@certik.org

Website:?certik.org

Twitter:?@certik.org

Telegram:?t.me/certik.org

Medium:medium.com/certik

币乎：bihu.com/people/1093109