Bug no documentado encontrado en el código de la computadora de guía del Apollo 11

 (juxt.pro)
2 puntos por GN⁺ 22 일 전 | 1 comentarios | Compartir por WhatsApp
  • Se descubrió un bug por omisión al liberar un bloqueo de recurso en el código de la Apollo Guidance Computer (AGC), considerado durante 57 años como casi perfecto
  • El equipo de JUXT analizó 130 mil líneas de ensamblador usando el lenguaje de especificación de IA Allium y Claude, e identificó un fallo que no aparecía con los métodos tradicionales de verificación
  • En la ruta de terminación anómala (BADEND) de la rutina de control del giroscopio, el bloqueo LGYRO no se libera, por lo que todas las funciones posteriores relacionadas con el giroscopio pueden detenerse
  • Si durante la misión real se hubiera presionado por error el interruptor Cage en órbita lunar, la alineación de Program 52 podría haberse interrumpido y Collins podría haberlo confundido con una falla de hardware
  • Este caso muestra que el análisis basado en especificaciones de comportamiento es una forma poderosa de encontrar nuevos defectos incluso en código antiguo

Falla potencial descubierta en la computadora de guía del Apollo 11

  • La Apollo Guidance Computer (AGC) es una de las bases de código más minuciosamente revisadas de la historia, y ha sido analizada por innumerables desarrolladores e investigadores
    • Sin embargo, se confirmó en el código de control del giroscopio un bug por omisión de liberación de bloqueo de recurso que no fue detectado durante 57 años
    • El problema consiste en que, en una ruta de error, el bloqueo no se libera y la función de realineación de la plataforma de guía queda deshabilitada
  • El equipo de JUXT usó el lenguaje de especificación basado en IA Allium y Claude para convertir 130 mil líneas de ensamblador de la AGC en 12,500 líneas de especificaciones de comportamiento
    • Extrajeron directamente del código las especificaciones para modelar todas las rutas de adquisición y liberación de recursos
    • En ese proceso apareció un defecto que no se había revelado con lectura de código ni emulación

Estructura del código y enfoque de análisis

  • El código fuente de la AGC se publicó en 2003, cuando Ron Burkey y voluntarios transcribieron manualmente los listados impresos del MIT Instrumentation Laboratory
    • En 2016 se publicó el repositorio de GitHub de Chris Garry, lo que permitió a desarrolladores de todo el mundo estudiar el código ensamblador de una máquina con 2 KB de RAM y CPU de 1 MHz
  • El programa se almacenaba en 74 KB de core rope memory, donde cables de cobre se tejían manualmente a través de núcleos magnéticos para representar 1 y 0
    • Las técnicas que realizaban ese trabajo eran conocidas como “Little Old Ladies”, y la memoria recibió el nombre de LOL memory
  • Hasta ahora no había registros de verificación formal, model checking ni análisis estático aplicados a la AGC
    • La mayor parte de la verificación se había concentrado en lectura de código, emulación y comprobación de la exactitud de la transcripción
  • JUXT escribió en Allium la especificación de comportamiento del subsistema IMU (Inertial Measurement Unit)
    • Al modelar los momentos de adquisición y liberación de cada recurso compartido, pudieron identificar el defecto

Omisión del desbloqueo en la rutina de control del giroscopio

  • La AGC gestionaba la IMU con un bloqueo compartido llamado LGYRO
    • Al aplicar torque al giroscopio adquiría el bloqueo, y lo liberaba cuando terminaban los tres ejes
    • Esto impedía que dos rutinas manipularan el hardware al mismo tiempo
  • Sin embargo, en la ruta de terminación anómala el bloqueo no se libera
    • En la salida normal, la rutina STRTGYR2 libera LGYRO, pero si ocurre “Caging” (bloqueo físico para proteger el giroscopio), el flujo pasa a la rutina BADEND
    • En BADEND faltan dos instrucciones, CAF ZERO y TS LGYRO (4 bytes en total), por lo que el bloqueo permanece activo
  • Si LGYRO no se libera, todas las rutinas posteriores de torque del giroscopio quedan detenidas esperando el bloqueo
    • Se interrumpen todas las funciones relacionadas con el giroscopio, como la alineación fina, la corrección de deriva y el torque manual

