自2014年比特幣交易所運營商MT.Gox遭黑客攻擊破產(chǎn)倒閉以來，至2018年1月日本另一家數(shù)字資產(chǎn)交易所CoinCheck價值約5.3億美元資產(chǎn)失竊；從2016年The DAO因代碼漏洞致五千萬美元以太幣失竊，到2017年11月Parity過億美元以太幣被凍結(jié)，在迅猛的發(fā)展勢頭下，日益壯大的數(shù)字資產(chǎn)市場一直擺脫不了安全事故頻發(fā)的陰影，安全問題成為了區(qū)塊鏈這一新興技術(shù)尋求突破、實現(xiàn)大規(guī)模落地最為主要的阻礙之一，業(yè)內(nèi)正集體呼喚著，解決這一痛點的可靠技術(shù)方案出現(xiàn)。

在上世紀九十年代概念被首次提出后，由于缺乏可信執(zhí)行環(huán)境，智能合約這一概念一直被看作是空中樓閣的設(shè)想。直到支持圖靈完備的腳本語言的以太坊的誕生，支持可編程合約的數(shù)字系統(tǒng)和區(qū)塊鏈技術(shù)的發(fā)明讓尼克·薩博的這一技術(shù)設(shè)想真正落地。但由于智能合約代碼編寫難度極高，編譯器缺少代碼庫和漏洞導(dǎo)致的系統(tǒng)崩潰等技術(shù)問題隨著區(qū)塊鏈發(fā)展歷程的推進被不斷放大，對于提升智能合約安全性的各種方案的探討也逐漸成為了業(yè)內(nèi)探討的技術(shù)熱點。

早在2016年以太坊開發(fā)者大會（Devcon2）上，形式化驗證就成為了社區(qū)的熱門話題。但用數(shù)學(xué)算法驗證軟件程序，在確保不同的網(wǎng)絡(luò)元件接受指令并以用戶的身份模擬執(zhí)行預(yù)定程序的過程中，本身就有著需要人工輸入等技術(shù)限制，如何運用各種工具包來整合形式化驗證，存在著諸多制約。

由耶魯大學(xué)計算機科學(xué)系教授邵中（詳見雷鋒網(wǎng)此前報道：《最牛華人“程序員”邵中，全世界程序員的命運都可能因他而變》）及其弟子、哥倫比亞大學(xué)計算機系助理教授顧榮輝帶領(lǐng)的形式化驗證智能合約項目CertiK，在耶魯大學(xué)數(shù)十年的研究成果的基礎(chǔ)上，致力于為現(xiàn)有所有的區(qū)塊鏈應(yīng)用提供最先進的安全性服務(wù)（官網(wǎng)：certik.org）。

在以往，基于區(qū)塊鏈去中心化的思想和技術(shù)特性，智能合約一旦提交至鏈上，合約的源代碼無法再被更改。正因為這一點，當黑客發(fā)現(xiàn)并利用其存在的漏洞來竊取資金時，唯一制止這種不法行為的方法只有硬分叉（hard forking）：將鏈強行分叉，并且使之前所有的交易信息作廢，還需所有社區(qū)里的用戶升級其本地的區(qū)塊鏈。以太坊（ETH）和以太坊經(jīng)典（ETC）即為一個最具說服力的前車之鑒，其通過硬分叉追討回失竊資金后使得社區(qū)內(nèi)部分裂，遭致違背去中心化的技術(shù)信仰的聲討，爆發(fā)的爭執(zhí)蔓延至今，仍影響著社區(qū)的穩(wěn)定和發(fā)展。

面對這樣巨大的安全風(fēng)險和不確定性，區(qū)塊鏈上的財富似乎可以被輕易攫取，也能被輕易掠奪。對此，顧榮輝教授表示，“區(qū)塊鏈建立于信任之上，但是它卻并不安全，它的代碼實現(xiàn)和所有的復(fù)雜系統(tǒng)一樣，都可能存在漏洞。甚至區(qū)塊鏈因為其去中心化的特性，在其上編寫代碼極易發(fā)生錯誤，卻很難更正代碼漏洞?！?/p>

從這一現(xiàn)實痛點出發(fā)，邵教授認為區(qū)塊鏈安全性問題亟需得到解決，在他看來，一旦所有的區(qū)塊鏈的代碼在上鏈前全部被形式化的數(shù)學(xué)證明驗證后，開發(fā)者和用戶們就無須再為區(qū)塊鏈上的系統(tǒng)遭受黑客攻擊而擔(dān)心，區(qū)塊鏈的安全性問題能夠真正得到解決。

2018年3月7日，耶魯大學(xué)在其官網(wǎng)上發(fā)表新聞稱，Certik項目的順利實施，對區(qū)塊鏈的安全問題提供了可靠的保障，使其在邁向落地應(yīng)用的過程中大大提高了可行性。文章提到，CertiK提供的首創(chuàng)性的安全服務(wù)，能夠幫助區(qū)塊鏈上的每筆交易避免程序錯誤（bug-free），并且無法被黑客所攻破（hack-resistent）從而造成用戶的資金損失，而這將會改變整個區(qū)塊鏈行業(yè)的規(guī)則和未來走向。

