技術詳解：CertiK對螞蟻集團HyperEnclave先進形式化驗證

CertiK

特邀专栏作者

2023-07-31 03:35

本文約3938字，閱讀全文需要約6分鐘

CertiK宣布已完成了對螞蟻集團可信原生技術團隊開發的創新開放式跨平台可信執行環境（TEE）HyperEnclave的先進形式化驗證，本文將詳述驗證的技術部分。

AI總結

展開

上週，CertiK 宣布已完成了對螞蟻集團可信原生技術團隊開發的創新開放式跨平台可信執行環境（TEE）HyperEnclave 的先進形式化驗證。

為了實現保護Web 3 世界的使命，CertiK 在審計過程中採用了一系列分析方法。這包括但不限於由人工審計員進行詳細嚴謹的代碼評審，通過模糊測試和靜態分析發現程序錯誤、以及使用模型檢測為標準協議提供程序正確性的數學證明。其中最強大的方法之一是使用機器驗證的證明（即形式化驗證）。

形式化驗證既包括對標準屬性的自動驗證，例如使用模型檢測，同時也包括更為先進的驗證，即為特定項目制定定制化的安全屬性並對其進行證明。

如下圖所示，Web 3 應用程序依賴於其軟件棧上的所有組件層次。智能合約的業務邏輯使用高級編程語言編寫，編譯為字節碼，並由區塊鏈節點上的字節碼虛擬機進行運行。鏈的節點執行其特定的代碼來計算諸如質押等配置，以及共識算法。此外，區塊鏈節點運行在物理雲基礎設施上，其中包括操作系統、虛擬機監視器、可信執行環境等系統軟件。

在討論Web 3 的安全性時，人們通常關注的焦點是位於其軟件棧頂層的智能合約。而位於較低層級的軟件組件是由多個不同的Web 3 應用程序共享的，因此它們經過了更多的測試，可能存在的錯誤較少。

但與此同時，這也使得它們變得更為重要：在區塊鏈節點代碼中的一個錯誤可能會危及該區塊鏈上的所有應用程序，而係統基礎設施中的一個錯誤則可能會危及整個Web 3 世界。

CertiK 在機器驗證證明方面的工作涵蓋了Web 3 軟件棧的每一層面。例如：

我們使用符號化模型檢測自動驗證ERC-20 合約和其他實現標準接口的Solidity 合約
我們驗證了類似UniSwap 的DeFi 應用程序的智能合約，形式化驗證是我們對Move 和Cardano 合約審計的一部分，我們為一些Solidity 項目驗證了定制屬性
我們的DeepSEA 驗證編譯器旨在排除編譯過程中的錯誤
我們形式化驗證了Cosmos SDK 的標準銀行模塊
一級標題

一級標題

HyperEnclave 可信執行環境

可信執行環境（Trusted Execution Environment，TEE）的設計目的是保護應用程序免受一種最具挑戰性的攻擊類型：那些甚至能夠控制計算機操作系統的攻擊方式。

一些最著名的TEE 包括英特爾的SGX、Arm TrustZone 和AMD SEV。它們的工作原理是讓CPU 通過加密的方式證明特定的安全應用程序（enclave）已加載，並防止其他軟件幹擾它。

TEE 已經融入到數字生活的許多方面。像蘋果FileVault 這樣的磁盤加密軟件、谷歌Authenticator 這樣的兩步驗證應用程序都將密鑰存儲於TEE 中，即使有人盜竊並拆解筆記本電腦或手機，密鑰也能得到保護。

同時，在Web 3 中，TEE 也變得越來越重要。數字貨幣錢包也使用TEE 來更安全地存儲加密密鑰。分佈式區塊鏈預言機可以使用TEE 來增加數據的真實性可信度。有提議將TEE 用於“ 2-of-3 系統”以幫助從零知識證明的實現錯誤中的恢復。

還有一些區塊鏈項目，如LucidiTEE、SubstraTEE、Oasis Network 和AntChain，則提議使用TEE 為用戶提供數據隱私保護。

目前，大多數TEE 都是閉源的，並且與特定的硬件供應商綁定。例如，要使用Intel SGX，應用程序必須在Intel CPU 上運行，並經過Intel 的批准和白名單驗證。但是硬件開發本身較慢，因此TEE 的功能集較小，而且安全問題的解決需要對CPU 固件進行更新。相比之下，HyperEnclave 大部分是使用軟件實現的，利用了兩個廣泛可用的硬件功能。

首先，計算機的可信平台模塊（TPM，通常用於實現UEFI 安全引導）用於驗證HyperEnclave 和一組特定的安全飛地（enclave）是否正在運行。其次，HyperEnclave 使用CPU 的虛擬化擴展來保護enclave（通常由虛擬機監視器如VMware、VirtualBox、Hyper-V、KVM 等使用）。對於計算機硬件而言，HyperEnclave 看起來就像任何其他的虛擬機監視器，但對於enclave 來說，它提供了一個兼容SGX 的API，使得針對SGX 編寫的應用程序可以輕鬆適應在HyperEnclave 上運行。通過使用標準虛擬化技術，它可以輕鬆支持與操作系統緊密交互的高性能應用程序。

