Ce dépôt inclut le code du projet VeriSMo.
tools/ : comprend des outils et des scripts de vérification et de compilation.
deps/ : inclut le package hacl
source/ : code vériste
source/verismo : code vérifié pour vérismo
source/verismo_main : bac exécutable principal, qui définit uniquement un gestionnaire de panique Rust non vérifié.
source/verismo/src/arch : modèle
source/verismo/src/entry.s : un petit code assembleur non vérifié.
source/target.json : configuration cible
Tout d’abord, installez la chaîne d’outils Rust ;
tools/install.sh
Ensuite, construisez les outils et dépendances verus, verus-rustc (en remplacement de rustc) et igvm.
tools/activate.sh
Maintenant, exécutez les contrôles de vérification et construisez le binaire.
? Cette étape prend plusieurs minutes.
Courir
make verify
ou
cd source/verismo_main; cargo verify --release;
cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;
Un résultat entièrement vérifié devrait avoir « vérifié » : 2138, « erreurs » : 0,
Si aucune modification n'est apportée dans source/verismo , nous vous recommandons de construire sans vérification pour accélérer le processus de construction.
make debugbuild
ou
cd source/verismo_main; cargo build --feature noverify --release;
make ou make verify ) Télécharger le sous-module Linux : git submodule update --init richos/snplinux
Créez un système d'exploitation invité et des pilotes : make fs -f Makefile.default
Exécutez sh source/target/target/release/verismo/igvm.sh pour générer le verismo au format IGVM pour Hyper-V : source/target/target/release/verismo/verismo-rust.bin
Exécutez make fs pour générer un fichier vhdx en tant que système de fichiers pour la VM : richos/test-fs/verismo.vhdx
Matériel : Une machine AMD SEV-SNP.
Système d'exploitation : Windows avec un hyperviseur publié après 20230909. Les versions antérieures peuvent ne pas prendre en charge les interruptions restreintes dans les deux VMPL et ne fonctionneront donc pas.
Facultatif : une machine de débogage avec le système d'exploitation Windows.
Déplacez les fichiers suivants vers votre ordinateur 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
L'accès GUI n'est pas pris en charge et vous devez utiliser ssh pour vous connecter au système d'exploitation invité.
Le verismo.vhdx inclut un processus d'initialisation qui ouvrira le service sshd sans mot de passe.
Attendez une minute avant de vous connecter.
ssh [email protected]
Une fois l'invité démarré, il a déjà parlé à VeriSMo pour réveiller l'AP et mettre à jour les autorisations de la page lors de son démarrage.
À l'intérieur de l'invité, nous avons également fourni un pilote Verismo et quelques tests, pour parler directement à VeriSMo si vous le souhaitez.
verismo.ko : pilote
decode_report : affiche le rapport binaire dans un format lisible.
test.sh : un script de test
cd verismo insmod verismo.ko sh test.sh
Reportez-vous au débogage à distance Windows pour activer le débogage de l'hôte et de l'hyperviseur. Le journal de démarrage VeriSMo n'est pas accessible depuis le système d'exploitation invité.
Dans source/.cargo/config.toml, nous avons remplacé rustc par verus-rustc. verus-rustc appellera verus pour compiler vstd (une bibliothèque verus), verismo et verismo-main package, et appellera rustc pour compiler tous les autres packages (hacl, core, etc.).
Voir source/verismo/build.rs
noverify : construire la source sans vérification
verifymodule : si ${VERUS_MODULE} n'est pas vide, vérifiez uniquement le module spécifié.
Dépend de cfg(debug_assertations) Le mode débogage imprime des messages supplémentaires à des fins de débogage via leak_debug ; Le mode Release efface toutes les informations de fuite_debug ou de débogage ;
Ce projet accueille les contributions et suggestions. La plupart des contributions nécessitent que vous acceptiez un contrat de licence de contributeur (CLA) déclarant que vous avez le droit de nous accorder, et que vous nous accordez effectivement, le droit d'utiliser votre contribution. Pour plus de détails, visitez https://cla.opensource.microsoft.com.
Lorsque vous soumettez une pull request, un robot CLA déterminera automatiquement si vous devez fournir un CLA et décorera le PR de manière appropriée (par exemple, vérification du statut, commentaire). Suivez simplement les instructions fournies par le bot. Vous n’aurez besoin de le faire qu’une seule fois pour tous les dépôts utilisant notre CLA.
Ce projet a adopté le code de conduite Microsoft Open Source. Pour plus d’informations, consultez la FAQ sur le code de conduite ou contactez [email protected] pour toute question ou commentaire supplémentaire.
Ce projet peut contenir des marques ou des logos pour des projets, des produits ou des services. L'utilisation autorisée des marques ou logos Microsoft est soumise et doit respecter les directives relatives aux marques et aux marques de Microsoft. L'utilisation des marques ou logos Microsoft dans les versions modifiées de ce projet ne doit pas prêter à confusion ni impliquer le parrainage de Microsoft. Toute utilisation de marques ou de logos tiers est soumise aux politiques de ces tiers.
