CertiK联合创始人顾荣辉：形式化验证 为智能合约提供更高安全保障 | 金色财经独家专访

区块链技术所蕴含的经济价值长期以来始终诱使着不法分子利用各种攻击手段谋取暴利。据网络安全公司Carbon Black的调查数据显示，2018年上半年，全球范围内大约价值11亿美元的数字资产被盗，且因安全事件所造成的损失金额还在不断攀升。区块链技术和其安全性问题始终是业内关注的重点。

智能合约的优势在于透明化和去中心化，但也因此，它必须保障源代码完全公开。这就意味着，相比于传统程序，智能合约更易受到黑客的攻击。攻击传统程序就像闭卷考试，比如攻击阿里的系统，完全是黑盒攻击，根本无法走近它的代码。而攻击智能合约就好比是开卷考试，黑客可以针对源代码进行攻击，极大的降低了攻击难度。加上如今越来越多的智能合约写就的程序被投入商业用途，成为数字金融交易的枢纽，攻击智能合约的获利空间变得更加明显，甚至提供了一定的半径粘性，对黑客来说更具吸引力。

为了最大程度地保护用户利益，业界也会使用相应的手段以保障智能合约的安全性。传统的安全手段多为测试加实时监控。测试需要运行程序，通过各种可能性的输入，检测是否存在整数溢出漏洞等问题。但测试通常无法100%覆盖所有可能的情形，因而不能排除有未检测到的漏洞存在。也就是Dijkstra说过的那句名言：“测试只能用来说明有Bug，并不能说明没有Bug。”

实时监控则是当系统发现了一个漏洞之后，通过打补丁尽快修复。但区块链的智能合约是基于一种共识和去中心化的本质，一旦部署则难以修改，因此一旦出现问题很难进行迅速修复。测试加实时监控的方式或许在传统程序安全领域是值得信赖的安全手段，运用在区块链中则显得力不从心。智能合约需要一种能在上链前就基本达到100%安全无漏洞的安全保护，有些重要合约由于其本身牵扯到的经济价值不容小觑，对于安全性的要求更为严苛。目前，唯一能够为智能合约提供这样值得信赖的安全环境的技术叫做形式化验证。

相比多为测试和实时监控，形式化验证可以从数学逻辑上上保证合约中没有漏洞。它在两个层次上对合约进行保证，第一层次是安全无漏洞，即用数学推理的方法，捕捉合约中所有行为，覆盖所有的可能性，从而保证合约没有漏洞。第二层次是可信，即公开透明，合约的创建者不仅要说明执行哪些操作，还要向大家证明代码确实是这样执行的。经过这两个层次所验证过并证明安全的智能合约，只要源代码不发生任何变化，则能够保证100%安全无漏洞并且无法被黑客攻破。

CertiK是智能合约及区块链生态安全服务提供商，采用形式化验证将智能合约转化为数学模型，通过逻辑上的推理演算验证模型，从而证明智能合约的安全性。CertiK联合创始人顾荣辉在接受金色财经专访时这样定义形式化验证：用逻辑语言来描述规范，通过严谨的数学推演来检查给定的代码是否满足规范要求，从而证明智能合约或其他区块链代码的安全性。

顾荣辉，CertiK联合创始人，清华大学本科，耶鲁大学博士，哥伦比亚大学助理教授，系统软件形式验证领域专家。

顾荣辉解释道，形式化验证技术通过数学的方法证明程序是安全而正确的，从而在逻辑上保证了代码安全的完备性，完美解决了“零日漏洞”问题。CertiK平台旨在为建立完全可信的智能合约和区块链生态系统开发一个可靠的形式验证框架。

CeriK如今的形式化验证科技是从其核心技术成果CertiKOS防黑客操作系统衍生而来。CertiKOS是两位创始人用6年时间研究开发的安全系统，共花费上千万美元的科研经费。目前CertiKOS不仅在商业市场中通过验证，其核心技术推广也在美国多个高等学府展开科研项目，并引起了耶鲁大学等美国学术界的关注。

在CertiKOS的设计过程中，团队就已实现了基于层的分解和模块化验证技术，这一技术可以将复杂的智能合约验证任务分解为较小的容易验证的任务，进而在CertiK生态系统中进行分布式验证。各种证明对象都可以构建并编码到CertiK的交易中，然后由其他参与者验证。不仅如此，其他参与者的验证结果还可以由第三方快速检查、校验，以确保验证结果的真实可信。

因此，CertiK旨在作为证书来展示经过验证的智能合约、DApp以及区块链本身实现的安全性和正确性。

顾荣辉介绍，CertiK拥有三大优势，一是存在一套成熟的形式化验证框架和完整的理论基础，能够从数学原理上证明智能合约程序是否存在安全隐患；二是具有很高的可扩展性，基于智能标签与层级分解技术，CertiK能够将复杂的智能合约细化为不同模块，从而得以分布式验证，大大提高了安全验证的弹性与效率；三是CertiK具有较高的自动化程度，不依赖于人工审阅程序来进行验证，而是通过验证引擎和审计算法来自动完成合约验证，对人力依赖非常少，最大化的将源代码转为机器可检查的验证对象。

基于区块链领域对安全性的特殊要求，形式化验证才是未来区块链安全领域真正需要的解决方案。但这项技术的门槛非常高，目前世界范围内能提供相关服务的团队寥寥无几。而CertiK充分利用其技术优势，在该领域内占得先机，目前已积累了大量区块链行业知名机构和客户，有望成为形式化验证这一细分市场的领头羊。

据了解，CertiK凭借坚实的技术实力和创新能力，作为新崛起的区块链智能合约和信息安全服务提供商，已经与国内外知名数字货币交易所例如币安，火币，KuCoin等达成安全合作与服务推广，同时还与诸如小蚁（NEO）、量子链（QTUM）、本体（ONT）等十余个主流公链建立了战略合作关系。同时还获得了币安实验室、比特大陆、丹华资本、光速中国等多家知名机构的战略资金支持。

同时，CertiK的核心团队成员几乎全部来自世界一流大学，用顾荣辉的话说：是一家拥有着常青藤血液的公司。善于发展行业痛点及细分市场，并能凭借自身技术实力快速开发满足市场需求的产品。CertiK的另一位联合创始人邵中是中科大少年班出身，普林斯顿大学博士，现任耶鲁大学计算机系系主任以及终身教授。首席科学家Vilhelm Sjoberg是宾夕法尼亚大学博士，曾任耶鲁大学研究科学家，是软件验证、编程语言和类型系统领域的专家。首席运营官Daryl Hok曾任FiscalNote公司发展部副总监，曾主导对经济学人集团旗下CQ Roll Call的收购。在工程开发方面，CertiK拥有近20位工程师，大多来自Google、Facebook等全球知名企业的资深工程师。

最后，顾荣辉表达了对智能合约未来场景的积极展望：“智能合约可以看作是传统合约的数字版本，践行代码即法律的理念。任何参与方都可以在任何应用层进行创建，并且相当于用代码来实现、来表述以及去执行传统的合约。它提供了一种非常迅捷有效的实现方式，并且我认为它提供的安全保障将会更加透明化、更加可信。未来会有更加广泛的应用场景！”