跳转到内容
Jason's Study

ASTRÉE 分析器 — 让飞机控制代码的静态分析做到零警告

是什么

ASTRÉE 是一个专门跑 C 写的飞机控制代码、能证明它一辈子不会出运行时错误的静态分析器。日常类比：它像一位极偏科的体检医生——只看一类病人（嵌入式控制软件），但对这一类，能给出”我保证你这辈子不会得这五种病”的体检报告。

它处理的代码长这样：

float pitch = sensor_read();
float command = K1 * pitch + K2 * pitch_prev;
if (command > LIMIT) command = LIMIT;
actuator_write(command);

ASTRÉE 读完整段（数十万行类似代码），输出：“0 个警告——证明除零、溢出、数组越界、未初始化、无效指针这五类错误一个都不会发生。”

这份”零警告报告”是 Airbus A380、A350 飞控真正用来过认证的依据之一。

为什么重要

不理解 ASTRÉE，下面这些事都没法解释：

  • 为什么 Cousot 1977 提出的抽象解释一直被吐槽”误报多到没法用”，到 2005 年突然能给空客出零警告报告
  • 为什么”静态分析必有大量 false positive”这条共识在某些场景就是错的
  • 为什么后来 Infer / Frama-C / SLAM 都把 ASTRÉE 当精度基准
  • 为什么”通用工具” vs “专用工具”在静态分析里差距能拉到 10 倍精度

核心要点

ASTRÉE 的招数可以拆成 三步：

  1. 窄输入：只接受无递归、无动态分配、无系统调用、无并发的 C 子集——这正好覆盖嵌入式飞控代码。把通用问题缩成专用问题，精度才能拉高。

  2. 专用抽象域叠加：不止用经典区间域，而是把多个针对性抽象域装在一起——

    • 八边形（octagon）：能表达 x − y ≤ c 这种两变量线性约束
    • 椭圆（ellipsoid）：专为数字滤波器（如 y = a·x + b·y_prev）设计，能证明滤波器输出不发散
    • 布尔关系：跟踪 flag1 && !flag2 ⇒ x in [0, 10] 这种条件依赖
    • decimal 浮点域：算清楚 IEEE 754 浮点的舍入边界

  3. trace partitioning：同一个变量在不同 if 分支走过的路径上分开存抽象值，不在汇合点早早合并。类比：医生不把”喝可乐的患者”和”喝水的患者”血糖平均一下，而是分开看。

三步加起来：窄定义域 + 多抽象域叠加 + 精细分区 = 把误报压到零。

实践案例

案例 1：椭圆域专治数字滤波器

飞控里典型代码：

y = 0.7 * x + 0.3 * y_prev;
y_prev = y;

普通区间域会推：“y_prev 每一轮都可能变大一点 → 区间不断膨胀 → 最终溢出”——误报。

椭圆抽象域知道这是个二阶数字滤波器，从控制理论查表得到”输出有界且收敛”，于是推出 y ∈ [−M, M] 永远成立，零警告通过。

这是 ASTRÉE 设计哲学的精华：领域知识硬编码进抽象域。

案例 2：trace partitioning 救误报

if (mode == LANDING) {
    gain = 1.5;
} else {
    gain = 0.8;
}
out = gain * input;

不分区时分析器会把 gain 合并成 [0.8, 1.5]，再乘 input 时区间放大太多，下游某处可能误报溢出。

trace partitioning 让分析器记住”gain=1.5 的那条路径”和”gain=0.8 的那条路径”是分开的，到 out 时分两条算，最后再合并。精度高一倍，警告消失。

案例 3：A340 实战数据（论文原话）

  • 输入规模：13.2 万行 C（A340 飞控核心循环）
  • 警告数：0
  • 分析时间：约 1 小时（2005 年的服务器）
  • A380（数十万行）：0 警告，分析时间数小时

这种数字让 Airbus 把 ASTRÉE 写进 DO-178B（航空软件认证标准）的证据链。

