Программное обеспечение бортового компьютера миссии «Аполлон» (AGC) по праву считается одной из самых детально изученных систем в истории информатики. Его код анализировали тысячи специалистов, он становился предметом научных работ по надежности, а современные эмуляторы позволяют запускать его пошагово. Тем не менее, нам удалось обнаружить уязвимость, которая, по-видимому, оставалась скрытой на протяжении пятидесяти семи лет: критическую ошибку синхронизации в подсистеме управления гироскопами. Этот недочет приводил к некорректному завершению процесса и «зависанию» блокировки, что лишало систему возможности корректировать ориентацию аппарата в пространстве.
Для проведения анализа мы использовали Claude совместно с Allium — нашим инструментом для формализации поведенческих спецификаций. Преобразовав 130 тысяч строк ассемблерного кода AGC в лаконичную модель из 12,5 тысяч строк, мы смогли выявить проблемный участок, опираясь исключительно на логику работы системы.
Архитектура «вязаной» памяти
Исходный код AGC стал достоянием общественности в 2003 году, когда группа энтузиастов во главе с Роном Бёрки начала оцифровку бумажных распечаток из MIT Instrumentation Laboratory. Позднее, в 2016 году, репозиторий Криса Гарри на GitHub привлек огромное внимание сообщества, позволив разработчикам со всего мира прикоснуться к уникальному коду, который работал на машине с 2 КБ ОЗУ и тактовой частотой в 1 МГц.
Основная часть ПО размещалась в «вязаной» памяти (core rope memory) объемом 74 КБ. Это была аппаратная реализация алгоритмов: медная проволока продевалась через магнитные сердечники вручную. Интересно, что сборку таких модулей выполняли сотрудницы производства, которых называли «маленькими старушками» (отсюда ироничное название LOL-память). Точность эмуляции, достигнутая проектами вроде Virtual AGC, подтверждается полным соответствием дампов памяти оригиналу.
Несмотря на тщательность изучения, широкой публике не было представлено результатов формальной верификации или статического анализа полётного кода. Мы же применили иной подход: с помощью Allium мы составили поведенческую модель модуля инерциальной навигации (IMU), ответив на вопросы о жизненном цикле ресурсов: кто, когда и при каких условиях запрашивает и освобождает доступ к ним.
Утечка блокировки
Для управления IMU компьютер использует семафор LGYRO. Перед выполнением маневров или коррекцией дрейфа система блокирует этот ресурс, чтобы избежать конфликтов при доступе к аппаратному обеспечению гироскопов. В штатном режиме блокировка снимается после успешного завершения операции.
Однако существует альтернативный сценарий — экстренное торможение гироскопов (caging), инициируемое астронавтом с панели управления. В этом случае код переходит к подпрограмме BADEND, которая, к сожалению, не содержит инструкций по освобождению LGYRO:
CAF ZERO
TS LGYROОтсутствие этих четырех байт кода приводило к тому, что при последующих попытках корректировки ориентации система уходила в бесконечное ожидание освобождения ресурса. Все команды по стабилизации платформы оказывались заблокированы.
Риски в глубоком космосе
Представим ситуацию: Майкл Коллинз, находясь в одиночестве на орбите Луны, проводит выравнивание платформы (программа P52). Случайное нажатие кнопки экстренного останова вызывает срабатывание BADEND. Попытка повторного запуска P52 приводит к полному «оцепенению» системы управления гироскопами. Коллинз видит работающий интерфейс DSKY, но не получает никакой обратной связи при попытках исправить положение. В условиях критической важности стыковки с модулем, находящимся на поверхности, такой отказ мог стать фатальным.
Наследие Маргарет Гамильтон
Маргарет Гамильтон и её команда заложили фундамент современной инженерии ПО, внедрив многозадачность, систему приоритетов и механизмы восстановления. Именно приоритетное планирование позволило компьютеру справиться с перегрузкой во время посадки «Аполлона-11», когда сработали знаменитые сигналы тревоги 1202.
Наш анализ показал, что современные инструменты верификации, такие как Allium, способны находить ошибки в самой спецификации логики, а не только в опечатках кода. В то время как классические тесты проверяют лишь ожидаемое поведение, формальные спецификации позволяют задавать вопросы о фундаментальных правилах работы системы, выявляя уязвимости на ранних этапах проектирования.
Примечание редакции
После публикации материала с нами связался Майк Стюарт, эксперт VirtualAGC, и пояснил, что данный баг не остался незамеченным навсегда. В ходе разработки ПО для миссий «Аполлон-15» и последующих, данная аномалия (зарегистрированная как L-1D-02) была устранена. Более того, архитектура системы такова, что переход между любыми основными программами (через вызов FRESH_START) принудительно обнулял блокировку, что фактически служило «предохранителем» и спасало ситуацию в большинстве сценариев. Проблема была глубокой, но, благодаря выдающейся инженерной культуре того времени, она не стала препятствием для успеха программы «Аполлон».