CertiK，区块链世界的安全专家

CertiK是一个是形式化验证框架，为智能合约和区块链应用提供最先进安全性服务的公司。经过CertiK验证的智能合同、DApp以及区块链将会被附上证书形式的标志，来展示其正确性和安全性。

形式化验证(Formal Verification)：用逻辑语言来描述规范，通过严谨的数学推演来检查给定的系统是否满足要求。

市场需求：安全是区块链世界心中的痛

智能合约的出现使得区块链进入了2.0的发展阶段，尽管智能合约的发展十分迅猛,然而智能合约漏洞所导致的很多安全问题却给人们带来巨大的财产损失。众所周知，公链系统基于信任和开放，一旦部署就是不可更改的。因此任何错误都很容易遭受黑客的攻击。

2016年黑客通过The Dao，利用智能合约中的漏洞，成功盗取360万以太币。The DAO事件发生后，以太坊创始人Vitalik Buterin提议修改以太坊代码，对以太坊区块链实施硬分叉，将黑客盗取资金的交易记录回滚，在得到社区大部分矿工支持的同时也遭到了少数人的强烈反对，最终导致了以太坊社区的分裂。

军用级别的CertiK 系统如何运行？

CertiK区块链解决方案是在已成功应用的技术基础上开发的。CertiKOS是邵中教授领导的小组成功研发的世界上第一个反黑客攻击操作系统，这个系统共花费千万美元的科研经费，两位创始人邵中教授和顾荣辉教授用6年多时间研究安全系统，目前CertiKOS不仅在商业市场中通过验证，也被应用到军事防御系统上，并引起了耶鲁大学等美国学术界的关注。

军用级别的技术应用在区块链和智能合约安全性，是不是听起来很高大上，很复杂?其实CertiK客户端的使用非常简单，用户可以一键提交并可接收检测结果。

完整的验证过程运作流程如下：

· 首先，客户在客户端向CertiK网络提交智能合约或任何其他系统源代码。

· CertiK将代码的“正确性”转换为类似的数学问题，然后以化整为零的解题思想，将一个难以证明的大问题拆分为许多容易证明的小问题，并将这些问题广播到CertiK网络。

· 分布式的CertiK节点并开始协作解决这些数学问题，以此换取奖励。

· 节点把各自找到的解决方案反馈到CertiK区块链上，并可以随时被用于验证。

· CertiK再将证明过的小问题重新组合回分解之前的较难的大问题，并将这些解决方案总结，并以证书的方式发送回客户端。

· 这个证书将想客户确认，要么代码是安全的(无漏洞并课抵抗黑客)，要么会支持潜在的风险和漏洞。

· 如果检测出潜在的风险或者漏洞，CertiK会同时提供一些案例介绍这些风险或漏洞可能被攻击的潜在方式。

全明星团队配置：

CertiK由来自哥伦比亚和耶鲁的全明星科学家团队创建，并得到谷歌，Facebook和FreeWheel的高级软件工程师的支持。

该团队成立于硅谷和纽约市，由世界级的正式验证专家组成，他们是耶鲁大学计算机科学系教授邵中及其弟子、哥伦比亚大学计算机系助理教授顾荣辉。

邵中教授：

团队联合创始人，1988年本科毕业于中国科学技术大学，1989年至1994年就读于美国普林斯顿大学，获得计算机科学专业博士学位，1994年至今一直任教于耶鲁大学，目前是计算机科学系的教授和系主任。他是SML / NJ编译器的主要开发人员，也是FLINT认证基础架构的主要架构师。

顾荣辉教授：

团队创始人，2011年本科毕业于清华大学，计算机科学专业，2011年-2016年就读于耶鲁大学，获得计算机科学专业博士学位，现任哥伦比亚大学计算机科学系的助理教授。他是CertiKOS的主要设计者和开发者，CertiKOS是世界上第一个经过全面验证的并发操作系统内核。

Vilhelm Sjöberg：

白皮书中展示的第三位成员，2015年获得宾夕法尼亚大学计算机博士，主要研究兴趣是软件验证，编程语言，类型系统和逻辑。

这个创始团队得到了Google，Facebook和FreeWheel的高级软件工程师的支持。该团队目前正在扩展到最多20名软件工程师和研究科学家，以便提供积极的路线图。

发展路线图 roadmap：

CertiK在过去几年取得了实质性的进展，如下图显示的2015年至2017年间的发展取得了很大的成功：

那么CertiK的未来会怎么发展呢?

概念证明已于2017年12月开始，进展十分迅速。

alpha智能标签和分层验证产品已于2018年2月推出，CertiK团队建立的在线社区正在进行测试和改进。