案例三·CertiK
由于智能合约一旦上传，即公开且不可更改，因此“区块链 2.0 ”时代的大多项目都产生了安全性验证的需求。CertiK 看好这一服务机会，致力于应用形式化验证技术，为智能合约和区块链生态提供安全保护。
在传统测试方法中，开发者会预想哪些情况下系统会遭攻击，再针对这些情景测试。这套方法的缺陷在于，黑客往往是从程序员想象之外的路径“下手”。而 CertiK 采用的形式化验证 ( Formal Verification )，将智能合约转化为数学模型，通过逻辑上的推理演算来验证模型，从而证明智能合约的安全性。因为整个演算过程符合严谨缜密的数学逻辑，所以其检验的结果很难被黑客攻克。
CertiK 的核心产品是 CertiKOS 防黑客操作系统。此系统花费千万美元的科研经费，两位创始人邵中和顾荣辉用 6 年多的时间来研究安全系统。目前 CertiKOS 不仅在商业市场中通过验证，也被应用到军事防御系统上，并引起耶鲁大学等美国学术界的关注。
由于军方需求相对复杂，创始团队于 2015 年中提出了分层结构理论，即将复杂的合约模块化，先逐个验证，再复合证明。
CertiK 的商业模式分两步走：
1. 依靠 CertiK 自身算力的中心化验证服务。如果客户本身有强大的硬件设备和系统，可向 CertiK 提交智能合约和需求，CertiK 将合约转化为数学模型，进行形式化验证，并生成报告，指明合约中哪一行可能出现漏洞，系统在什么状态或条件下可能被侵入。CertiK 根据合约的复杂程度收取不同的服务费。
2. 去中心化的安全验证生态系统，借助社区参与者的算力，共同生成报告。前文提到的分层结构理论可将复杂任务拆分成小的模块，CertiK 接到客户需求后，将“任务”和技术工具分发给社区，奖励提供算力、帮助检验小型模块的贡献者。交叉验证机制可以确保社区内无人投机取巧、没完成任务还“骗取奖励”。CertiK 认为，这种任务分发要比算 hash 值挖矿更有意义、更低能耗。
CertiK 现已与 NEO 、量子链等机构达成战略合作，同时对市面上的智能合约进行安全性验证，发现安全漏洞后主动联系团队，说明问题，提供解决方案，获取信任和口碑，逐步积累成功案例，再进行市场宣传。
据介绍，CertiK 已获耶鲁大学，丹华资本，光速中国等机构种子轮融资（金额暂未透露）。
CertiK 的核心优势在于团队。位于硅谷的技术团队从学术圈出身，去年开始商业化，工程师全部来自 Google、Facebook、Freewheel。联合创始人邵中，普林斯顿大学博士、耶鲁大学计算机系系主任/终身教授、中科大名誉院长、清华大学大师讲习团成员，20 余年安全领域经验。联合创始人顾荣辉，清华大学本科、耶鲁大学博士、哥伦比亚大学助理教授。
版权申明：本内容来自于互联网，属第三方汇集推荐平台。本文的版权归原作者所有，文章言论不代表链门户的观点，链门户不承担任何法律责任。如有侵权请联系QQ：3341927519进行反馈。
