让黑客从良？一种无法被黑客攻破的技术？！
硅谷Live / 实地探访 / 热点探秘 / 深度探讨
两年前的一个夜晚，熟睡了的计算机教授 Gun 被一旁的电话铃声震醒。
“快起来，我们被黑客攻击了！”
夜晚的寂静和睡意的朦胧感被电话外的这句话瞬间打破，Gun 立马掀开被子从床上跳起来，而下床的那一刻他已经知道要完了。
当所有人开始采取防御措施的时候，这场黑客的攻击已经结束。那晚，黑客们卷走了智能合约上价值千万美元的以太币。
这一次被盗事件不但成了许多人职业上的黑点，一个区块链项目的终结，也让信任他们的用户蒙受了巨大的损失。
而两年后的今天，数字资产被盗仍然是一个严重的问题。
区块链的业内人士正集体盼望着一种可以解决智能合约和区块链安全问题可行的技术方案的出现，包括聪哥我。
可以说只要安全问题没得到很好的解决，区块链领域的发展就会严重受到阻碍。
最近，小本聪的好友 Ken 向哥介绍了一个公司叫 CertiK。Ken 告诉聪哥，“CertiK 不但可以解决智能合约和区块链领域的安全问题，所有程序上的安全问题都会得到解决，未来的黑客们都将从良。”
能让黑客从良，这么牛 ？聪哥决定让 Ken 向大家介绍一下 CertiK：
CertiK 是什么？
（certik.org）
用一句最简单的话概括, CeriK 是一家用形式化验证为智能合约和区块链应用提供最先进安全性服务的公司。
而形式化验证（Formal Verification）又是什么？用 CertiK 联合创始人顾荣辉的话来说就是：用逻辑语言来描述规范，通过严谨的数学推演来检查给定的系统是否满足要求。
那么，为什么形式化验证可以解决现有区块链所面临的安全问题呢？
理解这问题前，我们需要先从四个点去了解智能合约在安全方面存在的问题：
第一，不可逆性：智能合约一旦发布在区块链上，合约的源代码是无法被修改的。
第二，代码开源：在平时不公开源代码的情况下都能被黑客攻击，更何况大多数区块链项目的代码都是开源的。开源只会让黑客的攻击将变得更加容易。
第三，成本高：如果将智能合约放在区块链上进行不断的安全测试，资产的不断转换会是一笔很大的开销。
第四，思维设限：即使开发者会预想智能合约在哪些情况下会遭攻击，再针对这些情景测试，但黑客的厉害之处在于，可以从程序员预想之外的路径下手。
正因为这四个方面让区块链上的数字资产很容易被黑客掠夺。
CertiK 能检测到开源代码的安全漏洞，从而告知开发人员，以至于在智能合约发布前就保证了安全性。依据数学原理的自动化推演，避免了人为检测的思维局限，而自动化验证也让智能合约验证的费用降到了最低。
其实形式化验证早在 2016 年以太坊开发者大会（Devcon2）上就成为热门话题，但一直存在着一定的争议性。
（Devco2：How can Formal Vertication Help)
争议性在于，用数学推演验证软件程序，在确保不同的网络元件接受指令并以用户的身份模拟执行预定程序的过程中，需要人工输入等技术限制，如何运用各种工具包来整合形式化验证，还存在着诸多制约性的因素。
但 CertiK 的出现很好的整合了形式化验证。只要你学过编程，就能很方便地用 CertiK 提供的教程说明来测试智能合约的安全问题。
我们来看一看产品：
你要做的，就是打开 CertiK 的系统，上传你要检测的智能合约，用 CertiK 提供的标记语言，标注好要进行测试的代码部分，按下检测按钮。
检测完毕后， CertiK 会给你提供这份智能合约的安全系数，并告诉你哪一块程序存在着错误，并提供详细的解决方案。
当你根据 CertiK 的解释进行修改，修改完后再进行测试，直到达到 CertiK 100分的安全评级，你的智能合约就可以避免安全漏洞受到黑客攻击。
是不是很简单！简直是智能合约开发者们的福音，黑客们的噩梦。
CertiK 的验证过程体现了化整为零的解题思想，将一个难以证明的大问题拆分为许多容易证明的小问题，然后再将证明过的小问题重新组合回分解之前的较难的大问题，并且保证其中从端到端的正确性（end-to-end guarantees）。
在这个过程中，这些小问题都将发送给整个社区，社区的开发者们可以利用 CertiK 提供的方法，也可以运用自己的算法来证明这些问题。一旦某个问题通过多方独立的开发者的验证，那么其便可以用来作为建立其他理论的依据，从而形成互助协作的技术机制和良好的社区氛围。
CertiK 是如何让智能合约的安全检测做到如此简单的？
团队
这就不得不提 CertiK 背后的团队了：CertiK 的联合创始人顾荣辉从清华大学本科毕业，耶鲁大学的博士，现为哥伦比亚大学计算机系助理教授。
CertiK 的联合创始人邵中，是普林斯顿大学的博士，耶鲁大学计算机系的主任和 Thomas L. Kempner 冠名教授，中科大大师讲席教授，有 20 余年的安全领域经验。
无法被黑客攻破的操作系统
介绍完膜拜三分的团队简历后，更牛的是邵中教授这位计算机程序语言设计的权威专家已经研发了经形式化验证过的无漏洞、无法被黑客攻破的操作系统：CertiKOS。CertiK 正是 CertiKOS 研究的一个延伸，利用数学证明的形式化验证方法开发完全可信经过验证的智能合约与区块链生态体系。
您已经看了全文的1/2了，休息一会：
这么牛的 CertiK 是谁推荐给聪哥的？
聪哥好友 Ken：
“我是 All In 区块链后再也不焦虑的 Ken，佛系炒币患者，U Network 北美社区负责人，爱写区块链相关的文章，坐标硅谷，欢迎交流。”
看看区块链安全市场有多大：
（以太坊创始人Vitalik)
Vitalik 在20岁创造的以太坊，打开了智能合约的潘多拉魔盒，成为黑客们致富的温床。
如今基于以太坊的智能合约在全球已经超过了一百万份，随着区块链入场的人越来越多，对智能合约的开发也水涨船高，智能合约的安全问题也逐渐被放大。
目前，一份智能合约的审核认证价格在市场上平均需要花费10万美金，可以说在未来是一个万亿级别的市场。
而从 2017 年全球爱西欧融资的角度来看，隐私和安全领域的区块链项目融资的占比只有1%。如果排除隐私类型的区块链项目，剩下专注在安全的项目占比就更小了，但这不能代表安全领域的区块链市场不被看好。
主要原因还在于区块链安全问题在 2017 年还没有受到市场足够的重视，而区块链安全领域项目的创业门槛较高，对大众的认知门槛也比其它项目更高。同时区块链安全领域项目 P2P 的社区模式也是一个很难的切入点。
看看其它项目：
Zeppelin 是一个社区驱动项目，它构建了安全智能合约的开源架构，目的在于实现安全智能合约的开发。目前有很多优质的海外区块链项目都采用了 Zeppelin 的智能合约安全服务。
但 CertiK 与 Zeppelin 最大的不同在于，Zeppelin 主要依赖专业的人士参与对智能合约的审核，而且主要针对程序性质的验证，并不支持 CertiK 程序功能正确性（Functional Correctness) 的验证。
Quantstamp 是一家智能合约的安全审计平台，是被 YC 录取的区块链公司，聪哥也在之前的文章介绍过 ：错过了区块链第一波淘金热？这家公司“卖铲子”被YC相中
和 Zeppelin 类似，Quantstamp 也需要人工的参与，同样不支持功能正确性的验证。
区块链公司 Axoni 不是一家专门做智能合约安全的公司。但他们最近也在专注与形式化验证技术。开发了专门服务于形式化验证的智能合约语言 Axlong。
与 CertiK 最大的不同点在于，CertiK 可以直接验证 Solidty 等各种语言，但 Axlong 想取代 Solidty。虽都是形式化验证技术，Axoni 实行的完全是一次曲线救国的形式化验证方式。
再看看投资人怎么说：
据了解，CertiK 已获耶鲁大学，丹华资本，光速中国等机构的支持。
作为 CertiK 的早期投资者，丹华资本董事总经理 Judy Yan 表示：“比特币仅为一条区块链，还有其他更多的公链和私链。目前有很多金融机构和相关团体都想打造自己的区块链，但无论如何，他们都需要解决区块链的安全性问题。”
斯坦福大学物理系的教授张首晟表示：“CertiK 是第一批提出利用数学证明的形式化验证方法来检查工程系统和智能合约安全性的团队。这将是区块链技术领域、甚至是科学领域的一大跨越式进步。”
耶鲁大学合作研究办公室（Yale OCR）的业务发展经理 Richard Anderson 称：“目前的区块链技术社区，极其容易受到黑客的攻击，但是耶鲁的这项技术将会改变世界。”
Ken还想说：
在形式化验证领域，邵教授已经是公认的最权威的专家之一。
我们可以看到的是，CertiK 不但为每个参与虚拟经济的个人提供了更强的安全保障，让每一位会编程的人能够参与到社区里来构建安全的网络环境，也让黑客“失业”后，给其一片净土（社区）去贡献他们的力量来获得合理的回报。
但如何让 CertiK 这项技术实现高效的 P2P 化，形成整个社区的安全生态，这将是一个区别与技术问题以外的挑战。
我相信 CertiK 的出现，将是区块链安全领域目前最浓重的一笔，真正形成了一个 “ In Math We Trust ”（我们只相信数学）的区块链生态。
看完这篇还不够？如果你也关注区块链领域，并且希望自己喜欢的区块链项目被我们报道，欢迎留言告诉我们！
推荐阅读
相关内容
微信扫码咨询专知VIP会员