Certik：智能合约的安全卫士 | ONE.TOP评级

声明：本测评内容仅供参考，任何依本测评内容作出的投资行为，与本测评内容无关。项目有风险，投资须谨慎。

Statement: the contents of this assessment are for reference only. Any investment behavior made according to the contents of this assessment is not related to the contents of this assessment. The project is risky and the investment must be prudent.

CertiK成立于硅谷和纽约市，是一个形式化验证框架，致力于构建安全的智能合约和区块链生态系统。

智能合约的出现使得区块链进入了2.0的发展阶段，然而智能合约漏洞所导致的很多安全问题却给人们带来巨大的财产损失。

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

无独有偶2017年7月19日, 多重签名钱包Parity1.5及以上版本出现安全漏洞，15万个ETH被盗,共价值3000万美元。

两次被盗事件都是因为智能合约中的漏洞，由此可见，加强智能合约审计是提高区块链安全的重要保证，其中形式化验证是解决智能合约审计的一个有效方法。形式化验证就是基于已建立的形式化规格，对所规格系统的相关特性进行分析和验证，以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误，但是可以最大限度地理解和分析系统，并尽可能地发现其中的不一致性、模糊性、不完备性等错误。形式化验证的主要技术包括模型验证和定理证明。certik正是从这个方面入手，打造一个形式化验证的框架，自动为代码加上标签，用形式化验证的方式去验证系统可能存在的漏洞。

目前涉及形式化验证的项目有quantstamp和链安科技，除此之外还有提供智能合约形式化验证的平台——runtime verification。形式化验证本身是一个比较冷门的技术，一般用于军工、航天等对系统安全非常高的领域，而且市面上做这个类型的项目很少，成熟的几乎没有，所以在这个细分市场里边certik有较强的技术壁垒和先入优势。

项目方对与团队的披露较少，核心成员只披露了三位，都是技术背景，未披露顾问团队、运营团队，项目方的运营实力不知如何。已有现象来看，目前热度一般，电报群上的维护还可以，鉴于该项目是币安实验室投资的项目之一，应该会对该项目的运营发展提供一定帮助。同时官方未披露token分配机制，只披露了一共有1亿枚token，整体市值估计，token分配和流通token都很不明朗。

暂未公布token机制情况。

Certik是一个是形式化验证框架，经过certik验证的智能合同、DApp以及区块链将会被附上证书形式的标志，来展示其正确性和安全性。Certik平台提供的主要功能包括以下部分。

智能标签框架

CertiK平台应用深度学习技术来构建智能标签框架，有了这个框架，大多数共享逻辑和属性代码（前置条件，后置条件，不变量等）都可以被自动标记，从而使得程序的逻辑，语义更加清晰和规范，这样验证的工作量就可以大大减少。

基于层的分解

这种技术揭示了分层设计模式的见解，并使得将复杂的证明任务分解为更小的任务成为可能，并在适当的抽象层面验证它们中的每一个。

可插拔的验证引擎

提供开放式的协议，更先进算法的证明引擎可以自由插入这个系统。

机器可检验的证明对象

构建机械式的证明对象（或者反例），这些证明对象可以快速的被任何人检验，同时作为验证程序的证书（机械式证明对象可直接作为证书，赏金猎人提供的证明对象，需要检察官进行人工检验后才能作为证书。注：赏金猎人和检察官后文会进行描述。）

认证的DAPP库

为集成开发环境提供了一系列认证库和插件，以便开发出质量更高的dapp，但是会花费一些CTK。

定制化的认证服务

如果有高可靠性要求，可以提供定制化的认证服务，由验证领域的专家提供帮助并出具综合报告。

Certik平台围绕bug的检测和修复建立了一个分布式的生态，该生态由五个角色构成，分别是客户、赏金猎人、检查官、社区贡献者以及开发使用者，该生态工运行模式如下图所示。

