В коде Apollo Guidance Computer обнаружен 57-летний баг, блокировавший управление гироскопом

В легендарном коде бортового компьютера Apollo Guidance Computer (AGC), который считался одной из самых изученных кодовых баз в истории, обнаружен критический баг, остававшийся незамеченным 57 лет. Ошибка в коде гироскопического управления приводила к блокировке ресурсов, утечке на ошибочный путь и отключала возможность изменения положения платформы наведения. Этот дефект, по сути, мог парализовать систему ориентации космического корабля, хотя в реальных миссиях он, по-видимому, не проявился.

Баг был выявлен не в ходе рутинного анализа, а с помощью современных методов формальной верификации. Исследователи использовали ИИ-модель Claude и опенсорсный язык спецификаций Allium для преобразования 130 тысяч строк ассемблерного кода AGC в 12,5 тысячи строк поведенческих спецификаций. Процесс автоматического вывода спецификаций непосредственно из кода и стал тем самым проводником, который привёл к обнаружению скрытой уязвимости.

Это открытие ставит под сомнение абсолютную надёжность исторически значимого ПО, которое прошло через тысячи глаз разработчиков, научные публикации и детальное изучение в эмуляторах. Оно демонстрирует, что даже в канонических, казалось бы, безупречных системах могут десятилетиями скрываться фундаментальные ошибки управления, которые современные инструменты формальной верификации только сейчас начинают выявлять. Инцидент служит мощным сигналом для инженеров, работающих с критически важными системами, о необходимости применения новых методов анализа, выходящих за рамки традиционного код-ревью.