C 有界模型检查器：严重被低估

原文 ↗ Hacker News 讨论 ↗

像 CBMC 这样的形式化验证工具——它是 C 的有界模型检查器，也是 Amazon 的 Kani（Rust 验证工具）的后端——因能在给定边界内穷尽探索程序路径，从而发现缓冲区溢出和逻辑错误等微妙漏洞而受到称赞。评论者讨论了这些工具在超出小型、单元测试式代码后的可扩展性，它们与 Frama-C、KLEE 和 sanitizer 等替代方案的比较，以及其所需投入是否比转向更安全的语言更值得。讨论进一步扩展到 C 的长期问题——未定义行为、缺少数组长度信息以及薄弱的安全保证——以及语言演进还是外部工具才是迈向更安全底层软件的更现实路径。

CBMC 的采用与使用场景

  • 几位评论者认为 CBMC 使用得太少，并主张把硬件风格的形式化验证带入主流软件。
  • 举出的例子包括：验证加密代码、AWS 的 C 库、FreeRTOS 组件、HTTP 客户端函数，以及大型商业 C 项目（约 50 万行代码）。
  • 一些用户表示确实找到了真实漏洞，例如缓冲区溢出、拒绝服务循环，以及解析器和网络代码中的问题。

可扩展性与验证风格

  • 共识是：CBMC 最适合单元级或小模块级，而不是整个大型系统。
  • 有效使用需要：
    • 基于契约的设计：明确的前置/后置条件和断言。
    • “Shadow” 函数，用于用更简单、非确定性的模型替换复杂的被调用方，同时遵守相同契约。
    • 保持搜索深度较浅，使每次运行都能快速完成。
  • 将其后改造到遗留的、结构不佳的代码上，被认为比从一开始就使用它更困难。

与其他工具的比较

  • Frama-C、Coq VST、seL4 的方法：更强大，但需要更多专业知识，且不容易扩展到日常代码。
  • KLEE：对 GNU text/coreutils 这类简单工具效果不错；在处理复杂的结构化输入（例如 protobuf、C++ 容器）时会遇到困难。
  • 静态分析器（例如编译器分析器加注解）可以覆盖部分缓冲区问题；CBMC 仍被看作另一层安全保障。
  • CBMC 也被用作 Kani 的后端，Kani 是一个 Rust 验证工具。

C 数组、边界与语言设计

  • 讨论延伸到 C 在数组退化为指针时丢失数组大小、从而导致缓冲区漏洞的问题。
  • 讨论中的提议包括：fat pointer/slice、非拥有型定长数组，以及指向数组的参数；其中一些已在其他语言中实现。
  • 有人对 C 标准至今未采纳这些特性表示沮丧，却接受了更冷门的特性（例如 Unicode 标识符）。

未定义行为与未初始化内存

  • CBMC 将未初始化的局部变量建模为非确定性值，这可能与 C 的 UB 语义不同。
  • 有人认为验证器应将任何 UB（例如读取未初始化变量）视为立即错误；也有人指出 CBMC 当前关注的是“类 C”模型，而不是精确的 C 语义。
  • 围绕 UB、编译器优化、“friendly/boring C”、sanitizer 和操作系统行为的长讨论，显示出人们对 UB 驱动的误编译和安全漏洞的深切担忧。
  • 大家一致认为，CBMC 应与编译器警告和 sanitizer 一起使用，作为纵深防御的一部分。