Meta用从不运行程序的静态分析器在投产代码中发现了10万个缺陷
Meta的Infer利用抽象解释和双向推理，通过推理代码结构而非执行来发现空指针解引用、内存泄漏和竞态条件。以下是它的工作原理以及如何在您自己的代码库中使用它。
Meta已经发布了超过10万个由静态分析器在代码到达用户之前捕获的缺陷修复。这个工具名为Infer，它是开源的，并且不会运行您的代码。它读取代码，构建代码可能执行的数学模型，并证明某些坏事不可能发生。或者它会找到一条可能发生的路径。…
想法与洞见
探索 AI 优先开发、编码护栏和可处置架构。
静态分析无法证明你的飞机不会坠毁。但它能证明一些更有用的东西。
抽象解释会对每一种可能的程序状态进行过度近似。如果除零错误在抽象中不可达，那它在真实代码中就不可达。以下是它的工作原理以及它的局限性。
静态分析无法证明飞机不会坠毁。但它可以证明你的高度计控制回路永远不会出现除零运算、永远不会越界索引、永远不会使定点累加器溢出。这种区别很重要，因为前者是对物理、空气动力学和铝材在应力下的断言，而后者是对代码的断言——你可以在飞机离地之前就验证它。…
如何证明你的代码没有运行时错误（以及为什么你很可能会放弃尝试）
抽象解释让你在执行之前就证明运行时错误不可能发生。以下是它的实际工作原理、难点所在，以及它在你的工具链中的定位。
你的测试套件通过了。你的类型检查器全是绿色。你发布了。两小时后，生产环境在一个没人想到要测试的边界情况上抛出了 。 测试能发现 bug。类型系统能预防一部分。但两者都无法证明你的程序完全没有运行时错误。要做到这一点，你需要更强力的手段：一种能够同时对所有可能的执行路径进行推理、而无需实际运行代码的方法。…
你的 C 代码无需全面 rewrite 即可在 capability 硬件上运行
CHERI 的 hybrid ABI 让你可以逐步将 C 代码移植到 capability 硬件上。本文介绍如何编译、哪些代码会出问题，以及如何在不 rewrite 整个 codebase 的情况下修复它们。
你有一个用 C 编写的codebase，它大到无法全部用 Rust rewrite，又关键到不能任由缓冲区溢出威胁。CHERI capability 硬件承诺在 CPU 层面捕获内存安全违规，但网上一直有人说 CHERI 指针是 128 位的，而你的代码默认指针是 64 位。 好消息是，CHERI…
权能硬件没有失败。它只是提前 40 年到来。
自 1970 年代以来，硬件层面的内存安全性就已可行。以下是权能架构为何一直败给扁平内存模型，以及为什么 CHERI 终于正在改变这一等式。
70% 的 CVE 是内存安全缺陷。缓冲区溢出、释放后使用、重复释放。这类漏洞让攻击者可以从一张畸形 JPEG 一路提权到 root 访问。 自 1975 年以来，我们就知道如何在硬件层面阻止其中的大部分。剑桥 CAP 计算机使用了基于权能的寻址。卡内基梅隆大学的 Hydra…
你的 C 依赖库可能让整个进程崩溃。WebAssembly 可以阻止它。
用容器来隔离单个 C 库未免小题大做。将其编译为 WebAssembly，在 WASI 沙箱中运行，即可实现内存安全、基于权能的文件系统访问和崩溃隔离，无需 Docker。
C 库内部的一次空指针解引用就可能导致整个应用程序崩溃。如果该库负责解析用户输入、解压图像或处理网络协议，那么一个畸形的数据包就足以引发崩溃。容器确实能解决这个问题，但仅为一个依赖项就启动 Docker，无异于为盆栽雇佣保镖。你需要的是没有额外开销的隔离。 WebAssembly 加上 WASI…
你的手机已经拥有能检测内存损坏的硬件
ARM Memory Tagging Extension 和 GWP-ASan 让现代移动设备在生产环境中检测内存安全成为可能。本文介绍它们的工作原理和权衡取舍。
你的手机可以在生产环境中检测内存损坏。不是用你在 CI 中运行的完整插桩，也不是针对每一次分配。但你口袋里的硬件在几年前就已经搭载了必要的原语，而且越来越多的生产应用正在悄悄启用它们。 简而言之：AddressSanitizer 对生产环境来说太贵了。ARM Memory Tagging Extension…
缓冲区溢出之所以反复发生，是因为我们在软件层面修复它
CHERI是一种硬件扩展，它将每个指针转变为带有边界的权能。本文介绍它如何在CPU层面阻止缓冲区溢出、代价几何，以及如何在真实硬件上试用。
缓冲区溢出在CWE Top 25榜单上盘踞了二十年之久。我们拥有栈金丝雀、ASLR、DEP、控制流完整性以及内存安全语言，然而它们仍然不断出现在关键代码中。原因很简单：这些缓解措施无一不是在软件中运行的，而软件可以被绕过、被错误配置，或者干脆未被启用。 倘若硬件本身拒绝让你读取数组末尾之后的数据呢？…
LLM 无法证明你的代码正确，但它们可以撰写实现证明的样板代码
净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。
净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。 瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM…
Cleanroom 实现每千行 0.1 个缺陷。你不需要全盘照搬也能达到这个目标。
Cleanroom software engineering 将 defect rate 降低 100 倍，但全面采用需要独立的 test team 和 formal proof。这里介绍一种 pragmatic subset，无需 overhead 即可捕获大部分收益。
Cleanroom software engineering 每千行代码仅产生 0.1 个缺陷。业界平均水平是 10 到 50。问题是，完整的 Cleanroom 要求你将团队拆分为 author 和 verifier，在每个 module 之前编写 formal specification，并禁止…