阿波罗11号导航计算机代码中发现57年未知的隐藏Bug

利用Claude AI和行为规范语言Allium，研究人员在阿波罗导航计算机（AGC）代码中发现了一个57年来未知的Bug。这个缺陷——陀螺仪控制系统中的资源锁泄漏——可能曾静默地禁用航天器重新对准导航平台的能力。

Bug的细节

AGC通过名为LGYRO的共享资源锁管理其惯性测量单元（IMU）。当计算机需要对陀螺仪施加力矩时，它在开始时获取LGYRO，在所有三个轴完成力矩后释放。

正常路径工作正确：获取锁→力矩→释放锁。但存在第三种情况——锁定（caging）——不会释放锁。

锁定是一项紧急措施，通过物理夹紧IMU的万向节来保护陀螺仪。当力矩进行中IMU被锁定时，代码通过名为BADEND的例程退出，跳过了清除LGYRO锁的两条指令：

CAF ZERO
TS LGYRO

仅缺失四个字节。

后果

一旦LGYRO卡死，后续每次尝试对陀螺仪施加力矩都会发现锁被持有，等待一个永远不会到来的唤醒信号，然后挂起。

历史背景

在阿波罗11号任务期间，Michael Collins独自在指令舱哥伦比亚号中绕月飞行。每隔两小时他就消失在月球背面。每次飞越期间，他运行52号程序——一个星瞄准对准程序。如果平台因这个Bug发生漂移，带他回家的发动机点火将指向错误方向。

发现方法

团队使用Allium将13万行AGC汇编代码提炼为1.25万行规范，直接指向了缺陷——数十年的手动阅读和仿真都未能发现。

更广泛的意义

1. 规模化形式方法 — AI可以从手动分析不切实际的海量代码库中推导行为规范
2. 资源管理Bug — 锁泄漏仍然是安全关键代码中最危险的并发Bug之一
3. 遗留系统验证 — 许多关键基础设施系统从未经过正式验证