Error no documentado encontrado en el código de la computadora de guía del Apolo 11 utilizando IA y lenguaje de especificación

Encontrando un error en una de las bases de código más examinadas de la historia

El código del Apollo Guidance Computer (AGC) ha estado disponible públicamente desde 2003, transcrito de listados impresos del MIT Instrumentation Laboratory. En 2016, el repositorio de GitHub de Chris Garry se volvió viral, y miles de desarrolladores han examinado este código ensamblador que se ejecuta en hardware con 2K de RAM borrable y un reloj de 1MHz. A pesar de este escrutinio, no se había publicado ninguna verificación formal, verificación de modelos o análisis estático contra el código de vuelo hasta ahora.

El error: Una fuga de bloqueo de recursos en el control del giroscopio

El error está en el subsistema de la Unidad de Medición Inercial (IMU), que gestiona la plataforma basada en giroscopios que le indica a la nave espacial hacia dónde apunta. El AGC gestiona la IMU a través de un bloqueo de recurso compartido llamado LGYRO. Cuando la computadora necesita aplicar torque a los giroscopios (para corregir la deriva de la plataforma o realizar alineación estelar), adquiere LGYRO al inicio y lo libera cuando los tres ejes han sido torquedos.

El problema ocurre durante el 'encajonamiento' (caging), una medida de emergencia donde una abrazadera física bloquea los cardanes de la IMU en su lugar para proteger los giroscopios de daños. Cuando el torque se completa normalmente, la rutina sale a través de STRTGYR2 y el bloqueo LGYRO se borra. Pero cuando la IMU está encajonada mientras un torque está en progreso, el código sale a través de una rutina llamada BADEND, que no borra el bloqueo.

Faltan dos instrucciones: CAF ZERO TS LGYRO - solo cuatro bytes. Una vez que LGYRO se atasca, cada intento posterior de aplicar torque a los giroscopios encuentra el bloqueo retenido, se duerme esperando una señal de activación que nunca llegará y se cuelga. Esto deshabilitaría la alineación fina, la compensación de deriva y el torque manual del giroscopio.

Cómo se encontró: IA y especificaciones de comportamiento

Los investigadores utilizaron Claude y Allium, su lenguaje de especificación de comportamiento de código abierto, para destilar 130,000 líneas de ensamblador del AGC en 12,500 líneas de especificaciones. La especificación modela el ciclo de vida de cada recurso compartido: cuándo se adquiere, cuándo debe liberarse y en qué rutas. Este enfoque reveló una falla que la lectura y emulación habían pasado por alto.

Las especificaciones se derivaron del código mismo, y el proceso señaló directamente al defecto. Esto representa un enfoque diferente del escrutinio anterior, que se centraba en leer el código, emular el código y verificar la transcripción.

Contexto histórico e impacto potencial

El 21 de julio de 1969, mientras Neil Armstrong y Buzz Aldrin caminaban sobre la superficie lunar, Michael Collins orbitaba solo en el Módulo de Comando Columbia. Cada dos horas desaparecía detrás de la Luna, fuera del contacto por radio con la Tierra. Durante cada pasada ejecutaba el Programa 52, una alineación de observación estelar que mantenía la plataforma de guía apuntando en la dirección correcta. Si la plataforma derivaba, la ignición del motor para traerlo a casa apuntaría en la dirección equivocada.

El error podría haberse manifestado si Collins activaba accidentalmente el interruptor de encajonamiento mientras la computadora estaba aplicando torque a los giroscopios. El código manejaría esto con gracia detectando el encajonamiento, abandonando el torque y saliendo, pero la alineación P52 fallaría, y la plataforma de guía podría perder su referencia.