We found an undocumented bug in the Apollo 11 guidance computer code
4 hours ago
- #Apollo Guidance Computer
- #Formal Verification
- #Software Bug
- A bug was found in the Apollo Guidance Computer (AGC) code after 57 years: a resource lock (LGYRO) in the gyro control code leaks on an error path, disabling the guidance platform's ability to realign.
- The bug was discovered using Claude and Allium, an open-source behavioural specification language, which distilled 130,000 lines of AGC assembly into 12,500 lines of specs to identify the defect.
- The AGC's code had been publicly available and scrutinized since 2003, but no formal verification or static analysis had been published before this approach.
- The bug occurs when the Inertial Measurement Unit (IMU) is caged during a torque operation, causing the code to exit via BADEND without clearing the LGYRO lock, leading to a permanent hang in gyro operations.
- A hypothetical scenario during Apollo 11 could have left Michael Collins stranded behind the Moon with a non-functional alignment system, though a hard reset would have cleared the issue.
- Margaret Hamilton's team pioneered software engineering concepts, and priority scheduling saved the Apollo 11 landing from 1202 alarms, but specification errors, not coding mistakes, were the most serious bugs.
- Modern languages have mechanisms to prevent resource leaks, but similar issues persist in systems where programmers manually manage resources, classified as CWE-772 by MITRE.
- The bug existed in both Command Module and Lunar Module software across missions but was never noticed or fixed, highlighting the importance of behavioral specifications to catch such defects.