想法与洞见 · 页 3

探索 AI 优先开发、编码护栏和可处置架构。

2026年8月5日

Meta用从不运行程序的静态分析器在投产代码中发现了10万个缺陷

Meta的Infer利用抽象解释和双向推理，通过推理代码结构而非执行来发现空指针解引用、内存泄漏和竞态条件。以下是它的工作原理以及如何在您自己的代码库中使用它。

2026年8月4日

抽象解释会对每一种可能的程序状态进行过度近似。如果除零错误在抽象中不可达，那它在真实代码中就不可达。以下是它的工作原理以及它的局限性。

2026年8月3日

抽象解释让你在执行之前就证明运行时错误不可能发生。以下是它的实际工作原理、难点所在，以及它在你的工具链中的定位。

2026年8月2日

CHERI 的 hybrid ABI 让你可以逐步将 C 代码移植到 capability 硬件上。本文介绍如何编译、哪些代码会出问题，以及如何在不 rewrite 整个 codebase 的情况下修复它们。

2026年8月1日

自 1970 年代以来，硬件层面的内存安全性就已可行。以下是权能架构为何一直败给扁平内存模型，以及为什么 CHERI 终于正在改变这一等式。

2026年7月31日

用容器来隔离单个 C 库未免小题大做。将其编译为 WebAssembly，在 WASI 沙箱中运行，即可实现内存安全、基于权能的文件系统访问和崩溃隔离，无需 Docker。

2026年7月30日

ARM Memory Tagging Extension 和 GWP-ASan 让现代移动设备在生产环境中检测内存安全成为可能。本文介绍它们的工作原理和权衡取舍。

2026年7月29日

CHERI是一种硬件扩展，它将每个指针转变为带有边界的权能。本文介绍它如何在CPU层面阻止缓冲区溢出、代价几何，以及如何在真实硬件上试用。

2026年7月28日

净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。

2026年7月27日

Cleanroom software engineering 将 defect rate 降低 100 倍，但全面采用需要独立的 test team 和 formal proof。这里介绍一种 pragmatic subset，无需 overhead 即可捕获大部分收益。