踩过的坑

  1. 抽象域不是免费午餐：每加一个抽象域，分析时间和实现复杂度都涨一截。ASTRÉE 团队花了好几年针对 Airbus 代码手工调参，才把零警告稳住。

  2. 稍微换一类代码就退化：把 ASTRÉE 拿去跑 Linux 内核或浏览器引擎——递归、malloc、并发样样有，它直接拒绝输入。它不是通用工具。

  3. 零警告 ≠ 无 bug：ASTRÉE 只证明那五类运行时错误不会发生，逻辑 bug、规格错误、需求错误它都看不见。Airbus 仍要做大量测试和形式验证补足。

  4. widening 调不好就发散：无限格（如区间）必须用 widening 算子强制跳到更宽的值才能收敛。调得太激进精度全丢、调得太保守永远算不完——ASTRÉE 的 widening 策略是论文里没完全公开的工程秘方。

适用 vs 不适用场景

适用：

  • 嵌入式控制软件（飞控、汽车 ECU、医疗设备控制器）
  • 无动态分配、无并发、循环结构规整的 C/C++ 代码
  • 安全认证场景（DO-178B、ISO 26262）需要”证明无某类错误”
  • 数字信号处理代码（椭圆域天然契合）

不适用：

  • 通用应用代码（含 malloc/递归/线程）→ 用 Infer / CodeQL / Coverity
  • 需要证明业务正确性 → 用 Frama-C + ACSL / F* / Dafny
  • 需要快速反馈（秒级）→ 用类型系统 / Rust borrow checker
  • 分析非 C 代码（Java/Python/Rust）→ 各自有专用工具

历史小故事（可跳过）

  • 1977 年：Cousot 夫妇发表抽象解释开山论文，建立 Galois connection + 不动点迭代框架。学界认知是”理论漂亮但精度差，工业用不了”。
  • 1990s：Cousot 学派持续做抽象域研究（八边形、多面体），但工业落地少。
  • 2001 年：Airbus 找到 Cousot 团队，问能不能证明 A340 飞控无运行时错误。团队决定针对这一类代码专门做工具。
  • 2003 年：A340 上线前，ASTRÉE 第一次跑出零警告。
  • 2005 年：ESOP 论文公开方法。这就是本篇笔记的对象。
  • 2007 年：A380 首飞，ASTRÉE 是其飞控验证工具链一员。
  • 后续：AbsInt 公司商业化，今天卖给汽车与航天客户。

学到什么

  1. 专用 > 通用：在静态分析这个领域，把问题域窄到一类代码，精度可以拉到普通工具的 10 倍以上
  2. 抽象域选得对，错误就消失：椭圆域之于数字滤波器，是”用对工具”的教科书案例
  3. 理论 → 工程要 25 年：1977 → 2005 ASTRÉE 落地，跨度跟 HM（1969 → 1990s）相当
  4. 零警告是工程目标不是理论目标：要靠定制抽象域 + 调参 + 领域知识硬编码，不是单纯算法改进

延伸阅读

关联

  • cousot-abstract-interpretation —— 1977 理论框架；ASTRÉE 是它最成功的工业落地
  • kildall-dataflow —— 数据流分析的格论基础，抽象解释的近亲
  • biere-bmc-1999 —— 有界模型检查；与抽象解释互补的另一条静态验证路线
  • sagiv-shape-analysis —— 形状分析；针对堆数据结构的专用抽象解释，与 ASTRÉE 同思路不同战场
  • hoare-logic —— 演绎式程序验证；与抽象解释并列的两大形式方法路线

反向链接

  • apron-2009 —— Apron — 把区间/八边形/多面体塞进同一个插槽
  • biere-bmc-1999 —— Bounded Model Checking — 把硬件验证翻译成一道 SAT 题
  • cousot-abstract-interpretation —— Cousot 抽象解释 — 给静态分析一套统一数学框架
  • cousot-halbwachs-polyhedra-1978 —— Cousot-Halbwachs 凸多面体域 — 让分析器自己发现变量间的线性关系
  • frama-c-2012 —— Frama-C — 一个开源平台把 C 程序的多种验证方法拼到一起
  • hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
  • kildall-dataflow —— Kildall 数据流框架 — 用一套格论统一所有全局编译优化
  • mine-octagon-2006 —— Miné 八边形抽象域 — 在区间和多面体之间的甜点
  • sagiv-shape-analysis —— Sagiv 参数化形状分析 — 用三值逻辑证明链表树仍是链表树
  • slam-microsoft —— SLAM — 让 Windows 驱动 bug 自己撞到工具上
  • vcc-2009 —— VCC — 给并发 C 加注解，让 SMT 自动证它对