Apollo 11导航计算机中的Bug：57年未被发现
发现：阿波罗制导计算机(AGC)代码中存在一个57年未被发现的bug——在陀螺仪控制代码中，一个资源锁在错误路径上泄漏，导致导航平台无法重新对齐。
代码审查的盲点
阿波罗制导计算机(AGC)是人类历史上审查最严格的代码之一：
- 数千年开发者读过它
- 学术界发表了关于其可靠性的论文
- 仿真器逐指令运行它
- Ken Shirriff分析到单个门级
但所有审查都是特定类型的：读代码、仿真代码、验证转录。没有形式化验证或模型检查。
新方法：Allium行为规范语言
JuxT团队使用Claude和Allium（开源行为规范语言）将130,000行AGC汇编代码提炼成12,500行规范。规范直接从代码中推导，过程直接指向缺陷。
关键数据：
• AGC代码：130,000行汇编
• Allium规范：12,500行
• 原始RAM：2K
• 时钟频率：1MHz
• 存储：74KB core rope memory（手工编织）
• AGC代码：130,000行汇编
• Allium规范：12,500行
• 原始RAM：2K
• 时钟频率：1MHz
• 存储：74KB core rope memory（手工编织）
Bug详情：LGYRO锁泄漏
AGC通过名为LGYRO的共享资源锁管理IMU（惯性测量单元）。当计算机需要扭矩陀螺仪时，获取LGYRO并在所有三个轴完成后释放。锁防止两个例程同时争夺陀螺仪硬件。
- 正常路径：通过STRTGYR2退出，LGYRO锁被清除
- caging（紧急措施）：物理夹具锁定IMU万向节以保护陀螺仪
- Bug：当IMU在扭矩进行中被caging时，代码通过BADEND退出，不清除锁。缺少两条指令：
CAF ZERO; TS LGYRO（4字节）
后果：一旦LGYRO卡住，每次后续扭矩尝试都发现锁被持有，等待永远不会到来的唤醒信号，然后挂起。精细对齐、漂移补偿、手动陀螺仪扭矩：全部被阻止。
历史背景
1969年7月21日，当Neil Armstrong和Buzz Aldrin在月球表面行走时，Michael Collins独自在哥伦比亚号指令舱中绕月飞行。每两小时他消失在月球背面，与地球失联。
每次通过他运行程序52——星观测对齐，保持制导平台指向正确方向。如果平台漂移，带他回家的引擎燃烧将指向错误的方向。
方法论意义
这个发现的重要性：
- 代码审查的局限：即使是最严格的人工审查也会遗漏并发和错误处理问题
- 形式化验证的价值：行为规范可以发现阅读和仿真错过的缺陷
- AI辅助分析：Claude + Allium的组合能够处理以前只能手工完成的分析
核心教训：对于关键系统，形式化验证不是"最好有"，而是"必须有"。即使是最神圣、历史最悠久的代码也可能隐藏致命缺陷。
收录时间: 2026-04-08 | 来源: JuxT Blog