Impacto potencial en la cara oculta de la Luna

  • El 21 de julio de 1969, Michael Collins ejecutaba periódicamente en órbita lunar Program 52 (programa de alineación por observación estelar)
    • Si la plataforma derivaba, existía el riesgo de que la dirección del motor de regreso quedara incorrecta
  • Si durante una maniobra de torque se hubiera presionado por error el interruptor Cage y el sistema hubiera caído en la ruta BADEND, es posible que LGYRO no se hubiera liberado y que todos los P52 posteriores quedaran bloqueados
    • El DSKY (pantalla y teclado) seguiría aceptando entradas, pero sin responder
    • Como otras funciones seguirían operando normalmente, Collins podría haberlo interpretado como una falla de hardware
  • Un reinicio (hard reset) habría resuelto el problema, pero por la experiencia con la alarma 1202 durante el alunizaje, no habría sido fácil decidir un reinicio inmediato

Diseño defensivo del sistema existente y sus límites

  • El equipo del MIT liderado por Margaret Hamilton introdujo conceptos fundamentales de la ingeniería de software moderna, como planificación por prioridades, multitarea asíncrona y protección ante reinicios
    • Gracias a ese diseño fue posible aterrizar incluso durante la alarma 1202
  • La mayoría de los defectos importantes eran errores de especificación, y hubo casos documentados por Don Eyles en los que la falta de sincronización de fase entre componentes de hardware aumentó la carga del CPU
  • Este defecto tiene una estructura similar
    • BADEND es una rutina general de terminación para cambios de modo de la IMU, y aunque libera recursos comunes como MODECADR, no maneja LGYRO
    • Como la lógica de reinicio inicializa LGYRO, el problema se recuperaba sin inconvenientes durante las pruebas y por eso quedó oculto
  • Pero en una situación real sin reinicio, el giroscopio podría haber quedado bloqueado de forma permanente

Cómo se descubrió el defecto con Allium

  • La especificación de Allium modela el ciclo de vida (lifecycle) de cada recurso
    • El campo gyros_busy representa LGYRO, la regla GyroTorque define la adquisición del bloqueo y la regla GyroTorqueBusy define el estado de espera cuando el bloqueo ya está tomado
  • La especificación establece la obligación de que “si el bloqueo pasa a true, necesariamente debe volver a false”
    • Después de rastrear todas las rutas, Claude determinó que en la ruta normal (STRTGYR2) se libera, pero en la ruta de error (BADEND) esa liberación falta
  • El enfoque basado en especificaciones no verifica qué hace el código, sino qué debería hacer
    • Las pruebas comprueban el comportamiento actual del código, mientras que las especificaciones validan el comportamiento previsto
  • La especificación en Allium y el código para reproducir el bug se publicaron en GitHub

Implicaciones modernas y lecciones

  • En ese momento, los programadores tenían que liberar manualmente el bloqueo con las instrucciones CAF ZERO y TS LGYRO
    • Debían recordar todas las rutas e insertar manualmente el código de liberación
  • Los lenguajes modernos previenen estructuralmente este tipo de problemas de liberación de recursos
    • Funciones como defer de Go, try-with-resources de Java, with de Python y el sistema de ownership de Rust garantizan la liberación automática
  • Aun así, los defectos del tipo CWE-772 (omisión de liberación de recursos) siguen existiendo
    • Las conexiones a bases de datos, bloqueos distribuidos, file handles y el orden de apagado de infraestructura siguen dependiendo de la responsabilidad del programador
  • Todas las misiones Apollo regresaron con éxito, pero este defecto siguió presente sin corregirse también en el software COMANCHE (módulo de mando) y LUMINARY (módulo lunar)
  • El defecto, oculto durante 57 años, muestra la importancia del análisis basado en especificaciones de comportamiento

