Код бортового управляющего компьютера космического аппарата Аполлон (AGC) — одна из самых тщательно исследованных кодовых баз в истории. Её прочитали тысячи разработчиков. Учёные публиковали статьи о её надёжности. Эмуляторы выполняют её команда за командой. Мы обнаружили в ней баг, который, похоже, оставался незамеченным пятьдесят семь лет: блокировку ресурсов в коде гироскопического управления, приводящую к утечке на ошибочный путь и отключающую возможность изменения положения платформы наведения.

Для преобразования 130 тысяч строк ассемблерного кода AGC в 12,5 тысячи строк спецификаций мы воспользовались Claude и Allium — нашим опенсорсным языком создания поведенческих спецификаций. Спецификации были выведены из самого кода, и этот процесс направил нас непосредственно к багу.

Картирование кода

Исходный код был опубликован в 2003 году, когда Рон Бёрки с командой добровольцев начали кропотливо переписывать его вручную с напечатанных листингов из MIT Instrumentation Laboratory. В 2016 году завирусился репозиторий GitHub бывшего стажёра НАСА Криса Гарри. Тысячи разработчиков изучали ассемблерный код машины с 2 КБ перезаписываемого ОЗУ и тактовой частотой 1 МГц.

Программы AGC хранились в 74 КБ вязаной памяти: медной проволоки, вручную продетой на заводе через крошечные магнитные сердечники (провод, проходящий через сердечник, означал 1; не проходящий через него означал 0). Вязавших эту память женщин называли маленькими старушками («Little Old Ladies»), а саму память назвали LOL-памятью. Программу физически вплетали в оборудование. Кен Ширифф проанализировал её вплоть до отдельных вентилей, а проект Virtual AGC выполняет ПО в эмуляции; побайтное соответствие с дампами исходной вязаной памяти подтверждено.

Насколько я понимаю, формальную верификацию, проверку модели или статический анализ полётного кода не публиковали. Изучение было глубоким, но специфическим: код прочитали, эмулировали и верифицировали точность транскрипции.

Мы пошли по другому пути: воспользовались Allium для генерации поведенческой спецификации подсистемы гиростабилизатора (Inertial Measurement Unit, IMU) — платформы на основе гироскопа, сообщающей космическому аппарату, куда он направлен. Спецификация моделирует жизненный цикл каждого общего ресурса: когда он запрашивается, когда должен быть освобождён и на каких путях исполнения кода.

Это позволило выявить баг, упущенный при чтении и эмуляции.

Потеря ссылки

AGC управляет IMU при помощи блокировки общего ресурса под названием LGYRO. Когда компьютеру нужно подать управляющий момент на гироскопы (чтобы скорректировать дрейф платформы или выполнить выравнивание по звёздам), он в начале блокирует LGYRO и освобождает его после подачи момента на все три оси. Блокирование предотвращает конфликты двух подпрограмм за оборудование гироскопа.

Блокировка получается на пути внутрь и освобождается на пути наружу. Но есть и третья возможность, при которой блокировка не освобождается.

Caging (останов) — экстренная мера: физическая фиксация, блокирующая карданы IMU для защиты гироскопов от повреждения. Экипаж может привести её в действие при помощи переключателя с предохранителем на кокпите.

Когда подача момента завершается штатно, подпрограмма выполняет выход через STRTGYR2, а блокировка LGYRO снимается. Если выполнен останов IMU, когда происходит подача момента, то код выполняет выход через подпрограмму BADEND, не снимающую блокировку. В ней не хватает двух команд:

        CAF  ZERO
        TS   LGYRO

Четыре байта.

Когда LGYRO застревает, каждая последующая попытка подачи момента на гироскопы наталкивается на установленную блокировку, уходит в сон до сигнала пробуждения, который не приходит никогда, и повисает. Тонкое выравнивание, компенсация дрейфа и ручная подача момента гироскопа заблокированы.

