精选优质项目CertiK

【项目介绍】

CertiK是一个正式的验证框架，在数学上证明智能合同和区块链生态系统是无漏洞和抗黑客的。为了扩大验证的规模，CertiK开发了一种基于层的方法，将这样一个本来禁止的验证任务分解为更小的任务。这些较小的证明义务可以编码在CertiK事务中，然后由参与者以分散的方式进行验证和验证。因此，Certik分类账作为证书来展示经过验证的智能合同和经过验证的区块链生态系统的端到端正确性和安全性，使它们完全可信。

用一句最简单的话概括,CeriK是一家用形式化验证为智能合约和区块链应用提供最先进安全性服务的公司。

形式化验证（FormalVerification）又是什么？用CertiK联合创始人顾荣辉的话来说就是：用逻辑语言来描述规范，通过严谨的数学推演来检查给定的系统是否满足要求。

那么，为什么形式化验证可以解决现有区块链所面临的安全问题呢？

理解这问题前，我们需要先从四个点去了解智能合约在安全方面存在的问题：

第一，不可逆性：智能合约一旦发布在区块链上，合约的源代码是无法被修改的。

第二，代码开源：在平时不公开源代码的情况下都能被黑客攻击，更何况大多数区块链项目的代码都是开源的。开源只会让黑客的攻击将变得更加容易。

第三，成本高：如果将智能合约放在区块链上进行不断的安全测试，资产的不断转换会是一笔很大的开销。

第四，思维设限：即使开发者会预想智能合约在哪些情况下会遭攻击，再针对这些情景测试，但黑客的厉害之处在于，可以从程序员预想之外的路径下手。

正因为这四个方面让区块链上的数字资产很容易被黑客掠夺。

CertiK能检测到开源代码的安全漏洞，从而告知开发人员，以至于在智能合约发布前就保证了安全性。依据数学原理的自动化推演，避免了人为检测的思维局限，而自动化验证也让智能合约验证的费用降到了最低。

争议性在于，用数学推演验证软件程序，在确保不同的网络元件接受指令并以用户的身份模拟执行预定程序的过程中，需要人工输入等技术限制，如何运用各种工具包来整合形式化验证，还存在着诸多制约性的因素。但CertiK的出现很好的整合了形式化验证。只要你学过编程，就能很方便地用CertiK提供的教程说明来测试智能合约的安全问题。

我们来看一看产品：

你要做的，就是打开CertiK的系统，上传你要检测的智能合约，用CertiK提供的标记语言，标注好要进行测试的代码部分，按下检测按钮。

检测完毕后，CertiK会给你提供这份智能合约的安全系数，并告诉你哪一块程序存在着错误，并提供详细的解决方案。

当你根据CertiK的解释进行修改，修改完后再进行测试，直到达到CertiK100分的安全评级，你的智能合约就可以避免安全漏洞受到黑客攻击。

是不是很简单！简直是智能合约开发者们的福音，黑客们的噩梦。

CertiK的验证过程体现了化整为零的解题思想，将一个难以证明的大问题拆分为许多容易证明的小问题，然后再将证明过的小问题重新组合回分解之前的较难的大问题，并且保证其中从端到端的正确性（end-to-endguarantees）。

在这个过程中，这些小问题都将发送给整个社区，社区的开发者们可以利用CertiK提供的方法，也可以运用自己的算法来证明这些问题。一旦某个问题通过多方独立的开发者的验证，那么其便可以用来作为建立其他理论的依据，从而形成互助协作的技术机制和良好的社区氛围。

CertiK是如何让智能合约的安全检测做到如此简单的？就不得不说他们的团队了

【项目团队】

一支全明星球队，有着良好的成功记录。由哥伦比亚和耶鲁大学的全明星科学家组成的团队创建，并得到了谷歌、Facebook和Free轮公司的高级软件工程师的支持。

Prof.Ronghui Gu

联合创始人

RonghuiGu是哥伦比亚大学计算机科学系的终身助理教授。

他获得了博士学位。于2016年在耶鲁大学获得计算机科学硕士学位，

他的论文获得了耶鲁大学杰出论文奖，并被提名为ACM论文奖。

他于2011年获得清华大学学士学位。顾教授是系统软件正式验证方面的专家。

他是CertiKOS的首席设计师和开发人员，

CertiKOS是全球首个经过充分验证的并行操作系统内核。

他在CertiKOS上的OSDI16论文已被提名并入选CACM的研究亮点部分。

Prof.Zhong Shao

联合创始人

钟少是耶鲁大学计算机科学系ThomasL. Kempner教授和系主任。

他获得博士学位。于1994年在普林斯顿大学获得计算机科学学位。

在他早期的职业生涯中，他是SML/ NJ编译器的主要开发人员，

也是FLINT认证基础架构的主要架构师。近年来，邵先生一直是网络安全，

编程语言，操作系统和认证软件等高度可见研究领域的领军人物。

他和他在耶鲁大学的FLINT小组开发了世界上第一个耐黑客并发操作系统CertiKOS--

这是建立可以免于软件漏洞的网络物理系统的一个重要里程碑。

博士 VilhelmSjöberg

研究科学家

VilhelmSjöberg是耶鲁大学的副研究科学家。

他获得了博士学位。于2015年在宾夕法尼亚大学获得计算机科学硕士学位。

他是软件验证，编程语言和类型系统方面的专家。

他的论文研究集中在使依赖型系统对通用编程语言更具吸引力，

因为通过证明函数终止以及通过合并闭包来引入自动定理证明是可选的。

目前他对CertiKOS等分层认证系统的语言支持感兴趣。

Sjöberg博士是2016ACM SIGPLAN John C. Reynolds博士论文奖的获得者。