Lecturas relacionadas

1 comentarios

 
GN⁺ 22 일 전
Comentarios en Hacker News

  • Soy Mike Stewart, dirigí el proyecto de restauración del AGC en el canal CuriousMarc y soy coadministrador de VirtualAGC.
    El bug mencionado esta vez fue un defecto real del software del AGC. Pero no se dejó abandonado durante toda la vida del programa. Se descubrió durante la prueba de etapa 3 de SATANCHE, se registró como L-1D-02 y se corrigió entre Apollo 14 y 15.
    Los informes relacionados pueden verse en documento 1 de ibiblio y documento 2.
    La corrección no fue simplemente agregar dos líneas para poner LGYRO en 0, sino que también incluyó una reestructuración de la lógica del código y la lógica para despertar trabajos en espera. Si comparan el código de Apollo 14 y 15 (código de Apollo 14, código de Apollo 15), pueden ver la diferencia.
    No es un bug que ocurra silenciosamente como se describe en el artículo. LGYRO también se inicializa en STARTSB2, que se ejecuta cada vez que hay un cambio de programa y resuelve el problema automáticamente. Por eso, en la práctica, solo ocurría rara vez al realizar una operación de torque durante BADEND.
    Si el bug persistía, se acumulaban varios trabajos y eventualmente provocaba el error 31202 (la versión posterior del 1202). Este problema fue detectado antes del vuelo de Apollo 14 y se añadió un procedimiento de recuperación en Apollo 14 Program Notes.
    Además, aunque se dice que Ken Shirriff hizo el análisis a nivel de compuertas, en realidad yo hice la mayor parte.
    Virtual AGC solo ha completado la verificación de coincidencia byte por byte con volcados originales de core rope para algunos programas, y todavía no es posible para el programa completo. La mayor parte del código fuente fue restaurada a partir de impresos o checksums.
    Margaret Hamilton fue la ‘rope mother’ de Comanche (software del módulo de mando), y Luminary (módulo lunar) estuvo a cargo de Jim Kernan. Esto puede confirmarse en el organigrama de 1969.
    En el momento de la alarma 1202, el AGC no estaba diseñado para eliminar trabajos de baja prioridad. Al contrario, la guía de aterrizaje era la tarea de prioridad más baja, y el control de antena o la actualización de pantalla tenían mayor prioridad. Este documento resume la prioridad de cada tarea.
    Por último, en pruebas reales de hardware se confirmó que la causa de la alarma 1202 no fue una diferencia de fase, sino una diferencia de voltaje (28V vs 15V). El video del experimento relacionado puede verse en este enlace de YouTube.

    • Estaba esperando tu comentario. Gracias por compartir unos detalles históricos realmente asombrosos.
    • La portada ya pasó a otro tema, pero esto es información realmente valiosísima. Gracias por tomarte el tiempo.

  • Si te interesa el Apollo AGC, de verdad recomiendo ver el canal de YouTube CuriousMarc. Un equipo técnicamente excelente documenta el proceso de restaurar y analizar varias partes del AGC.
    Una parte especialmente interesante es la reinterpretación de la infame alarma 1202. Normalmente se la presenta como un error de sensor que podía ignorarse, pero en realidad, bajo ciertas condiciones, pudo haber sido muy crítico.

    • Entonces podría decirse que hoy sería más difícil o más fácil intentar el mismo alunizaje otra vez. Sabemos muchos más modos de falla que en ese momento.
    • Lo “explicado para el público” y lo “realmente comprendido” no son lo mismo. Hay muchas explicaciones simplificadas, pero entre especialistas es un fenómeno bien entendido desde hace tiempo.
    • La discusión del equipo de CuriousMarc sobre la restauración del AGC también sigue en este hilo.

  • Mi fragmento de código favorito es este.

    TC  BANKCALL  # TEMPORARY, I HOPE HOPE HOPE
