Dieses Repo enthält den Code für das VeriSMo-Projekt.
tools/: Enthält Verifizierer- und Compiler-Tools und Skripte.
deps/: Enthält das Hacl-Paket
Quelle/: Verismo-Code
Quelle/Verismo: Verifizierter Code für Verismo
source/verismo_main: Haupt-Bin der ausführbaren Datei, der nur einen nicht verifizierten Rust-Panic-Handler definiert.
source/verismo/src/arch: Modell
source/verismo/src/entry.s: ein kleiner und nicht verifizierter Assemblercode.
source/target.json: Zielkonfiguration
Installieren Sie zunächst die Rust-Toolchain.
tools/install.sh
Erstellen Sie dann die Tools und Abhängigkeiten von Verus, Verus-Rustc (anstelle von Rustc) und Igvm.
tools/activate.sh
Führen Sie nun Überprüfungen durch und erstellen Sie die Binärdatei.
? Dieser Schritt dauert mehrere Minuten.
Laufen
make verify
oder
cd source/verismo_main; cargo verify --release;
cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;
Ein vollständig verifiziertes Ergebnis hätte „verified“: 2138, „errors“: 0,
Wenn keine Änderungen in source/verismo vorgenommen werden, empfehlen wir, ohne Überprüfung zu erstellen, um den Build-Prozess zu beschleunigen.
make debugbuild
oder
cd source/verismo_main; cargo build --feature noverify --release;
make oder make verify ausführen) Laden Sie das Linux-Submodul herunter: git submodule update --init richos/snplinux
Erstellen Sie Gastbetriebssystem und Treiber: make fs -f Makefile.default
Führen Sie sh source/target/target/release/verismo/igvm.sh aus, um den Verismo im IGVM-Format für Hyper-V zu generieren: source/target/target/release/verismo/verismo-rust.bin
Führen Sie make fs aus, um eine VHDX-Datei als Dateisystem für die VM zu generieren: richos/test-fs/verismo.vhdx
Hardware: Eine AMD SEV-SNP-Maschine.
Betriebssystem: Windows mit einem Hypervisor, der nach 20230909 veröffentlicht wurde. Frühere Versionen unterstützen möglicherweise keine eingeschränkten Interrupts in beiden VMPLs und funktionieren daher nicht.
Optional: Eine Debug-Maschine mit Windows-Betriebssystem.
Verschieben Sie die folgenden Dateien auf Ihren AMD SEV-SNP-Computer.
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
Der GUI-Zugriff wird nicht unterstützt und Sie müssen sich mit ssh beim Gastbetriebssystem anmelden.
Die verismo.vhdx enthält einen Init-Prozess, der den SSHD-Dienst ohne Passwort öffnet.
Warten Sie eine Minute, bevor Sie eine Verbindung herstellen.
ssh [email protected]
Sobald der Gast gestartet ist, hat er bereits mit VeriSMo kommuniziert, um den AP zu aktivieren und die Seitenberechtigungen während des Startvorgangs zu aktualisieren.
Im Gast haben wir auch einen Verismo-Treiber und einige Tests bereitgestellt, um bei Bedarf direkt mit VeriSMo zu kommunizieren.
verismo.ko: Treiber
decode_report: Zeigt den Binärbericht in einem lesbaren Format an.
test.sh: ein Testskript
cd verismo insmod verismo.ko sh test.sh
Informationen zum Aktivieren des Host- und Hypervisor-Debuggens finden Sie unter Windows Remote Debug. Auf das VeriSMo-Boot-Protokoll kann vom Gastbetriebssystem aus nicht zugegriffen werden.
In source/.cargo/config.toml haben wir rustc durch verus-rustc ersetzt. verus-rustc ruft verus auf, um vstd (eine Verus-Bibliothek), verismo und verismo-main -Paket zu kompilieren, und ruft rustc auf, um alle anderen Pakete (HACL, Core usw.) zu kompilieren.
Siehe source/verismo/build.rs
Noverify: Quellcode ohne Überprüfung erstellen
Verifizierungsmodule: Wenn ${VERUS_MODULE} nicht leer ist, überprüfen Sie nur das angegebene Modul.
Hängt von cfg(debug_assertations) ab. Der Debug-Modus gibt zusätzliche Meldungen zu Debug-Zwecken über Leak_debug aus. Der Release-Modus löscht alle Leak_debug- oder Debug-Informationen.
Dieses Projekt freut sich über Beiträge und Vorschläge. Für die meisten Beiträge müssen Sie einem Contributor License Agreement (CLA) zustimmen, in dem Sie erklären, dass Sie das Recht haben, uns die Rechte zur Nutzung Ihres Beitrags zu gewähren, und dies auch tatsächlich tun. Weitere Informationen finden Sie unter https://cla.opensource.microsoft.com.
Wenn Sie eine Pull-Anfrage einreichen, ermittelt ein CLA-Bot automatisch, ob Sie eine CLA bereitstellen müssen, und schmückt die PR entsprechend (z. B. Statusprüfung, Kommentar). Folgen Sie einfach den Anweisungen des Bots. Sie müssen dies nur einmal für alle Repos tun, die unsere CLA verwenden.
Dieses Projekt hat den Microsoft Open Source Verhaltenskodex übernommen. Weitere Informationen finden Sie in den FAQ zum Verhaltenskodex oder wenden Sie sich bei weiteren Fragen oder Kommentaren an [email protected].
Dieses Projekt kann Marken oder Logos für Projekte, Produkte oder Dienstleistungen enthalten. Die autorisierte Nutzung von Microsoft-Marken oder -Logos unterliegt den Marken- und Markenrichtlinien von Microsoft und muss diesen entsprechen. Die Verwendung von Microsoft-Marken oder -Logos in geänderten Versionen dieses Projekts darf keine Verwirrung stiften oder eine Sponsorschaft durch Microsoft implizieren. Jegliche Nutzung von Marken oder Logos Dritter unterliegt den Richtlinien dieser Drittanbieter.
