你相信天底下有保证绝无漏洞的代码吗？你相信有一种方式可以保证让人写出这样无漏洞的代码吗？这件事听起来似乎太不真实，但一个由来自耶鲁和哥大背景的中国团队 CertiK，正在尝试推出这样的安全验证服务，要为黑客事件频发的区块链行业，建立起安全标准。
CertiK 是由耶鲁大学计算机系主任邵中与哥伦比亚大学计算机系教授顾荣辉联合创立，2017 年底正式成立于纽约及硅谷，核心技术为运用形式化验证（formal verification），为智能合约和区块链应用提供安全验证和生态安全解决方案。
图｜CertiK 联合创始人顾荣辉（来源：DeepTech）
2018 年全球区块链领域安全事件暴增 5～8 倍
目前，区块链堪称是风险最高、最容易发生黑客攻击、且行业安全意识又最低的领域之一。根据不同统计，2018 年全球区块链领域发生至少百起安全事件，与 2017 年相比暴增 5～8 倍。而损失总金额达 20～38 亿美元之间，对比目前全球加密货币总市值也不过约 1700 亿美元左右，这样的安全损失比例实在高得吓人。
区块链的安全攻击形式层出不穷，分层来看，从数据层、网络层、共识层、激励层、合约层，到应用层，都可以成为攻击切入的途径。其中，又以应用层攻击最多，智能合约更被认为是区块链安全事件的重灾区，最经典的案例就是 2016 年“The DAO”事件，黑客利用去中心化风险投资基金“The DAO”的智能合约漏洞，盗走 360 万枚以太币（当时价值约 5000 万美元），最后迫使整个以太坊采取激进的防卫措施创建硬分叉，才能挽回损失。
而 CertiK 截至目前，已累计为 150 家以上客户提供了安全验证服务，其中许多是加密资产相关平台，保护了总值近 13 亿美元的数字资产免受到黑客攻击，并保持着“零事故率”的记录。
其客户包含币安、火币、OKEX、比特大陆、以太坊基金会、量子链等加密货币与区块链行业知名公司。去年 10 月，CertiK 获得币安旗下投资机构——币安孵化器 Binance Labs 数百万美元的投资。币安孵化器 CEO 张灵（Ella Zhang）说，CertiK“解决了当今区块链生态中一个关键痛点，也同时保护我们的交易用户，正在逐步成为交易上币的行业标准。”
图｜CertiK 成立一年多成绩不斐（来源：CertiK）
而 CertiK 的可保证代码无漏洞的安全验证服务，其核心技术其实就是两位联合创始人绍中和顾荣辉，将他们在“形式化验证”（formal verification）领域的多年研究成果，打造成 CertiKOS 防黑客操作系统，这套系统在 2016 年就曾被美国国防高级研究计划局（DARPA）资助的”高保证网络军事系统（HACMS）”采用，成为该系统核心构件之一。
形式化验证，让人写出无漏洞代码
何谓形式化验证技术？真能让人写出无漏洞代码？
简而言之，形式化验证是通过数学逻辑来推理演算，从数学的角度证明一段程序、一个软件、或一个智能合约，不存在安全漏洞。每一个证明在逻辑上都承接上一个证明。通过形式化验证，一个这样的程序可以像证明数学定理一样，无论如何测试都一定会得到正确的结果。
顾荣辉对 DeepTech 解释，一般安全技术通常都是设法找出可能存在的漏洞，或是在概率上保证很大程度不会出错，但形式化验证是希望能够从数学上直接证明一个软件是正确的，“是目前已知的安全等级最高的一项技术”。
也就是说，通过形式化验证，在某种程度上可以保证能让人写出没有漏洞的代码。
“当然，这是建立在数学模型正确性的基础上，必须依赖很多的前提和假设”，顾荣辉补充，“但如果其前提条件可以被满足，那么最终它能达到安全等级是高于其它技术的。”
形式化验证其实是从 20 世纪 60、70 年代就开始兴起的研究方向，但由于对应用条件要求较高，无法处理较为复杂的软件系统，在大多数实际案例中，形式化证明的完全实现是非常困难的。因此形式化证明一直处于技术上突破有限、也苦于找不到理想应用领域的状态。直到 2015 年左右，绍中和顾荣辉将在形式化验证领域多年积累研究成果，具体研发成深度规范、分层结构等技术，才得到了比较大的突破。
话虽如此，形式化验证所适合应用的场景，仍偏向于代码不是太过复杂、条件相对单纯、但却价值很高的程序。而区块链正好符合这些特点，因为区块链往往是用相对有限的代码数量来对应高价值加密资产，且链上条件相对可控。更重要的是，因区块链不可篡改，代码漏洞修补困难，就更适合形式化验证这样的技术。
正因如此，适逢 2017 年比特币大涨带动区块链技术发展，CertiK 快速在这一行业找到落点，推出形式化验证平台，为包括智能合约、DApps 等所有区块链生态系统组件提供安全审计服务。
简单来说，CertiK 的服务是通过分层结构，对所要验证的某个复杂系统先进行分层，将软件模块拆分，然后再用深度规范进行复合证明，验证每一分层是否都符合规范。如此一来，便可同时提升安全验证的弹性和效率，将形式化验证应用在具体业务场景。
以某个稳定币客户为例，CertiK 为其智能合约所做的是，先用标签的形式写下合约的规范，然后将复杂的智能合约拆分为较小的可验证模块，在不同的抽象层进行证明。最后再将经过证明的模块合并起来，生成整个合约正确性的证书。
图｜运用“深度规范”保护智能合约（来源：CertiK）
针对智能合约的编程语言 DeepSEA
顾荣辉分析，区块链行业之所以安全事件高度频发，一方面是因为行业安全意识普遍低落、且对安全技术缺乏认识，许多区块链项目或平台并未将安全放在优先考量，不愿意投资安全建设。而即便是重视安全者，也不知该如何选择，可能付出高额费用，但是得到的安全加持非常有限。
另一方面，问题也出在区块链行业惯用的开发工具上。顾荣辉指出，现在区块链行业程序员普遍爱用 C++ 或 Python 来写智能合约，但这些工具从安全专业的角度来看，都是非常不安全的语言。尤其是 Python，天生就不适合用来开发对安全需求很高的系统。
“不同的语言就像工具一样，有不同的使用的方法，这就好像你用一个螺丝刀当钳子来使。”顾荣辉认为，如果整个行业大量依赖这些语言来从事开发，那么安全检测与验证相当于只是亡羊补牢。
因此，CertiK 近来推出一项新的编程语言 DeepSEA，这是一种针对智能合约的函数式智能合约编程语言，通过引入形式化验证技术，保证智能合约的安全性。
据顾荣辉解释，DeepSEA 可以说是一种“无漏洞的编译器”，可以证明源代码无漏洞，通过 DeepSEA-Blockchain 框架可以构建出跨平台的、可信赖的智能合约，目标是为 Hyperledger、EVM 等平台上的开发者提供一个安全可信赖的开发环境。
“我们的出发点是希望在源代码级别，从语言设计上引入安全的设计理念，可以在比较早期就杜绝一些很简单的安全错误”，顾荣辉说。
DeepSEA 推出以来，几个月内已陆续获得哥伦比亚-IBM 区块链中心的种子基金、以太坊基金会（Ethereum Foundation）第五批科研奖金，以及量子链（Qtum）科研经费等。
图｜CertiK 团队（来源：DeepTech）
此外，顾荣辉告诉 DeepTech，正式成立刚满一年不久的 CertiK，也已陆续融资约 3000 万美元。在资金支持下，CertiK 团队规模已成长至 20 余人，包括曾是谷歌 gVisor 创始人员的研发副总裁倪兆中和曾任职国际货币基金组织（IMF）经济学家的首席商务官阎开，团队分散在纽约、西雅图、北京、首尔等地，并将在今年持续完成更大规模扩张。
蜂拥而至的奖助与投资，凸显出区块链行业对于可信赖、标准化的安全建设存在迫切需求。目前，加密资产的安全环境仍然十分脆弱，如果包含 CertiK 在内的区块链安全服务提供商，能够成功使其产品被行业广为接受，也将有望从根本上改变区块链产业的生态。
