獲得 IBM 和以太坊基金會科研獎金的編程語言 DeepSEA 究竟是什麼?

以太坊基金會(Ethereum Foundation)剛剛宣佈了第五批科研獎金名單,共有 7 個項目被授予資金支持,包括:
1) The Matter,一項應用了 zkSNARK 技術的 Plasma 擴容方案;
2) LeapDAO,Plasma 擴容方案「Leap」的新版設計;
3) Py-libp2p,ibp2p 的 Python 語言實現,可以應用於 Eth2.0 研究;
4) Ethereum on ARM ,在 ARM 設備等資源受限設備上運行以太坊客戶端的方案;
5) Goerli 測試網,一種跨各種客戶端的以太坊測試網;
6) Shadowlands,Python 語言開發的全文字界面以太坊 DApp 平臺;
7) DeepSEA,一共用於編寫已驗證智能合約的編程語言。

其中第七個項目「DeepSEA」值得關注。DeepSEA 由安全服務商 CertiK 研發團隊、耶魯大學和哥倫比亞大學科研團隊進行相關研究。在獲得以太坊基金會的科研獎金資助之前,這個項目還已經獲得了 IBM-哥倫比亞數據中心和量子鏈(Qtum)授予的科研經費。這次又獲得以太坊基金會的資金支持,體現出業內對區塊鏈安全體系建設的重視程度,以及推動跨行業應用場景實現的強烈願景。

鏈聞了解到,DeepSEA 項目由 CertiK 兩位聯合創始人耶魯大學計算機系主任邵中教授與哥倫比亞大學計算機系顧榮輝教授共同主導,是一種針對智能合約的函數式智能合約編程語言。

CertiK 團隊告訴鏈聞,他們開發 DeepSEA 這個智能合約編程語言,是希望讓開發者在智能合約中引入交互式形式化驗證技術,讓智能合約能夠被編譯成函數定義導入 Coq (一種輔助證明工具),並且被自動放入相應的 DeepSEA 規範層(Specification Layer)中,從而用數學方式完全證明。

換句話說,DeepSEA 的誕生,讓多種用於編寫智能合約的高級語言能夠被編譯到例如以太坊虛擬機(EVM)或超級賬本(Hyperledger)等機器語言中,並能夠保證編譯過程不會產生任何漏洞。這會對跨平臺智能合約的功能整合和安全驗證起到了舉足輕重的作用。

CertiK 聯合創始人、哥倫比亞大學計算機系顧榮輝教授曾經提到:雖然區塊鏈程序漏洞的檢測已經被業界高度重視,但智能合約安全事件仍舊頻繁發生,因此 CertiK 團隊產生了一個想法:「是否可以從源頭處解決區塊鏈的安全問題?是否可以通過設計新的智能合約語言在開發階段消滅安全漏洞?」

帶着這個想法,CertiK 團隊開始了 DeepSEA 項目的研發工作,他們通過 DeepSEA-Blockchain 框架構建跨平臺的、可信賴的智能合約框架,爲 Hyperledger、EVM 等平臺上的開發者提供一個值得信賴的開發環境。

據顧榮輝教授介紹,DeepSEA 是一種「無漏洞的編譯器」,該編譯器可以證明源代碼無漏洞,同時被編譯後的機器碼不會存在漏洞。同時,DeepSEA 源代碼中的程序規範可以被手動導入 Coq 證明輔助器中,開發者可以在 Coq 中對程序進行手動或者半自動證明。

獲得 IBM 和以太坊基金會科研獎金的編程語言 DeepSEA 究竟是什麼?DeepSEA 架構示意圖

DeepSEA 框架的獨特屬性表明該語言可以有效處理編程中的“固有衝突”,詳述如下:
“如今的主流操作系統和虛擬機管理程序仍然是用類似 C 的底層語言編寫的。我們發現,高級的形式化推理和底層系統編程之間似乎存在固有的衝突:前者依賴於高抽象級別的豐富理論,而後者必須操縱和管理低級別的影響和硬件資源。”

顧榮輝教授表示,DeepSEA 項目將幫助 CertiK 公司進一步探索形式化驗證技術在區塊鏈領域的應用,從而更好的保護用戶的數字資產安全。爲了讓 DeepSEA 項目在實際場景中更好地應用,研究人員的目標是設計和實現一個“工具鏈”。該工具鏈將會被應用於“構建經認證的操作系統內核”。CertiK 將有機會把 DeepSEA 工具鏈納入其現有的形式化驗證科技中,實現更完善的智能合約和區塊鏈生態安全驗證,從而更好地保護用戶的數字資產安全。

CertiK 是一個由計算機科學領域的自身教授創立的公司,團隊核心成員包括耶魯大學教授邵中、哥倫比亞大學教授顧榮輝,該項目通過形式化驗證技術,提供規模化智能合約驗證服務,來保證智能合約和區塊鏈系統的安全性。根據 CertiK 團隊披露,CertiK 在 2018 年間共保護了價值 12 億美金的數字資產免受損失,這一數字在新的一年中還在持續增長。