案例三·CertiK
由于智能合約一旦上傳，即公開且不可更改，因此“區塊鏈 2.0 ”時代的大多項目都產生了安全性驗證的需求。CertiK 看好這一服務機會，致力于應用形式化驗證技術，為智能合約和區塊鏈生態提供安全保護。
在傳統測試方法中，開發者會預想哪些情況下系統會遭攻擊，再針對這些情景測試。這套方法的缺陷在于，黑客往往是從程序員想象之外的路徑“下手”。而 CertiK 采用的形式化驗證 ( Formal Verification )，將智能合約轉化為數學模型，通過邏輯上的推理演算來驗證模型，從而證明智能合約的安全性。因為整個演算過程符合嚴謹縝密的數學邏輯，所以其檢驗的結果很難被黑客攻克。
CertiK 的核心產品是 CertiKOS 防黑客操作系統。此系統花費千萬美元的科研經費，兩位創始人邵中和顧榮輝用 6 年多的時間來研究安全系統。目前 CertiKOS 不僅在商業市場中通過驗證，也被應用到軍事防御系統上，并引起耶魯大學等美國學術界的關注。
由于軍方需求相對復雜，創始團隊于 2015 年中提出了分層結構理論，即將復雜的合約模塊化，先逐個驗證，再復合證明。
CertiK 的商業模式分兩步走：
1. 依靠 CertiK 自身算力的中心化驗證服務。如果客戶本身有強大的硬件設備和系統，可向 CertiK 提交智能合約和需求，CertiK 將合約轉化為數學模型，進行形式化驗證，并生成報告，指明合約中哪一行可能出現漏洞，系統在什么狀態或條件下可能被侵入。CertiK 根據合約的復雜程度收取不同的服務費。
2. 去中心化的安全驗證生態系統，借助社區參與者的算力，共同生成報告。前文提到的分層結構理論可將復雜任務拆分成小的模塊，CertiK 接到客戶需求后，將“任務”和技術工具分發給社區，獎勵提供算力、幫助檢驗小型模塊的貢獻者。交叉驗證機制可以確保社區內無人投機取巧、沒完成任務還“騙取獎勵”。CertiK 認為，這種任務分發要比算 hash 值挖礦更有意義、更低能耗。
CertiK 現已與 NEO 、量子鏈等機構達成戰略合作，同時對市面上的智能合約進行安全性驗證，發現安全漏洞后主動聯系團隊，說明問題，提供解決方案，獲取信任和口碑，逐步積累成功案例，再進行市場宣傳。
據介紹，CertiK 已獲耶魯大學，丹華資本，光速中國等機構種子輪融資（金額暫未透露）。
CertiK 的核心優勢在于團隊。位于硅谷的技術團隊從學術圈出身，去年開始商業化，工程師全部來自 Google、Facebook、Freewheel。聯合創始人邵中，普林斯頓大學博士、耶魯大學計算機系系主任/終身教授、中科大名譽院長、清華大學大師講習團成員，20 余年安全領域經驗。聯合創始人顧榮輝，清華大學本科、耶魯大學博士、哥倫比亞大學助理教授。
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
