CertiK是一個是形式化驗證框架，為智能合約和區(qū)塊鏈應(yīng)用提供最先進(jìn)安全性服務(wù)的公司。經(jīng)過CerTIK驗證的智能合同、DApp以及區(qū)塊鏈將會被附上證書形式的標(biāo)志，來展示其正確性和安全性。

形式化驗證（Formal VerificaTIon）：用邏輯語言來描述規(guī)范，通過嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)推演來檢查給定的系統(tǒng)是否滿足要求。

市場需求：安全是區(qū)塊鏈?zhǔn)澜缧闹械耐?/p>

智能合約的出現(xiàn)使得區(qū)塊鏈進(jìn)入了2.0的發(fā)展階段，盡管智能合約的發(fā)展十分迅猛，然而智能合約漏洞所導(dǎo)致的很多安全問題卻給人們帶來巨大的財產(chǎn)損失。眾所周知，公鏈系統(tǒng)基于信任和開放，一旦部署就是不可更改的。因此任何錯誤都很容易遭受黑客的攻擊。

2016年黑客通過The Dao，利用智能合約中的漏洞，成功盜取360萬以太幣。The DAO事件發(fā)生后，以太坊創(chuàng)始人Vitalik Buterin提議修改以太坊代碼，對以太坊區(qū)塊鏈實施硬分叉，將黑客盜取資金的交易記錄回滾，在得到社區(qū)大部分礦工支持的同時也遭到了少數(shù)人的強(qiáng)烈反對，最終導(dǎo)致了以太坊社區(qū)的分裂。

軍用級別的CerTIK 系統(tǒng)如何運(yùn)行？

CerTIK區(qū)塊鏈解決方案是在已成功應(yīng)用的技術(shù)基礎(chǔ)上開發(fā)的。CertiKOS是邵中教授領(lǐng)導(dǎo)的小組成功研發(fā)的世界上第一個反黑客攻擊操作系統(tǒng)，這個系統(tǒng)共花費(fèi)千萬美元的科研經(jīng)費(fèi)，兩位創(chuàng)始人邵中教授和顧榮輝教授用6年多時間研究安全系統(tǒng)，目前CertiKOS不僅在商業(yè)市場中通過驗證，也被應(yīng)用到軍事防御系統(tǒng)上，并引起了耶魯大學(xué)等美國學(xué)術(shù)界的關(guān)注。

軍用級別的技術(shù)應(yīng)用在區(qū)塊鏈和智能合約安全性，是不是聽起來很高大上，很復(fù)雜？其實CertiK客戶端的使用非常簡單，用戶可以一鍵提交并可接收檢測結(jié)果。

完整的驗證過程運(yùn)作流程如下：

· 首先，客戶在客戶端向CertiK網(wǎng)絡(luò)提交智能合約或任何其他系統(tǒng)源代碼。

· CertiK將代碼的“正確性”轉(zhuǎn)換為類似的數(shù)學(xué)問題，然后以化整為零的解題思想，將一個難以證明的大問題拆分為許多容易證明的小問題，并將這些問題廣播到CertiK網(wǎng)絡(luò)。

· 分布式的CertiK節(jié)點并開始協(xié)作解決這些數(shù)學(xué)問題，以此換取獎勵。

· 節(jié)點把各自找到的解決方案反饋到CertiK區(qū)塊鏈上，并可以隨時被用于驗證。

· CertiK再將證明過的小問題重新組合回分解之前的較難的大問題，并將這些解決方案總結(jié)，并以證書的方式發(fā)送回客戶端。

· 這個證書將想客戶確認(rèn)，要么代碼是安全的（無漏洞并課抵抗黑客），要么會支持潛在的風(fēng)險和漏洞。

· 如果檢測出潛在的風(fēng)險或者漏洞，CertiK會同時提供一些案例介紹這些風(fēng)險或漏洞可能被攻擊的潛在方式。

全明星團(tuán)隊配置：

CertiK由來自哥倫比亞和耶魯?shù)娜餍强茖W(xué)家團(tuán)隊創(chuàng)建，并得到谷歌，F(xiàn)acebook和FreeWheel的高級軟件工程師的支持。

該團(tuán)隊成立于硅谷和紐約市，由世界級的正式驗證專家組成，他們是耶魯大學(xué)計算機(jī)科學(xué)系教授邵中及其弟子、哥倫比亞大學(xué)計算機(jī)系助理教授顧榮輝。

邵中教授：

團(tuán)隊聯(lián)合創(chuàng)始人，1988年本科畢業(yè)于中國科學(xué)技術(shù)大學(xué)，1989年至1994年就讀于美國普林斯頓大學(xué)，獲得計算機(jī)科學(xué)專業(yè)博士學(xué)位，1994年至今一直任教于耶魯大學(xué)，目前是計算機(jī)科學(xué)系的教授和系主任。他是SML / NJ編譯器的主要開發(fā)人員，也是FLINT認(rèn)證基礎(chǔ)架構(gòu)的主要架構(gòu)師。

顧榮輝教授：

團(tuán)隊創(chuàng)始人，2011年本科畢業(yè)于清華大學(xué)，計算機(jī)科學(xué)專業(yè)，2011年-2016年就讀于耶魯大學(xué)，獲得計算機(jī)科學(xué)專業(yè)博士學(xué)位，現(xiàn)任哥倫比亞大學(xué)計算機(jī)科學(xué)系的助理教授。他是CertiKOS的主要設(shè)計者和開發(fā)者，CertiKOS是世界上第一個經(jīng)過全面驗證的并發(fā)操作系統(tǒng)內(nèi)核。

Vilhelm Sj?berg：

白皮書中展示的第三位成員，2015年獲得賓夕法尼亞大學(xué)計算機(jī)博士，主要研究興趣是軟件驗證，編程語言，類型系統(tǒng)和邏輯。

這個創(chuàng)始團(tuán)隊得到了Google，F(xiàn)acebook和FreeWheel的高級軟件工程師的支持。該團(tuán)隊目前正在擴(kuò)展到最多20名軟件工程師和研究科學(xué)家，以便提供積極的路線圖。

發(fā)展路線圖 roadmap：

CertiK在過去幾年取得了實質(zhì)性的進(jìn)展，如下圖顯示的2015年至2017年間的發(fā)展取得了很大的成功：

那么CertiK的未來會怎么發(fā)展呢？

概念證明已于2017年12月開始，進(jìn)展十分迅速。

alpha智能標(biāo)簽和分層驗證產(chǎn)品已于2018年2月推出，CertiK團(tuán)隊建立的在線社區(qū)正在進(jìn)行測試和改進(jìn)。

2018年5月推出了測試版產(chǎn)品，并與數(shù)家商業(yè)合作伙伴建立合作。2018年6月首次發(fā)布CertiK1.0產(chǎn)品，并與30家商業(yè)合作伙伴進(jìn)行合作計劃于2018年下半年全面對外公開產(chǎn)品服務(wù)。

都有誰看好CertiK？

CertiK已獲得幣安實驗室、耶魯大學(xué)、丹華資本、光速中國等機(jī)構(gòu)的支持；

同時CertiK將為Qtum量子鏈提供全棧式的形式化驗證服務(wù)，包括提供Qtum系Dapps的安全性報告與一站式驗證服務(wù)，為Qtum X86虛擬機(jī)的形式化建模 （formal model），以及Qtum量子鏈的代碼證明等，為Qtum生態(tài)系統(tǒng)的安全性保駕護(hù)航。除此之外，菩提、Ink、nebulas星云鏈也和CertiK建立了合作關(guān)系。