CertiK區(qū)塊鏈解決方案正在解決區(qū)塊鏈?zhǔn)澜缧闹械陌踩?/h1>
CertiK是一個(gè)是形式化驗(yàn)證框架，為智能合約和區(qū)塊鏈應(yīng)用提供最先進(jìn)安全性服務(wù)的公司。經(jīng)過CerTIK驗(yàn)證的智能合同、DApp以及區(qū)塊鏈將會(huì)被附上證書形式的標(biāo)志，來展示其正確性和安全性。
形式化驗(yàn)證（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)致的很多安全問題卻給人們帶來巨大的財(cái)產(chǎn)損失。眾所周知，公鏈系統(tǒng)基于信任和開放，一旦部署就是不可更改的。因此任何錯(cuò)誤都很容易遭受黑客的攻擊。
2016年黑客通過The Dao，利用智能合約中的漏洞，成功盜取360萬以太幣。The DAO事件發(fā)生后，以太坊創(chuàng)始人Vitalik Buterin提議修改以太坊代碼，對以太坊區(qū)塊鏈實(shí)施硬分叉，將黑客盜取資金的交易記錄回滾，在得到社區(qū)大部分礦工支持的同時(shí)也遭到了少數(shù)人的強(qiáng)烈反對，最終導(dǎo)致了以太坊社區(qū)的分裂。
軍用級別的CerTIK 系統(tǒng)如何運(yùn)行？
CerTIK區(qū)塊鏈解決方案是在已成功應(yīng)用的技術(shù)基礎(chǔ)上開發(fā)的。CertiKOS是邵中教授領(lǐng)導(dǎo)的小組成功研發(fā)的世界上第一個(gè)反黑客攻擊操作系統(tǒng)，這個(gè)系統(tǒng)共花費(fèi)千萬美元的科研經(jīng)費(fèi)，兩位創(chuàng)始人邵中教授和顧榮輝教授用6年多時(shí)間研究安全系統(tǒng)，目前CertiKOS不僅在商業(yè)市場中通過驗(yàn)證，也被應(yīng)用到軍事防御系統(tǒng)上，并引起了耶魯大學(xué)等美國學(xué)術(shù)界的關(guān)注。
軍用級別的技術(shù)應(yīng)用在區(qū)塊鏈和智能合約安全性，是不是聽起來很高大上，很復(fù)雜？其實(shí)CertiK客戶端的使用非常簡單，用戶可以一鍵提交并可接收檢測結(jié)果。
完整的驗(yàn)證過程運(yùn)作流程如下：
· 首先，客戶在客戶端向CertiK網(wǎng)絡(luò)提交智能合約或任何其他系統(tǒng)源代碼。
· CertiK將代碼的“正確性”轉(zhuǎn)換為類似的數(shù)學(xué)問題，然后以化整為零的解題思想，將一個(gè)難以證明的大問題拆分為許多容易證明的小問題，并將這些問題廣播到CertiK網(wǎng)絡(luò)。
· 分布式的CertiK節(jié)點(diǎn)并開始協(xié)作解決這些數(shù)學(xué)問題，以此換取獎(jiǎng)勵(lì)。
· 節(jié)點(diǎn)把各自找到的解決方案反饋到CertiK區(qū)塊鏈上，并可以隨時(shí)被用于驗(yàn)證。
· CertiK再將證明過的小問題重新組合回分解之前的較難的大問題，并將這些解決方案總結(jié)，并以證書的方式發(fā)送回客戶端。
· 這個(gè)證書將想客戶確認(rèn)，要么代碼是安全的（無漏洞并課抵抗黑客），要么會(huì)支持潛在的風(fēng)險(xiǎn)和漏洞。
· 如果檢測出潛在的風(fēng)險(xiǎn)或者漏洞，CertiK會(huì)同時(shí)提供一些案例介紹這些風(fēng)險(xiǎn)或漏洞可能被攻擊的潛在方式。
全明星團(tuán)隊(duì)配置：
CertiK由來自哥倫比亞和耶魯?shù)娜餍强茖W(xué)家團(tuán)隊(duì)創(chuàng)建，并得到谷歌，F(xiàn)acebook和FreeWheel的高級軟件工程師的支持。
該團(tuán)隊(duì)成立于硅谷和紐約市，由世界級的正式驗(yàn)證專家組成，他們是耶魯大學(xué)計(jì)算機(jī)科學(xué)系教授邵中及其弟子、哥倫比亞大學(xué)計(jì)算機(jī)系助理教授顧榮輝。
邵中教授：
團(tuán)隊(duì)聯(lián)合創(chuàng)始人，1988年本科畢業(yè)于中國科學(xué)技術(shù)大學(xué)，1989年至1994年就讀于美國普林斯頓大學(xué)，獲得計(jì)算機(jī)科學(xué)專業(yè)博士學(xué)位，1994年至今一直任教于耶魯大學(xué)，目前是計(jì)算機(jī)科學(xué)系的教授和系主任。他是SML / NJ編譯器的主要開發(fā)人員，也是FLINT認(rèn)證基礎(chǔ)架構(gòu)的主要架構(gòu)師。
顧榮輝教授：
團(tuán)隊(duì)創(chuàng)始人，2011年本科畢業(yè)于清華大學(xué)，計(jì)算機(jī)科學(xué)專業(yè)，2011年-2016年就讀于耶魯大學(xué)，獲得計(jì)算機(jī)科學(xué)專業(yè)博士學(xué)位，現(xiàn)任哥倫比亞大學(xué)計(jì)算機(jī)科學(xué)系的助理教授。他是CertiKOS的主要設(shè)計(jì)者和開發(fā)者，CertiKOS是世界上第一個(gè)經(jīng)過全面驗(yàn)證的并發(fā)操作系統(tǒng)內(nèi)核。
Vilhelm Sj?berg：
白皮書中展示的第三位成員，2015年獲得賓夕法尼亞大學(xué)計(jì)算機(jī)博士，主要研究興趣是軟件驗(yàn)證，編程語言，類型系統(tǒng)和邏輯。
這個(gè)創(chuàng)始團(tuán)隊(duì)得到了Google，F(xiàn)acebook和FreeWheel的高級軟件工程師的支持。該團(tuán)隊(duì)目前正在擴(kuò)展到最多20名軟件工程師和研究科學(xué)家，以便提供積極的路線圖。
發(fā)展路線圖 roadmap：
CertiK在過去幾年取得了實(shí)質(zhì)性的進(jìn)展，如下圖顯示的2015年至2017年間的發(fā)展取得了很大的成功：
那么CertiK的未來會(huì)怎么發(fā)展呢？
概念證明已于2017年12月開始，進(jìn)展十分迅速。
alpha智能標(biāo)簽和分層驗(yàn)證產(chǎn)品已于2018年2月推出，CertiK團(tuán)隊(duì)建立的在線社區(qū)正在進(jìn)行測試和改進(jìn)。
2018年5月推出了測試版產(chǎn)品，并與數(shù)家商業(yè)合作伙伴建立合作。2018年6月首次發(fā)布CertiK1.0產(chǎn)品，并與30家商業(yè)合作伙伴進(jìn)行合作計(jì)劃于2018年下半年全面對外公開產(chǎn)品服務(wù)。
都有誰看好CertiK？
CertiK已獲得幣安實(shí)驗(yàn)室、耶魯大學(xué)、丹華資本、光速中國等機(jī)構(gòu)的支持；
同時(shí)CertiK將為Qtum量子鏈提供全棧式的形式化驗(yàn)證服務(wù)，包括提供Qtum系Dapps的安全性報(bào)告與一站式驗(yàn)證服務(wù)，為Qtum X86虛擬機(jī)的形式化建模 （formal model），以及Qtum量子鏈的代碼證明等，為Qtum生態(tài)系統(tǒng)的安全性保駕護(hù)航。除此之外，菩提、Ink、nebulas星云鏈也和CertiK建立了合作關(guān)系。
下載文檔
