最牛華人「程序員」邵中教授與哥大顧榮輝教授聯手解決安全問題痛點，打造區塊鏈理想世界

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

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

早在2016年以太坊開發者大會（Devcon2）上，形式化驗證就成為了社區的熱門話題。但用數學演算法驗證軟體程序，在確保不同的網路元件接受指令並以用戶的身份模擬執行預定程序的過程中，本身就有著需要人工輸入等技術限制，如何運用各種工具包來整合形式化驗證，存在著諸多制約。

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

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

面對這樣巨大的安全風險和不確定性，區塊鏈上的財富似乎可以被輕易攫取，也能被輕易掠奪。對此，顧榮輝教授表示，「區塊鏈建立於信任之上，但是它卻並不安全，它的代碼實現和所有的複雜系統一樣，都可能存在漏洞。甚至區塊鏈因為其去中心化的特性，在其上編寫代碼極易發生錯誤，卻很難更正代碼漏洞。」

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

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

據透露，CertiK目前的首要目標是實現比特幣、以太幣等數字貨幣交易的完全安全性；而在遠期的宏大目標上，CertiK願景為在世界範圍內實現透明、公平、安全的區塊鏈生態。作為耶魯大學的終身教授，邵中教授在過去二十多年來，致力於利用數學證明的方法開發形式化驗證過的軟體系統。

雷鋒網此前曾報道，這位計算機程序語言設計的權威專家已經研發了經形式化驗證過的無漏洞、無法被黑客攻破的操作系統：CertiKOS，而CertiK正是CertiKOS研究的一個延伸，利用數學證明的形式化驗證方法開發完全可信經過驗證的智能合約與區塊鏈生態體系。

顧榮輝教授：CertiK構建安全性編程社區打人類知識資料庫

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

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

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

展望未來，邵教授認為：「可編程化的區塊鏈擁有超越互聯網的潛力」，他為我們勾畫了這樣一個理想世界：在這個世界裡，包括保險、銀行、法律、會計等在內的越來越多重要的服務，都將會移植到不用擔心人為錯誤的網路世界，人們將在區塊鏈上完成各項商業活動。「

他特彆強調：

「在未來，或許虛擬世界將會扮演比現實世界更為重要的角色。「

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

來自學界同行的評測同樣對CertiK寄予了厚望。斯坦福大學物理系的JG Jackson and CJ Wood教授張首晟表示：「CertiK 是第一批提出利用數學證明的形式化眼妝方法來檢查工程系統和智能合約安全性的團隊。這將是區塊鏈技術領域、甚至是科學領域的一大跨越式進步。「

一直以來，耶魯大學合作研究辦公室（Yale Office of Cooperative Research,OCR）都與邵教授和顧教授有著緊密的合作，來尋求研究成果的商業化之路。OCR的高級業務發展經理Richard Anderson稱：「目前的區塊鏈技術社區，極其容易受到黑客的攻擊，但是耶魯的這項技術將會改變世界。」

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！