Este repositorio incluye el código del proyecto VeriSMo.
herramientas/: incluye scripts y herramientas de verificación y compilación.
deps/ : incluye paquete hacl
fuente/: código verismo
fuente/verismo: código verificado para verismo
source/verismo_main: bin ejecutable principal, que solo define un controlador de pánico de Rust no verificado.
fuente/verismo/src/arch: modelo
source/verismo/src/entry.s: un código ensamblador pequeño y no verificado.
source/target.json: configuración de destino
Primero, instale la cadena de herramientas oxidada;
tools/install.sh
Luego, cree herramientas y dependencias verus, verus-rustc (que reemplaza a rustc) e igvm.
tools/activate.sh
Ahora, ejecute comprobaciones de verificación y cree el binario.
? Este paso lleva varios minutos.
Correr
make verify
o
cd source/verismo_main; cargo verify --release;
cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;
Un resultado completamente verificado debería tener "verificado": 2138, "errores": 0,
Si no se realizan cambios en source/verismo , recomendamos compilar sin verificación para acelerar el proceso de compilación.
make debugbuild
o
cd source/verismo_main; cargo build --feature noverify --release;
make o make verify ) Descargar el submódulo de Linux: git submodule update --init richos/snplinux
Cree controladores y sistemas operativos invitados: make fs -f Makefile.default
Ejecute sh source/target/target/release/verismo/igvm.sh para generar el verismo en formato IGVM para Hyper-V: source/target/target/release/verismo/verismo-rust.bin
Ejecute make fs para generar un archivo vhdx como sistema de archivos para la VM: richos/test-fs/verismo.vhdx
Hardware: Una máquina AMD SEV-SNP.
SO: Windows con un hipervisor lanzado después de 20230909. Es posible que una versión anterior no admita interrupciones restringidas en ambos VMPL y, por lo tanto, no funcionará.
Opcional: una máquina de depuración con sistema operativo Windows.
Mueva los siguientes archivos a su máquina 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
El acceso GUI no es compatible y debe usar ssh para iniciar sesión en el sistema operativo invitado.
Verismo.vhdx incluye un proceso de inicio que abrirá el servicio sshd sin contraseña.
Espere un minuto antes de conectarse.
ssh [email protected]
Una vez que se inicia el invitado, ya se comunicó con VeriSMo para activar el AP y actualizar los permisos de la página durante el inicio.
Dentro del invitado, también proporcionamos un controlador de verismo y algunas pruebas, para hablar directamente con VeriSMo si lo desea.
verismo.ko: conductor
decode_report: muestra el informe binario en un formato legible.
test.sh: un script de prueba
cd verismo insmod verismo.ko sh test.sh
Consulte la depuración remota de Windows para habilitar la depuración tanto del host como del hipervisor. No se puede acceder al registro de inicio de VeriSMo desde el sistema operativo invitado.
En source/.cargo/config.toml, reemplazamos rustc con verus-rustc. verus-rustc llamará verus para compilar vstd (una biblioteca de verus), verismo y el paquete verismo-main , y llamará rustc para compilar todos los demás paquetes (hacl, core, etc.).
Ver source/verismo/build.rs
noverify: compila la fuente sin verificación
verificarmodule: si ${VERUS_MODULE} no está vacío, verifique solo el módulo especificado.
Depende de cfg(debug_assertations) El modo de depuración imprime mensajes adicionales para fines de depuración a través de fugas_debug; El modo de lanzamiento borra toda la información de fuga_depuración o depuración;
Este proyecto agradece contribuciones y sugerencias. La mayoría de las contribuciones requieren que usted acepte un Acuerdo de licencia de colaborador (CLA) que declara que tiene derecho a otorgarnos, y de hecho lo hace, los derechos para usar su contribución. Para obtener más detalles, visite https://cla.opensource.microsoft.com.
Cuando envía una solicitud de extracción, un bot CLA determinará automáticamente si necesita proporcionar un CLA y decorar el PR de manera adecuada (por ejemplo, verificación de estado, comentario). Simplemente siga las instrucciones proporcionadas por el bot. Solo necesitarás hacer esto una vez en todos los repositorios que utilicen nuestro CLA.
Este proyecto ha adoptado el Código de conducta de código abierto de Microsoft. Para obtener más información, consulte las preguntas frecuentes sobre el Código de conducta o comuníquese con [email protected] si tiene alguna pregunta o comentario adicional.
Este proyecto puede contener marcas comerciales o logotipos de proyectos, productos o servicios. El uso autorizado de las marcas comerciales o logotipos de Microsoft está sujeto y debe seguir las Pautas de marcas y marcas comerciales de Microsoft. El uso de marcas comerciales o logotipos de Microsoft en versiones modificadas de este proyecto no debe causar confusión ni implicar patrocinio de Microsoft. Cualquier uso de marcas comerciales o logotipos de terceros está sujeto a las políticas de dichos terceros.