该系统可以分为机械化部分和人工部分。客户在certik平台上提交dapp或者程序系统，平台自动为其添加智能标签，并自动进行分解，形成小模块的证明任务，这个环节客户需要消耗一定量的CTK。

分解完小模块后，系统由两种方式进行验证，简单的证明任务可以由一些自动验证器(例如SMT解算器)解决。除了平台内部自带的验证器（证明引擎），CertiK平台提供开放协议，社区贡献者可以将带有更高级的求解算法的证明引擎自由地插入到该系统中，并获得一些CTK奖励。赏金猎人可以随机使用他们的引擎，并进行评估，优秀的引擎将被社区研究和推广。

另一种验证方式针对较为复杂的证明任务。赏金猎人接到该任务后，构建一个证明对象并进行广播，接着检查官对证明对象进行检测，当证明对象验证通过后，会被贴上证书的标签，赏金猎人和检查官分别获得CTK奖励。

所有分解的证明任务被验证后，CertiK平台的后端将返回详细而全面的评估报告。

开发使用者可以使用所有CertiK平台的认证库和IDE插件， 构建自己的DApp /系统，这需要花费一定的CTK。

官网未公布代码开源地址。

在安全检测这块，很多项目都是通过白帽黑客的方式，用激励的模式提供人工的检测修复，mofas和path是相关的两个例子。Certik的模式里边分为两部分，既有机器直接检测的部分，也有人工检测的部分。人工检测的部分里边，还进一步的将一个工作量较大的任务分解成无数个工作量较小的证明任务，再分发给链上的节点进行证明。相比于其他的安全项目，certik加入了智能标签框架，基于层的分解以及可插拔的证明引擎，这些功能的加入，使得智能合约的验证检测更加的高效便捷，从另一个方面说，由于市面上并没有相关的技术可以借鉴，开发的难度是相对较大的。

项目从2017年12月份开始，到2018年6月份，整个项目的安排是比较紧凑的，但核心理论的验证在2017年12月就进行了，说明项目之前是有筹备过一段时间的。从路线图上看，总共进行了三次募资，第一次是1月1日早期投资者，第二次是2月5日私募，第三次是6月30之后进行公募，但是官方电报群坚持没有相关信息披露。经过与项目方核实，项目各方面进度都在计划内，certik1.0即是官方验证服务，该服务已经为一些项目方提供验证。

经核实，项目按照路线图规划照常执行。

Ronghui Gu

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

Zhong Shao

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

vilhelm Sjöberg

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

项目未披露顾问团队。

据披露，certik已获得币安实验室、耶鲁大学、丹华资本、光速中国等机构的支持；同时CertiK将为Qtum量子链提供全栈式的形式化验证服务，包括提供Qtum系Dapps的安全性报告与一站式验证服务，为Qtum X86虚拟机的形式化建模 (formal model)，以及Qtum量子链的代码证明等，为Qtum生态系统的安全性保驾护航。除此之外，菩提、Ink、nebulas星云链也和CertiK建立了合作关系。

电报群有36000+的成员，群内发言活跃，管理员回复问题及时。Twitter关注者较少，只有1193人，更新频率中等，转发点赞量少。

Certik是难得的好项目，成员来自世界一流的大学，团队技术背景过硬，已有一批项目与certik达成合作，为智能合约的安全性进行验证，同时certik还获得了币安实验室和丹华资本的投资。如若certik的自动化形式验证能够解决绝大部分的智能合约漏洞，将会使区块链行业的智能合约安全显著提升，并大大提升合约验证的效率，取代部分人工验证。除了优势方面，Certik也存在着不足的地方，从目前来看，其运营能力一般，热度不高，只有电报群保持着较好的活跃度，市场炒作度低，且官方一直未披露与token有关的相关信息，包括token分配、募集情况、资金运用都没有公布，保密性较高。

综上，Certik总分6.77 分，评级等级A-级，综合能力强。