解读

在国内一线厂、量化与区块链团队的 Rust 面试中，unsafe 块是“性能与安全的分水岭”。面试官并不满足于“尽量少用”这类套话，而是想确认候选人能否把不可证明的 unsafe 操作封装成可审计、可单元测试、可静态验证的契约，并给出可落地的工程化流程。回答要体现“编译期尽量多推、运行期尽量少猜、人工尽量多审”的 Rust 文化。

知识点

1. 契约（Contract）三要素：前置条件、不变式、后置条件。
2. 语言级工具：SAFETY: 注释、debug_assert!、 assert_unchecked!（nightly）、#[cfg(debug_assertions)]。
3. 静态验证：
   • Miri：检测未定义行为（UB），CI nightly 跑。
   • Prusti、Creusot、Kani：前置/后置条件形式化证明，国内华子、蚂蚁已有试点。
4. 动态模糊 + 单元测试：cargo-fuzz、libfuzzer-sys、proptest，把 unsafe 边界值全部跑一遍。
5. 封装准则：最小暴露、最大封装——unsafe 块只在私有模块出现，对外提供 100 % safe API；公开接口用 #[forbid(unsafe_code)] 强制隔离。
6. 代码审查清单（Checklist）：
   • 指针是否可能空、未对齐、悬垂？
   • 生命周期是否短于实际使用？
   • 别名规则是否违反 &mut 独占？
   • 并发场景是否出现 data race？
   • 数字转指针是否越界？
7. 文档化：每个 unsafe 块必须写 “SAFETY: xxx” 注释，并链接到对应单元测试用例编号，方便后续回归。

答案

“验证 unsafe 块契约”我采用 四层防线：

1. 契约先行
   在写代码前先用注释写明前置条件、不变式、后置条件，例如：

   // SAFETY: `ptr` 必须由 Box::into_raw 产生且未释放；offset 在 0..len 范围内。
   let slice = unsafe { std::slice::from_raw_parts(ptr, len) };
   

2. 静态证明

   • 本地用 cargo +nightly miri test 跑全部测试，Miri 无 UB 报警才能进主干。
   • 对关键路径用 Kani 做形式化验证，把“不可能越界”写成 kani::assume 和 kani::assert，让 SAT 求解器自动证明。

3. 动态轰炸

   • 为每个 unsafe 块手写 proptest 策略，自动生成边界输入：空指针、首尾地址、奇数对齐、极端长度。
   • CI nightly 跑 cargo fuzz 至少 1 亿 次迭代，崩溃用例立即进回归池。

4. 人工审计与封装

   • 代码合并前必须经过 两人以上 Rust 专家 Review，使用内部 Checklist 逐条打勾。
   • 所有 unsafe 限制在 私有 mod raw_ffi，对外只暴露 safe 包装，并在 lib.rs 顶部加 #![forbid(unsafe_code)] 强制隔离。

通过“契约注释 → Miri/Kani → Fuzz → Review”四步，我们把不可证明的 unsafe 变成了可审计、可回归、可复现的工程流程；过去两年我们在生产环境零 segfault、零 CVE。

拓展思考

1. 当 Miri 遇到 FFI 内存（如 mmap 或 DMA 缓冲区）会误报，此时可用 Kani 的 __CPROVER_allocate 模型或 Rust-Verifier 做抽象建模，把硬件地址当成不透明的符号地址进行验证。
2. 异步 unsafe：tokio 的 AsyncFd 在 epoll 就绪后用户再读，可能因内核队列为空产生 EAGAIN；此时契约要加 “调用者必须保证 epoll 事件仍在”，并用 loom 做并发状态机测试。
3. 国内合规要求：等保 2.0 对“内存安全可审计”有明文条款，把 unsafe 契约文档、Miri 报告、Kani 证明脚本打包进交付物，可直接作为第三方渗透测试的豁免证据，显著缩短过审周期。