HyperEnclave 中最關鍵的部分是稱為RustMonitor 的監視器，用於保護enclave 免受來自其它enclave 和來自操作系統的危險。 enclave 和操作系統在虛擬化的"guest"模式下執行，這意味著它們每次嘗試訪問內存時，所訪問的內存地址首先通過由RustMonitor 所管理的頁表進行轉換。通過將enclave 放置在物理內存的不同區域中，RustMonitor 可以確保它們永遠無法讀取或覆蓋其他enclave 所擁有的數據。但這不能僅僅是簡單的靜態分離：一些內存地址必須被允許重疊，以便enclave 與操作系統進行通信，並且地址映射在處理頁面中斷時會被更新。

一級標題

對HyperEnclave 的RustMonitor 進行形式化驗證

RustMonitor 的頁表管理代碼是一個很好的驗證目標，因為它既小巧、其安全性又很關鍵。類似於Web 3 智能合約的情況，對其投入精力進行形式化驗證是可行的。在這個項目中，CertiK 從頁表必須遵守的不變性質入手，將它們從英語翻譯成Coq 形式化規範語言。然後，我們產生一份機器檢查的證明，以證明當RustMonitor 代碼修改表格時，所得到的表格仍滿足所有的不變性質。

不相干定理"不相干定理"）。所有這些證明放在一起，共同提供了一個強有力的保證，即頁表管理在設計上和實現上都是正確的。

然而，證明TEE 監控程序的正確性並不是一項簡單的任務。像虛擬化監視器和操作系統內核這樣的系統級程序大量使用低級代碼，其涉及帶有指針的數據結構、跳過類型抽象、以及為性能高度優化。直至今日，對此類程序的驗證仍然是值得發表在頂級計算機科學期刊上的論文中的熱門研究問題，對其每一行代碼進行證明需要巨大的努力。

例如，seL 4 的初始證明用了20 個人年，而Komodo 花費了2 個人年來驗證與約650 行C 代碼對應的彙編代碼。這些項目中的代碼是為了簡化驗證而重新專門編寫的，與HyperEnclave 很不同——後者已經投入生產並採用了Rust 的慣用寫法。基於現有技術水平，對所有代碼進行驗證在經濟上並不切實際。另一個問題是，與其他編程語言相比，Rust 的驗證工具鏈並不成熟。通過編寫手工的“模型”代碼而不是實際代碼，可以減輕驗證的負擔。一個例子是Sanctum TEE，一個驗證研究項目。這種方法的缺點是，代碼與抽像模型之間的不匹配可能會削弱任何關於模型的安全性或正確性屬性，甚至使其無效化。

CertiK 在解決這個問題上具備得天獨厚的條件。我們的兩位創始人，邵中教授和顧榮輝教授，是並發認證抽象層（CCAL）驗證方法的發明者，他們用這種方法驗證了世界上第一個並發認證操作系統內核CertiKOS，並驗證了KVM 虛擬化監視器seKVM 和ARM 機密計算架構。 CCAL 的基本思想是將程序中的所有函數劃分為很多“層”，為每層編寫其抽像模型，然後證明函數的實際代碼實現了抽像模型，這顯著降低了代碼與抽像模型行為不匹配的風險。同試圖將整個程序作為單個整體進行驗證相比，分層方法更容易處理代碼證明和並發問題。此前對seKVM 和Arm CCA 的工作在驗證工業級系統軟件項目方面受到了關注，而在這之前這類項目的規模對於形式化驗證來說過於龐大。

HyperEnclave 形式化驗證團隊包括之前參與CertiKOS 和seKVM 驗證的人員，我們試圖利用這些經驗在安全保證和驗證的資源投入之間取得良好的平衡。為此，我們使用了一種基於CCAL 規範的彈性驗證方法：我們的框架支持驗證函數代碼是否符合模型，但我們選擇僅對一部分函數進行這項驗證（49 個直接處理內存頁表的函數）。對於其他函數，我們則假定對Rust 代碼的手工Coq 翻譯是正確的，僅證明這些Coq 模型的功能正確性。這裡源碼中所訪問數據結構的抽象程度決定了每個函數是否需要驗證其代碼符合模型。當HyperEnclave 使用高級Rust 數據結構時，我們直接將其轉換到Coq，但當其使用基於字節的低級頁表格式時，我們則花更多精力來證明其等效於高級功能模型（詳見完整形式化驗證報告）。就RustMonitor 而言，這意味著我們對處理頁表表示的“Memory”模塊進行了代碼證明，對管理enclave 狀態的“Enclave”模塊使用了抽像模型，然後結合所有產生的模型證明了不變性定理和頂層安全定理。