Este repositório inclui o código do projeto VeriSMo.
ferramentas/ : inclui ferramentas e scripts de verificador e compilador.
deps/ : inclui pacote hacl
fonte/: código verismo
source/verismo : código verificado para verismo
source/verismo_main : bin executável principal, que define apenas um manipulador de pânico Rust não verificado.
source/verismo/src/arch : modelo
source/verismo/src/entry.s : um código assembly pequeno e não verificado.
source/target.json: configuração de destino
Primeiro, instale o conjunto de ferramentas de ferrugem;
tools/install.sh
Em seguida, crie ferramentas e dependências verus, verus-rustc (substituindo rustc) e igvm.
tools/activate.sh
Agora, execute verificações e construa o binário.
? Esta etapa leva vários minutos.
Correr
make verify
ou
cd source/verismo_main; cargo verify --release;
cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;
Um resultado totalmente verificado deveria ter "verificado": 2138, "erros": 0,
Se nenhuma alteração for feita em source/verismo , recomendamos compilar sem verificação para acelerar o processo de compilação.
make debugbuild
ou
cd source/verismo_main; cargo build --feature noverify --release;
make ou make verify ) Baixe o submódulo linux: git submodule update --init richos/snplinux
Crie sistemas operacionais e drivers convidados: make fs -f Makefile.default
Execute sh source/target/target/release/verismo/igvm.sh para gerar o verismo no formato IGVM para Hyper-V: source/target/target/release/verismo/verismo-rust.bin
Execute make fs para gerar um arquivo vhdx como sistema de arquivos para a VM: richos/test-fs/verismo.vhdx
Hardware: Uma máquina AMD SEV-SNP.
SO: Windows com hipervisor lançado após 20230909. Versões anteriores podem não suportar interrupções restritas em ambos os VMPLs e, portanto, não funcionarão.
Opcional: Uma máquina de depuração com sistema operacional Windows.
Mova os seguintes arquivos para sua 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
O acesso GUI não é suportado e você precisa usar ssh para fazer login no sistema operacional convidado.
O verismo.vhdx inclui o processo init que abrirá o serviço sshd sem senha.
Aguarde um minuto antes de conectar.
ssh [email protected]
Assim que o convidado for inicializado, ele já conversou com o VeriSMo para ativar o AP e atualizar as permissões da página durante a inicialização.
Dentro do convidado, também disponibilizamos um driver verismo e alguns testes, para falar diretamente com o VeriSMo se quiser.
verismo.ko: motorista
decode_report: exibe o relatório binário em um formato legível.
test.sh: um script de teste
cd verismo insmod verismo.ko sh test.sh
Consulte a depuração remota do Windows para ativar a depuração do host e do hipervisor. O log de inicialização do VeriSMo não está acessível no sistema operacional convidado.
Em source/.cargo/config.toml, substituímos rustc por verus-rustc. verus-rustc chamará verus para compilar vstd (uma biblioteca verus), verismo e pacote verismo-main , e chamará rustc para compilar todos os outros pacotes (hacl, core, etc.).
Veja source/verismo/build.rs
noverify: fonte de compilação sem verificação
verifymodule: se ${VERUS_MODULE} não estiver vazio, verifique apenas o módulo especificado.
Depende de cfg(debug_assertations) O modo de depuração imprime mensagens adicionais para fins de depuração via leak_debug; O modo de liberação apaga todas as informações de leak_debug ou depuração;
Este projeto aceita contribuições e sugestões. A maioria das contribuições exige que você concorde com um Contrato de Licença de Colaborador (CLA), declarando que você tem o direito de nos conceder, e realmente nos concede, os direitos de uso de sua contribuição. Para obter detalhes, visite https://cla.opensource.microsoft.com.
Quando você envia uma solicitação pull, um bot CLA determinará automaticamente se você precisa fornecer um CLA e decorará o PR adequadamente (por exemplo, verificação de status, comentário). Basta seguir as instruções fornecidas pelo bot. Você só precisará fazer isso uma vez em todos os repositórios usando nosso CLA.
Este projeto adotou o Código de Conduta de Código Aberto da Microsoft. Para obter mais informações, consulte as Perguntas frequentes sobre o Código de Conduta ou entre em contato com [email protected] com perguntas ou comentários adicionais.
Este projeto pode conter marcas registradas ou logotipos de projetos, produtos ou serviços. O uso autorizado de marcas registradas ou logotipos da Microsoft está sujeito e deve seguir as Diretrizes de Marcas Registradas e Marcas da Microsoft. O uso de marcas registradas ou logotipos da Microsoft em versões modificadas deste projeto não deve causar confusão nem implicar patrocínio da Microsoft. Qualquer uso de marcas registradas ou logotipos de terceiros está sujeito às políticas desses terceiros.