21 июля 1969 года, когда Нил Армстронг и Базз Олдрин гуляли по поверхности Луны, Майкл Коллинз в одиночку находился на орбите в командном модуле Колумбия. Каждые два часа он пропадал из радиоконтакта с Землёй за Луной. «Сейчас я один, по-настоящему один, абсолютно изолирован от всей известной жизни. Если бы мы считали, то счёт был бы три миллиарда плюс две на другой стороне Луны, и один плюс Бог знает сколько на этой стороне», — писал он в книге Carrying the Fire.

На каждом проходе он запускал программу 52 — выравнивание с помощью астровизирования, поворачивающее платформу наведения в нужном направлении. Если платформа дрейфовала, то импульс двигателя для возврата его домой был бы направлен не туда.

Радиомолчание

Расскажем о том, как бы мог проявиться баг.

Коллинз только что завершил астровизирование (наблюдение за звёздами при помощи астровизира) на оптической станции в нижнем отсеке оборудования и ввёл окончательные команды. Компьютер подаёт момент на гироскоп для коррекции по всем трём осям.

Коллинз возвращается к главной панели тесного кокпита, двигаясь мимо переключателя останова, защищённого крышкой. Он задевает локтем крышку и нажимает переключатель. Код обрабатывает всё правильно: подпрограмма CAGETEST распознаёт останов, прекращает подачу момента и выполняет выход. Программа P52 завершается сбоем, и астронавт понимает его причину: останов прервал корректировку. Он снимает останов IMU и возвращается на оптическую станцию для повторной настройки.

Он запускает новую P52. Программа зависает.

Никаких аварийных сигналов, никаких загорающихся индикаторов. DSKY (дисплей и клавиатура, единственный способ взаимодействия с компьютером) принимает ввод, но ничего не делает. Коллинз пробует V41 — ручную подачу момента гироскопа. Тот же результат. Всё остальное в компьютере работает. Не отвечают лишь операции с гироскопом.

Первый сбой выглядел нормально: событие останова при выравнивании, способ восстановления известен. Второй не даёт никаких подсказок о причинах. Астронавт обучен реагировать на случайный останов его отключением и повторным выравниванием. Коллинза учили перезапускать компьютер, но ничто в сбое не говорит о необходимости этой процедуры. Команды принимаются, всё остальное работает. Это походит на отказ оборудования, а не на застрявший останов.

«Последние полгода я втайне испытывал ужас из-за того, что могу оставить их на Луне и вернуться на Землю один», — писал в рандеву Коллинз. Умершая на обратной стороне Луны система гиростабилизатора, когда Армстронг и Олдрин на поверхности ждут импульса рандеву, зависящего от нерегулируемой платформы — это именно такой сценарий.

Аппаратный перезапуск решил бы проблему. Однако аварийные тревоги 1202 во время спуска были и так достаточно стрессовыми, даже на связи с ЦУП и Стивом Бейлсом, принимающем решение о прекращении или продолжении миссии.

За Луной, в одиночестве, с компьютером, только принимающим команды и никак не реагирующим, Коллинз вынужден бы был принимать это решение самостоятельно.

Известные ориентиры

Маргарет Гамильтон (в качестве «матери вязаной памяти» LUMINARY) утверждала окончательные полётные программы перед их связыванием в память. Её команда из MIT Instrumentation Laboratory придумала концепции, которые мы сегодня считаем чем-то естественным: планирование с приоритетами, асинхронную многозадачность, защиту перезапуском и программное восстановление от ошибок. Даже термин «software engineering» придумала она.

Планирование с приоритетами спасло прилунение Аполлона-11, когда при спуске сработали аварийные тревоги 1202: под нагрузкой низкоприоритетные задачи опускались вниз точно так, как это было спроектировано. Большинство современных систем не сможет столь же хорошо справляться с перегрузками.

