该存储库包含 VeriSMo 项目的代码。
tools/ ：包括验证器和编译器工具和脚本。
deps/ : 包括 hacl 包
来源/：verismo代码
source/verismo : verismo 的验证代码
source/verismo_main ：主要可执行 bin，仅定义未经验证的 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;
完全验证的结果应该有“已验证”：2138，“错误”：0，
如果未对source/verismo进行任何更改，我们建议在不进行验证的情况下进行构建，以加快构建过程。
make debugbuild
或者
cd source/verismo_main; cargo build --feature noverify --release;
make或make verify则跳过）下载linux子模块： git submodule update --init richos/snplinux
构建来宾操作系统和驱动程序： 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以生成 vhdx 文件作为 VM 的文件系统： richos/test-fs/verismo.vhdx
硬件：AMD SEV-SNP 机器。
操作系统：带有 Hypervisor 的 Windows 在 20230909 之后发布。早期版本可能不支持两个 VMPL 中的受限中断，因此无法工作。
可选：带有 Windows 操作系统的调试机器。
将以下文件移至您的 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 访问，您需要使用 ssh 登录来宾操作系统。
verismo.vhdx 包含 init 进程，无需密码即可打开 sshd 服务。
连接前请等待一分钟。
ssh [email protected]
一旦 guest 虚拟机启动，它就已经与 VeriSMo 通信以在启动期间唤醒 AP 并更新页面权限。
在 guest 中，我们还提供了 verismo 驱动程序和一些测试，如果您愿意，可以直接与 Verismo 对话。
verismo.ko：驱动程序
解码报告：以可读格式显示二进制报告。
test.sh：测试脚本
cd verismo insmod verismo.ko sh test.sh
请参阅 Windows 远程调试以启用主机和管理程序调试。无法从来宾操作系统访问 VeriSMo 启动日志。
在 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打印额外的消息用于调试目的； Release模式擦除所有leak_debug或debug信息；
该项目欢迎贡献和建议。 大多数贡献都要求您同意贡献者许可协议 (CLA)，声明您有权并且实际上授予我们使用您的贡献的权利。有关详细信息，请访问 https://cla.opensource.microsoft.com。
当您提交拉取请求时，CLA 机器人将自动确定您是否需要提供 CLA 并适当地装饰 PR（例如，状态检查、评论）。只需按照机器人提供的说明进行操作即可。您只需使用我们的 CLA 在所有存储库中执行一次此操作。
该项目采用了微软开源行为准则。有关详细信息，请参阅行为准则常见问题解答或联系 [email protected] 提出任何其他问题或意见。
该项目可能包含项目、产品或服务的商标或徽标。 Microsoft 商标或徽标的授权使用须遵守且必须遵循 Microsoft 的商标和品牌指南。在此项目的修改版本中使用 Microsoft 商标或徽标不得引起混淆或暗示 Microsoft 赞助。对第三方商标或徽标的任何使用均须遵守这些第三方的政策。
