讓黑客從良？一種無法被黑客攻破的技術？！
矽谷Live / 實地探訪/ 熱點探秘 / 深度探討
兩年前的一個夜晚，熟睡了的計算機教授 Gun 被一旁的電話鈴聲震醒。
「快起來，我們被黑客攻擊了！」
夜晚的寂靜和睡意的朦朧感被電話外的這句話瞬間打破，Gun 立馬掀開被子從床上跳起來，而下床的那一刻他已經知道要完了。
當所有人開始採取防禦措施的時候，這場黑客的攻擊已經結束。那晚，黑客們捲走了智能合約上價值千萬美元的以太幣。
這一次被盜事件不但成了許多人職業上的黑點，一個區塊鏈項目的終結，也讓信任他們的用戶蒙受了巨大的損失。
而兩年後的今天，數字資產被盜仍然是一個嚴重的問題。
區塊鏈的業內人士正集體盼望著一種可以解決智能合約和區塊鏈安全問題可行的技術方案的出現，包括聰哥我。
可以說只要安全問題沒得到很好的解決，區塊鏈領域的發展就會嚴重受到阻礙。
最近，小本聰的好友 Ken 向哥介紹了一個公司叫 CertiK。Ken 告訴聰哥，「CertiK 不但可以解決智能合約和區塊鏈領域的安全問題，所有程序上的安全問題都會得到解決，未來的黑客們都將從良。」
能讓黑客從良，這麼牛 ？聰哥決定讓 Ken 向大家介紹一下 CertiK：
CertiK 是什麼？
（certik.org）
用一句最簡單的話概括, CeriK 是一家用形式化驗證為智能合約和區塊鏈應用提供最先進安全性服務的公司。
而形式化驗證（Formal Verification）又是什麼？用 CertiK 聯合創始人顧榮輝的話來說就是：用邏輯語言來描述規範，通過嚴謹的數學推演來檢查給定的系統是否滿足要求。
那麼，為什麼形式化驗證可以解決現有區塊鏈所面臨的安全問題呢？
理解這問題前，我們需要先從四個點去了解智能合約在安全方面存在的問題：
第一，不可逆性：智能合約一旦發布在區塊鏈上，合約的源代碼是無法被修改的。
第二，代碼開源：在平時不公開源代碼的情況下都能被黑客攻擊，更何況大多數區塊鏈項目的代碼都是開源的。開源只會讓黑客的攻擊將變得更加容易。
第三，成本高：如果將智能合約放在區塊鏈上進行不斷的安全測試，資產的不斷轉換會是一筆很大的開銷。
第四，思維設限：即使開發者會預想智能合約在哪些情況下會遭攻擊，再針對這些情景測試，但黑客的厲害之處在於，可以從程序員預想之外的路徑下手。
正因為這四個方面讓區塊鏈上的數字資產很容易被黑客掠奪。
CertiK 能檢測到開源代碼的安全漏洞，從而告知開發人員，以至於在智能合約發布前就保證了安全性。依據數學原理的自動化推演，避免了人為檢測的思維局限，而自動化驗證也讓智能合約驗證的費用降到了最低。
其實形式化驗證早在 2016 年以太坊開發者大會（Devcon2）上就成為熱門話題，但一直存在著一定的爭議性。
（Devco2：How can Formal Vertication Help)
爭議性在於，用數學推演驗證軟體程序，在確保不同的網路元件接受指令並以用戶的身份模擬執行預定程序的過程中，需要人工輸入等技術限制，如何運用各種工具包來整合形式化驗證，還存在著諸多制約性的因素。
但 CertiK 的出現很好的整合了形式化驗證。只要你學過編程，就能很方便地用 CertiK 提供的教程說明來測試智能合約的安全問題。
我們來看一看產品：
你要做的，就是打開 CertiK 的系統，上傳你要檢測的智能合約，用 CertiK 提供的標記語言，標註好要進行測試的代碼部分，按下檢測按鈕。
檢測完畢後， CertiK 會給你提供這份智能合約的安全係數，並告訴你哪一塊程序存在著錯誤，並提供詳細的解決方案。
當你根據 CertiK 的解釋進行修改，修改完後再進行測試，直到達到 CertiK 100分的安全評級，你的智能合約就可以避免安全漏洞受到黑客攻擊。
是不是很簡單！簡直是智能合約開發者們的福音，黑客們的噩夢。
CertiK 的驗證過程體現了化整為零的解題思想，將一個難以證明的大問題拆分為許多容易證明的小問題，然後再將證明過的小問題重新組合回分解之前的較難的大問題，並且保證其中從端到端的正確性（end-to-end guarantees）。
在這個過程中，這些小問題都將發送給整個社區，社區的開發者們可以利用 CertiK 提供的方法，也可以運用自己的演算法來證明這些問題。一旦某個問題通過多方獨立的開發者的驗證，那麼其便可以用來作為建立其他理論的依據，從而形成互助協作的技術機制和良好的社區氛圍。
CertiK 是如何讓智能合約的安全檢測做到如此簡單的？
團隊
這就不得不提 CertiK 背後的團隊了：CertiK 的聯合創始人顧榮輝從清華大學本科畢業，耶魯大學的博士，現為哥倫比亞大學計算機系助理教授。
CertiK 的聯合創始人邵中，是普林斯頓大學的博士，耶魯大學計算機系的主任和 Thomas L. Kempner 冠名教授，中科大大師講席教授，有 20 余年的安全領域經驗。
無法被黑客攻破的操作系統
介紹完膜拜三分的團隊簡歷後，更牛的是邵中教授這位計算機程序語言設計的權威專家已經研發了經形式化驗證過的無漏洞、無法被黑客攻破的操作系統：CertiKOS。CertiK 正是 CertiKOS 研究的一個延伸，利用數學證明的形式化驗證方法開發完全可信經過驗證的智能合約與區塊鏈生態體系。
您已經看了全文的1/2了，休息一會：
這麼牛的 CertiK 是誰推薦給聰哥的？
聰哥好友 Ken：
「我是 All In 區塊鏈後再也不焦慮的 Ken，佛系炒幣患者，U Network 北美社區負責人，愛寫區塊鏈相關的文章，坐標矽谷，歡迎交流。」
看看區塊鏈安全市場有多大：
（以太坊創始人Vitalik)
Vitalik 在20歲創造的以太坊，打開了智能合約的潘多拉魔盒，成為黑客們致富的溫床。
如今基於以太坊的智能合約在全球已經超過了一百萬份，隨著區塊鏈入場的人越來越多，對智能合約的開發也水漲船高，智能合約的安全問題也逐漸被放大。
目前，一份智能合約的審核認證價格在市場上平均需要花費10萬美金，可以說在未來是一個萬億級別的市場。
而從 2017 年全球愛西歐融資的角度來看，隱私和安全領域的區塊鏈項目融資的佔比只有1%。如果排除隱私類型的區塊鏈項目，剩下專註在安全的項目佔比就更小了，但這不能代表安全領域的區塊鏈市場不被看好。
主要原因還在於區塊鏈安全問題在 2017 年還沒有受到市場足夠的重視，而區塊鏈安全領域項目的創業門檻較高，對大眾的認知門檻也比其它項目更高。同時區塊鏈安全領域項目 P2P 的社區模式也是一個很難的切入點。
看看其它項目：
Zeppelin 是一個社區驅動項目，它構建了安全智能合約的開源架構，目的在於實現安全智能合約的開發。目前有很多優質的海外區塊鏈項目都採用了 Zeppelin 的智能合約安全服務。
但 CertiK 與 Zeppelin 最大的不同在於，Zeppelin 主要依賴專業的人士參與對智能合約的審核，而且主要針對程序性質的驗證，並不支持 CertiK 程序功能正確性（Functional Correctness) 的驗證。
Quantstamp 是一家智能合約的安全審計平台，是被 YC 錄取的區塊鏈公司，聰哥也在之前的文章介紹過 ：錯過了區塊鏈第一波淘金熱？這家公司「賣鏟子」被YC相中
和 Zeppelin 類似，Quantstamp 也需要人工的參與，同樣不支持功能正確性的驗證。
區塊鏈公司 Axoni 不是一家專門做智能合約安全的公司。但他們最近也在專註與形式化驗證技術。開發了專門服務於形式化驗證的智能合約語言 Axlong。
與 CertiK 最大的不同點在於，CertiK 可以直接驗證 Solidty 等各種語言，但 Axlong 想取代 Solidty。雖都是形式化驗證技術，Axoni 實行的完全是一次曲線救國的形式化驗證方式。
再看看投資人怎麼說：
據了解，CertiK 已獲耶魯大學，丹華資本，光速中國等機構的支持。
作為 CertiK 的早期投資者，丹華資本董事總經理 Judy Yan 表示：「比特幣僅為一條區塊鏈，還有其他更多的公鏈和私鏈。目前有很多金融機構和相關團體都想打造自己的區塊鏈，但無論如何，他們都需要解決區塊鏈的安全性問題。」
斯坦福大學物理系的教授張首晟表示：「CertiK 是第一批提出利用數學證明的形式化驗證方法來檢查工程系統和智能合約安全性的團隊。這將是區塊鏈技術領域、甚至是科學領域的一大跨越式進步。」
耶魯大學合作研究辦公室（Yale OCR）的業務發展經理 Richard Anderson 稱：「目前的區塊鏈技術社區，極其容易受到黑客的攻擊，但是耶魯的這項技術將會改變世界。」
Ken還想說：
在形式化驗證領域，邵教授已經是公認的最權威的專家之一。
我們可以看到的是，CertiK 不但為每個參與虛擬經濟的個人提供了更強的安全保障，讓每一位會編程的人能夠參與到社區里來構建安全的網路環境，也讓黑客「失業」後，給其一片凈土（社區）去貢獻他們的力量來獲得合理的回報。
但如何讓 CertiK 這項技術實現高效的 P2P 化，形成整個社區的安全生態，這將是一個區別與技術問題以外的挑戰。
我相信 CertiK 的出現，將是區塊鏈安全領域目前最濃重的一筆，真正形成了一個 「 In Math We Trust 」（我們只相信數學）的區塊鏈生態。
看完這篇還不夠？如果你也關注區塊鏈領域，並且希望自己喜歡的區塊鏈項目被我們報道，歡迎留言告訴我們！
TAG:矽谷密探 |