Самыми серьёзными всплывшими багами оказались ошибки спецификации, а не кодинга. Дон Эйлс, писавший код управления посадкой, задокументировал многие из них. Например, в ICD радара рандеву было указано, что два 800-герцовых источника питания будут фиксированы по частоте, но ничего не сказано о фазовой синхронизации. Получившийся фазовый дрейф привёл к вибрациям антенны, генерирующим приблизительно 6,4 тысячи ложных прерываний в секунду на угол и занимавшим примерно 13% от мощности компьютера во время спуска Аполлона-11. Именно это стало первопричиной аварийных тревог 1202.

Этот дефект возник из-за похожих причин. BADEND — это подпрограмма завершения общего назначения, используемая всеми операциями смены режима IMU. Она сбрасывает MODECADR (регистр простоя), пробуждает спящие задачи и выполняет выход. Но LGYRO — это блокировка конкретно для гироскопа, получаемая только кодом импульсной подачи момента и освобождаемая только обычным путём завершения в STRTGYR2. Когда ошибочный путь проходит через BADEND, она корректно обрабатывает общие ресурсы, но не блокировку гироскопа.

Код AGC писался настолько защитным образом, что подобные скрытые сбои втихомолку устранялись бы логикой перезапуска, сбрасывающей LGYRO как побочный эффект полной инициализации стираемой памяти. Любой тест, который бы вызвал перезапуск после бага, без проблем выполнил бы восстановление системы.

Защитный кодинг скрыл проблему, но не устранил её. Событие останова без последующего перезапуска всё равно оставляет гироскопы заблокированными. Коллинз бы никак не мог выровнять платформу наведения, и никакая диагностика не указала бы на причину.

Наблюдение за звёздами

Мы обнаружили этот дефект благодаря созданию поведенческой спецификации подсистемы IMU при помощи Allium — ИИ-нативного языка поведенческих спецификаций. Спецификация моделирует каждый общий ресурс как сущность с жизненным циклом: получение, удерживание, освобождение.

Сущность IMU объявляет поле gyros_busy, моделирующее LGYRO. Им управляют два правила:

rule GyroTorque {
    -- Отправляет команды импульсов моментов гироскопов. Резервирует гироскопы,
    -- включает питание и отправляет импульсы на каждую ось.
    когда: GyroTorque(команда: GyroTorqueCommand)

    требует:
        imu.mode != caged
        imu.gyros_busy = false

    проверяет:
        imu.gyros_busy = true
        GyroTorqueStarted()
}

rule GyroTorqueBusy {
    -- Гироскопы уже зарезервированы другой операцией подачи момента.
    -- Вызывающая сторона спит, пока не сбросится LGYRO.
    когда: GyroTorque(команда: GyroTorqueCommand)

    требует: imu.gyros_busy = true

    обеспечивает:
        JobSleep(job: calling_job())
}

GyroTorque требует gyros_busy = false и обеспечивает gyros_busy = true: получается блокировка. На каком-то из этапов каждого из последующих путей блокировка должна быть освобождена. Спецификация не показывает, в какой части кода происходит освобождение, но делает это требование явным: если gyros_busy принимает значение true, то что-то должно вернуть ей значение false.

Записав это требование, Claude оттрасировал каждый путь, выполняемый после присвоения gyros_busy значения true. Обычный путь завершения (STRTGYR2) сбрасывает его. Путь прерывания остановом (BADEND) этого не делает. Другой общий ресурс MODECADR корректно сбрасывается в BADEND: LGYRO там отсутствует.

Спецификация принудительно задаёт этот вопрос на каждом пути через код переключения режимов IMU. Ревьюер BADEND увидел бы корректный полный сброс для каждого ресурса, который должна обрабатывать BADEND.

Спецификация подходит к этому под другим углом: начиная с LGYRO и спрашивая, есть ли пути, на которых не удаётся её сбросить.

Тесты проверяют код так, как он написан; поведенческая спецификация задаёт вопросы о предназначении кода.