CADR STOPRATE  # TEMPORARY, I HOPE HOPE HOPE
TC  DOWNFLAG  # PERMIT X-AXIS OVERRIDE

    Enlace de GitHub

    • Este código también se menciona en The Codeless Code.
    • Aquí CADR no tiene relación con la función cadr de Lisp.
    • ¿Hay alguien que pueda explicar por qué este código es gracioso?
    • Recuerdo haber visto antes un poema sobre este código en XKCD, aunque quizá lo estoy confundiendo.

  • Me pregunto si alguna vez se verificó que este bug realmente exista. La IA es buena para este tipo de análisis exploratorio, pero sigue teniendo una tasa alta de falsos positivos.
    Dependiendo del contexto, puede ser importante o no. También hay muchos bugs que la IA no encuentra.
    No tengo la experiencia para validarlo por mi cuenta, pero me parece muy interesante.

    • En realidad ni siquiera está claro que la IA haya encontrado el bug. Solo dice que “lo modelaron en un lenguaje nativo de IA”.
      Aun así, la explicación de la adquisición del lock y del escenario de falla resultó bastante convincente.

  • Es interesante que hayan encontrado un bug real. Pero la puesta en escena dramática del texto está cerca de la ficción.
    Cosas como golpear un switch con el codo o exagerar un problema que podría resolverse con un reset. Eso hizo el texto más sensacionalista, pero menos confiable. Además, la prosa parece escrita por IA, lo que molesta más.

    • Claro, el switch tenía una cubierta de protección.
      Pero para explicarle a un lector general un bug sutil, hace falta cierto nivel de narrativa. Si es demasiado técnico, pierde el interés; si es demasiado dramático, los expertos lo critican. Me parece difícil encontrar ese equilibrio.

  • Ejecuté directamente el código de reproducción (repro) incluido en el artículo.
    Enlace de GitHub
    Sí corre, pero la Phase 5 (demostración del deadlock) es una salida falsa por completo. No ejecuta el emulador real, solo imprime el resultado esperado.
    Así que subí este PR que corregí yo mismo, para que de verdad funcionara en el emulador y para verificar también si el parche de dos líneas resolvía el bug.

    • Veo este tipo de “código de IA” muy seguido. Imita el desarrollo guiado por pruebas, pero en realidad entrega código falso que solo pasa las pruebas.
      El código generado por IA tiende a detenerse con un “¡ahora sí está perfecto!”, y la gente que le cree lo publica tal cual. Ese es el verdadero problema.

  • El texto en sí es interesante, pero tiene una sensación artificial, como escrita por un LLM.

    • A mí no me dio nada de impresión de LLM. Me pareció más bien estilo artículo científico.
    • Juxt lleva tiempo escribiendo textos excelentes y tiene suficiente experiencia. Por eso veo poco probable que este texto haya sido escrito por IA.
    • Como referencia, según el análisis de Pangram, este texto fue clasificado como escrito por un humano.
    • Pero uno de los otros textos de Juxt sí indica explícitamente que fue escrito por Claude. Lo dice en el último párrafo de ese artículo.
    • Además, la parte sobre Rust y los locks no coincide con los hechos. Lo señalan en este comentario.

  • Que incluso el software que llevó seres humanos a la Luna con solo 4 KB de memoria todavía tenga bugs no descubiertos muestra que la complejidad puede esconderse incluso en código pequeño.

    • Cuanta menos memoria hay, más débil es la correlación entre longitud del código y tasa de bugs. Más bien, al intentar comprimir la complejidad, aumentan los bugs.
    • Eso suena simplemente como un lugar común vacío.

  • La expresión “derivaron la especificación a partir del código” es incorrecta. Haría falta volver a revisar qué significa specification.

    • En realidad eso solo significa ingeniería inversa.

  • Tanto el artículo como el repositorio son trabajos descuidados (sloppy).
    Si miras el repositorio, se supone que es una “reproducción”, pero no ejecuta el bug real; simplemente enumera mensajes de salida del tipo “esto pasaría”.