このリポジトリには、VeriSMo プロジェクトのコードが含まれています。
tools/ : ベリファイアーおよびコンパイラーのツールとスクリプトが含まれます。
deps/ : hacl パッケージが含まれます
ソース/ : ベリズモコード
source/verismo : verismo の検証済みコード
source/verismo_main : メインの実行可能ファイル。未検証の Rust パニック ハンドラーのみを定義します。
ソース/verismo/src/arch : モデル
source/verismo/src/entry.s : 小規模で未検証のアセンブリ コード。
source/target.json : ターゲット設定
まず、Rust ツールチェーンをインストールします。
tools/install.sh
次に、verus、verus-rustc (rustc を置き換える)、igvm ツールと依存関係を構築します。
tools/activate.sh
次に、検証チェックを実行してバイナリをビルドします。
?このステップには数分かかります。
走る
make verify
または
cd source/verismo_main; cargo verify --release;
cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;
完全に検証された結果は、「verified」: 2138、「errors」: 0 になるはずです。
source/verismoに変更が加えられていない場合は、ビルド プロセスを高速化するために検証なしでビルドすることをお勧めします。
make debugbuild
または
cd source/verismo_main; cargo build --feature noverify --release;
makeまたはmake verify実行する場合はスキップします) Linux サブモジュールをダウンロードします: git submodule update --init richos/snplinux
ゲスト OS とドライバーをビルドします: 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を実行して、VM のファイルシステムとして vhdx ファイルを生成します: richos/test-fs/verismo.vhdx
ハードウェア: AMD SEV-SNP マシン。
OS: 20230909 以降にリリースされたハイパーバイザーを搭載した Windows。それより前のリリースでは、両方の VMPL で制限付き割り込みがサポートされていない可能性があるため、機能しません。
オプション: Windows OS を搭載したデバッグ マシン。
次のファイルを AMD SEV-SNP マシンに移動します。
source/target/target/release/verismo/verismo-rust.bin
richos/test-fs/verismo.vhdx
tools/vm/*
build-vm.ps1 verismo verismo-rust.bin None verismo.vhdx
start-vm verismo
GUI アクセスはサポートされていないため、ゲスト OS にログインするには ssh を使用する必要があります。
verismo.vhdx には、パスワードなしで sshd サービスを開く init プロセスが含まれています。
接続する前に 1 分間待ちます。
ssh [email protected]
ゲストが起動すると、すでに VeriSMo と通信して AP をウェイクアップし、起動中にページのアクセス許可を更新します。
ゲスト内には、必要に応じて Verismo と直接通信できるように、verismo ドライバーといくつかのテストも提供されました。
verismo.ko: ドライバー
decode_report: バイナリ レポートを読み取り可能な形式で表示します。
test.sh: テストスクリプト
cd verismo insmod verismo.ko sh test.sh
ホストとハイパーバイザーの両方のデバッグを有効にするには、Windows リモート デバッグを参照してください。 VeriSMo ブート ログにはゲスト OS からアクセスできません。
source/.cargo/config.toml で、rustc を verus-rustc に置き換えました。 verus-rustc は、 verus呼び出してvstd (verus ライブラリ)、 verismoおよびverismo-mainパッケージをコンパイルし、 rustc呼び出して他のすべてのパッケージ (hacl、core など) をコンパイルします。
source/verismo/build.rs参照してください。
noverify: 検証なしでソースをビルドする
verifymodule: ${VERUS_MODULE} が空でない場合は、指定されたモジュールのみを検証します。
cfg(debug_assertations) に依存します。 デバッグ モードは、leak_debug を介してデバッグ目的の追加メッセージを出力します。リリース モードでは、leak_debug またはデバッグ情報がすべて消去されます。
このプロジェクトは貢献と提案を歓迎します。 ほとんどの投稿では、投稿を使用する権利をお客様が有しており、実際に当社に付与することを宣言する投稿者ライセンス契約 (CLA) に同意する必要があります。詳細については、https://cla.opensource.microsoft.com をご覧ください。
プル リクエストを送信すると、CLA ボットが CLA を提供する必要があるかどうかを自動的に判断し、PR を適切に装飾します (ステータス チェック、コメントなど)。ボットが提供する指示に従ってください。 CLA を使用するすべてのリポジトリでこれを 1 回行うだけで済みます。
このプロジェクトはマイクロソフトのオープンソース行動規範を採用しています。詳細については、「行動規範に関するよくある質問」を参照するか、追加の質問やコメントがあれば [email protected] までお問い合わせください。
このプロジェクトには、プロジェクト、製品、またはサービスの商標またはロゴが含まれている場合があります。 Microsoft の商標またはロゴの許可された使用には、Microsoft の商標およびブランド ガイドラインが適用され、それに従わなければなりません。このプロジェクトの修正バージョンで Microsoft の商標またはロゴを使用することは、混乱を引き起こしたり、Microsoft のスポンサーであることを暗示したりしてはなりません。第三者の商標またはロゴの使用には、それらの第三者のポリシーが適用されます。
