verismo 下載 - verismo 原始碼下載

現實主義

其他源碼

下載

VeriSMo：經過正式驗證的 AMD 機密虛擬機器安全模組。

此儲存庫包含 VeriSMo 專案的程式碼。

文件？

tools/ ：包含驗證器和編譯器工具和腳本。
deps/ : 包括 hacl 包
來源/：verismo程式碼
source/verismo : verismo 的驗證程式碼
source/verismo_main ：主要可執行 bin，僅定義未經驗證的 Rust 恐慌處理程序。
來源/verismo/src/arch ：模型
source/verismo/src/entry.s ：一個小的且未經驗證的組譯程式碼。
source/target.json ：目標配置

0. 前置要求

首先，安裝rust工具鏈；

tools/install.sh

1. 安裝工具 ?

然後，建立 verus、verus-rustc（取代 rustc）和 igvm 工具和依賴項。

tools/activate.sh

2. 驗證和構建

現在，執行驗證檢查並建置二進位檔案。

？此步驟需要幾分鐘。

一個。驗證整個專案：

跑步

make verify

或者

cd source/verismo_main; cargo verify --release;

b.驗證單一模組，這對開發很有用：

cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;

c.了解結果：

完全驗證的結果應該有「已驗證」：2138，「錯誤」：0，

d.無需驗證即可構建

如果未對source/verismo進行任何更改，我們建議在不進行驗證的情況下進行構建，以加快構建過程。

make debugbuild

或者

cd source/verismo_main; cargo build --feature noverify --release;

3. 建立虛擬機器鏡像（如果執行`make`或`make verify`則跳過）

下載linux子模組： git submodule update --init richos/snplinux
建立來賓作業系統和驅動程式： make fs -f Makefile.default
執行sh source/target/target/release/verismo/igvm.sh為 Hyper-V 產生 IGVM 格式的 verismo： source/target/target/release/verismo/verismo-rust.bin
執行make fs以產生 vhdx 檔案作為 VM 的檔案系統： richos/test-fs/verismo.vhdx

4. 部署並運行

要求

硬體：AMD SEV-SNP 機器。
作業系統：帶有 Hypervisor 的 Windows 在 20230909 之後發布。
可選：具有 Windows 作業系統的調試機器。

步驟

將以下文件移至您的 AMD SEV-SNP 計算機。

source/target/target/release/verismo/verismo-rust.bin
richos/test-fs/verismo.vhdx
tools/vm/*

1. 使用管理員權限從 powershell 建立 SNP VM。

build-vm.ps1 verismo verismo-rust.bin None verismo.vhdx

2.啟動虛擬機

start-vm verismo

3. 連接到訪客。

不支援 GUI 訪問，您需要使用 ssh 登入來賓作業系統。

verismo.vhdx 包含 init 進程，無需密碼即可開啟 sshd 服務。

連接前請等待一分鐘。

ssh [email protected]

4. 與VeriSMo模組對話

一旦 guest 虛擬機器啟動，它就已經與 VeriSMo 通訊以在啟動期間喚醒 AP 並更新頁面權限。

在 guest 中，我們還提供了 verismo 驅動程式和一些測試，如果您願意，可以直接與 Verismo 對話。

verismo.ko：驅動程式
解碼報告：以可讀格式顯示二進位報告。
test.sh：測試腳本

cd verismo
insmod verismo.ko
sh test.sh

5. 選用：您可以透過遠端偵錯器從 VeriSMo 存取啟動日誌。

請參閱 Windows 遠端偵錯以啟用主機和管理程式偵錯。無法從來賓作業系統存取 VeriSMo 啟動日誌。

建置過程如何進行？

將 rustc 替換為 verus-rustc

在 source/.cargo/config.toml 中，我們將 rustc 替換為 verus-rustc。 verus-rustc 將呼叫verus來編譯vstd （一個 verus 函式庫）、 verismo和verismo-main套件，並呼叫rustc來編譯所有其他套件（hacl、core 等）。