Созданная Allium спецификация моделирует жизненные циклы ресурсов по всем путям, в том числе и тем, которые никто не подумал тестировать. Посмотреть спецификации Allium и воссоздание бага можно на GitHub.

Корректировка курса

Команда Гамильтон освобождала ресурсы, загружая ноль в аккумулятор (CAF ZERO) и сохраняя его в регистр блокировки (TS LGYRO). Каждое освобождение выполнялось вручную программистом, который помнил все пути, способные достигнуть этой точки.

В современных языках предпринята попытка сделать утечки блокировок структурно невозможными: в Go есть defer, в Java есть try-with-resources, в Python есть with, система владения Rust делает утечки блокировок ошибкой компиляции.

Тем не менее, утечки блокировок всё ещё существуют. MITRE классифицирует этот паттерн, как CWE-772: «отсутствие освобождения ресурса после фактического срока жизни» и оценивает вероятность его эксплойта как высокую. Не все ресурсы управляются средой исполнения языка. Подключения к базам данных, распределённые блокировки, дескрипторы файлов в скриптах оболочки, инфраструктура, которая должна демонтироваться в нужном порядке: часто всё это остаётся ответственностью программиста. Каждый раз, когда программист отвечает за написание сброса, возникает вероятность того же самого бага.

Экипажи всех Аполлонов прибыли домой в безопасности. Однако подпрограммы переключения режимов IMU выполнялись в миссиях и в ПО командного модуля (COMANCHE), и в ПО лунного модуля (LUMINARY). Сбой ни разу не заметили и не устранили.

Примечание

В комментариях на Hacker News появился Майк Стюарт, руководивший восстановлением AGC, задокументированным на канале CuriousMarc, а также помогающий в администрировании VirtualAGC.

«Во-первых, должен сказать, что это реальный баг ПО AGC. Однако он не оставался незамеченным в течение всей программы. Его обнаружили на уровне 3 тестирования SATANCHE и поздней ветки разработки ПО командного модуля COMANCHE. Ему был присвоен номер аномалии L-1D-02, и он был устранён между Аполлоном-14 и Аполлоном-15. Сохранилось две известных копии отчёта об аномалии L-1D-02:

Описанное в статье исправление частично устраняет проблему, но, как отмечено в отчёте об аномалии, это ещё не всё. Вместо того, чтобы просто добавлять две команды для обнуления LGYRO, разработчики немного изменили структуру кода, а также заставили его пробуждать ожидающие задачи. Можете сравнить соответствующие части ПО лунного модуля Аполлона-14 и Аполлона-15:

Баг не проявился бы незаметно, как это описано в статье. Во-первых, LGYRO также обнуляется в STARTSB2, исполняемой через GOPROG2 при любом крупном изменении программы: https://github.com/virtualagc/virtualagc/blob/master/Luminary099/FRESH_START_AND_RESTART.agc#L570

Это означает, что переключение с любой программы на любую другую программу немедленно бы устранило проблему. Почти наверняка именно во многом из-за этого баг так долго оставался незамеченным. Исполнение BADEND при активной подаче момента — довольно редкое событие, избегаемое обычной подпрограммой. Описанный в статье сценарий не мог произойти, потому что процесс запуска P52 обнулил бы LGYRO.

Более того, в очень специфичных сценариях, когда баг мог бы сработать и сохраниться, он привёл бы к накоплению нескольких задач, пытающихся подать момент на гироскопы. Рано или поздно у компьютера бы закончилось место под новые задачи (аналогично тому, что произошло на Аполлоне-11), и сработали бы аварийные тревоги 31202 (аналог 1202 для Аполлона-12 и последующих проектов).

Так как проблема была найдена до полёта Аполлона-14, дополнительное описание возможных причин её возникновения и процедуры восстановления должны были добавить в Аннотацию программы Аполлона-14: https://www.ibiblio.org/apollo/Documents/LUM159_text.pdf#page=3.