據(jù)透露，CertiK目前的首要目標是實現(xiàn)比特幣、以太幣等數(shù)字貨幣交易的完全安全性；而在遠期的宏大目標上，CertiK愿景為在世界范圍內(nèi)實現(xiàn)透明、公平、安全的區(qū)塊鏈生態(tài)。作為耶魯大學(xué)的終身教授，邵中教授在過去二十多年來，致力于利用數(shù)學(xué)證明的方法開發(fā)形式化驗證過的軟件系統(tǒng)。

雷鋒網(wǎng)此前曾報道，這位計算機程序語言設(shè)計的權(quán)威專家已經(jīng)研發(fā)了經(jīng)形式化驗證過的無漏洞、無法被黑客攻破的操作系統(tǒng)：CertiKOS，而CertiK正是CertiKOS研究的一個延伸，利用數(shù)學(xué)證明的形式化驗證方法開發(fā)完全可信經(jīng)過驗證的智能合約與區(qū)塊鏈生態(tài)體系。

顧榮輝教授：CertiK構(gòu)建安全性編程社區(qū)打人類知識數(shù)據(jù)庫

而CertiK在大大提高各種豐富多樣的區(qū)塊鏈應(yīng)用的可行性、改善區(qū)塊鏈應(yīng)用生態(tài)的同時，目光也放得更為長遠，不僅僅將自己定位為一個提升區(qū)塊鏈交易安全性的科技初創(chuàng)公司，更是一個致力于建設(shè)安全性編程社區(qū)的基金會，如顧教授所言，這其實是在建立一個經(jīng)過形式化驗證的人類知識數(shù)據(jù)庫。

具體來看，是如何一步步構(gòu)建這個如此宏大的數(shù)據(jù)庫？顧教授透露，基金會將首先會為社區(qū)的開發(fā)者們提供大量的形式化驗證的教程。他表示，CertiK的驗證過程體現(xiàn)了化整為零的解題思想，將一個難以證明的大問題拆分為許多容易證明的小問題，然后再將證明過的小問題重新組合回分解之前的較難的大問題，并且保證其中從端到端的正確性（end-to-end guarantees）。

在這個過程中，前述所有的這些小問題都將發(fā)送給整個社區(qū)，社區(qū)的開發(fā)者們可以利用CertiK提供的方法，也可以運用自己的算法來證明這些問題。一旦某個問題通過多方獨立的開發(fā)者的驗證，那么其便可以用來作為建立其他理論的依據(jù)，從而形成互助協(xié)作的技術(shù)機制和良好的社區(qū)氛圍。

可編程化區(qū)塊鏈塑造理想世界:商業(yè)業(yè)務(wù)遷移上鏈杜絕人為錯誤

展望未來，邵教授認為：“可編程化的區(qū)塊鏈擁有超越互聯(lián)網(wǎng)的潛力”，他為我們勾畫了這樣一個理想世界：在這個世界里，包括保險、銀行、法律、會計等在內(nèi)的越來越多重要的服務(wù)，都將會移植到不用擔(dān)心人為錯誤的網(wǎng)絡(luò)世界，人們將在區(qū)塊鏈上完成各項商業(yè)活動?！?/p>

他特別強調(diào)：

“在未來，或許虛擬世界將會扮演比現(xiàn)實世界更為重要的角色。“

而在丹華資本董事總經(jīng)理Judy Yan看來，一旦安全性問題被解決，將沒有任何東西能夠阻礙區(qū)塊鏈的擴張。作為CertiK的早期投資者，其表示：“比特幣僅為一條區(qū)塊鏈，還有其他更多的公鏈和私鏈。目前有很多金融機構(gòu)和相關(guān)團體都想打造自己的區(qū)塊鏈，但無論如何，他們都需要解決區(qū)塊鏈的安全性問題?！?/p>

來自學(xué)界同行的評測同樣對CertiK寄予了厚望。斯坦福大學(xué)物理系的JG Jackson and CJ Wood教授張首晟表示：“CertiK 是第一批提出利用數(shù)學(xué)證明的形式化驗證方法來檢查工程系統(tǒng)和智能合約安全性的團隊。這將是區(qū)塊鏈技術(shù)領(lǐng)域、甚至是科學(xué)領(lǐng)域的一大跨越式進步?！?/p>

一直以來，耶魯大學(xué)合作研究辦公室（Yale Office of Cooperative Research,OCR）都與邵教授和顧教授有著緊密的合作，來尋求研究成果的商業(yè)化之路。OCR的高級業(yè)務(wù)發(fā)展經(jīng)理Richard Anderson稱：“目前的區(qū)塊鏈技術(shù)社區(qū)，極其容易受到黑客的攻擊，但是耶魯?shù)倪@項技術(shù)將會改變世界。”

雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。