VeriWasm：为本地编译的Wasm提供SFI安全

此仓库包含构建VeriWasm以及重现我们NDSS'21论文中提出的结果所需的所有代码和数据信任，但验证：为本地编译的Wasm提供SFI安全。

摘要

WebAssembly (Wasm) 是一种平台无关的字节码，它既提供良好的性能，又提供运行时隔离。为了实现隔离，编译器在将Wasm编译为本机机器代码时插入安全检查。虽然这种方法成本低廉，但它也要求信任编译器的正确性——信任编译器已在每个适当的位置正确地插入了每个必要的检查。不幸的是，Wasm编译器中的微妙错误可能会破坏——并且已经破坏——隔离保证。为了解决这个问题，我们建议在编译后验证Wasm二进制文件的内存隔离。我们在VeriWasm中实现了这种方法，VeriWasm是一个针对从Wasm编译的本机x86-64二进制文件的静态离线验证器；我们证明了验证器的正确性，并发现它可以检测到没有误报的错误。最后，我们描述了我们在Fastly上的VeriWasm部署。

构建VeriWasm

首先，您需要安装几个依赖项

• git
• Rust
• nasm（用于编译测试用例）
• gcc（用于编译测试用例）
• python3（用于脚本）

一旦您拥有这些，您就可以构建VeriWasm

git submodule update --init --recursive
cargo build --release

运行VeriWasm

要在您的二进制文件上运行VeriWasm，只需将其指向您想要检查的模块即可

cargo run --release -- -i <input path> 

用法

VeriWasm 0.1.0
Validates safety of native Wasm code

USAGE:
    veriwasm [FLAGS] [OPTIONS] -i <module path>

FLAGS:
    -h, --help       Prints help information
    -q, --quiet      
    -V, --version    Prints version information

OPTIONS:
    -j, --jobs <jobs>                   Number of parallel threads (default 1)
    -i <module path>                    path to native Wasm module to validate
    -o, --output <stats output path>    Path to output stats file

重现评估结果

此仓库包含重现论文中描述的结果所需的所有基础设施。一旦构建了VeriWasm，您就可以运行我们的测试和性能基准。

运行评估套件

要验证论文中描述的所有二进制文件（除了SPEC CPU 2006二进制文件（它们是专有的）和Fastly生产二进制文件），请运行

git clone https://github.com/PLSysSec/veriwasm_public_data.git
cd veriwasm_public_data && sh setup.sh && sh build_negative_tests.sh && cd ..
cargo test --release

要获取二进制文件的性能统计信息，请运行

make compute_stats
python3 graph_stats.py stats/*

模糊VeriWasm

要模糊VeriWasm，您需要安装 cmake 然后构建模糊器（以及它们所依赖的工具）

make build_fuzzers

然后，运行基于 Csmith 的模糊器

cd veriwasm_fuzzing
make csmith_fuzz

或基于Wasm的fuzzer

cd veriwasm_fuzzing
make wasm_fuzz

默认情况下，make将使用四个核心；您可能需要更改此设置。

相关仓库

• 用于评估的二进制文件：我们评估过程中验证的二进制文件在此。

• Fuzzing脚本：我们用于fuzz VeriWasm的脚本在此。

• 机械化证明：我们论文中的证明在此。