Un bug non documenté découvert dans le code de l’ordinateur de guidage d’Apollo 11

• Un bug d’omission de libération de verrou de ressource a été découvert dans le code de l’Apollo Guidance Computer (AGC), considéré depuis 57 ans comme presque parfait
• L’équipe JUXT a analysé 130�0 lignes d’assembleur à l’aide du langage de spécification IA Allium et de Claude, et a identifié une défaillance que les méthodes de vérification classiques n’avaient pas mise en évidence
• Dans le chemin de terminaison anormale (BADEND) de la routine de contrôle des gyroscopes, le verrou LGYRO n’est pas libéré, ce qui peut bloquer ensuite toutes les fonctions liées aux gyroscopes
• Si, pendant la mission réelle, l’interrupteur Cage avait été actionné par erreur en orbite lunaire, l’alignement Program 52 aurait pu être interrompu et Collins aurait pu le prendre pour une panne matérielle
• Ce cas montre que l’analyse fondée sur des spécifications comportementales est une méthode puissante pour découvrir de nouveaux défauts, même dans du code ancien

---

Un défaut potentiel découvert dans l’ordinateur de guidage d’Apollo 11

• L’Apollo Guidance Computer (AGC) est l’une des bases de code les plus minutieusement examinées de l’histoire, analysée par d’innombrables développeurs et chercheurs
  • Pourtant, un bug de verrouillage de ressource non libéré passé inaperçu pendant 57 ans a été confirmé dans le code de contrôle des gyroscopes
  • Sur un chemin d’erreur, le verrou n’est pas libéré, ce qui peut désactiver la fonction de réalignement de la plateforme de guidage
• L’équipe JUXT a utilisé le langage de spécification fondé sur l’IA Allium et Claude pour transformer 130�0 lignes d’assembleur AGC en 1200 lignes de spécifications comportementales
  • Les spécifications ont été extraites directement du code afin de modéliser tous les chemins d’acquisition et de libération des ressources
  • Ce processus a mis au jour un défaut qui n’apparaissait pas avec la simple lecture du code ni avec l’émulation

Structure du code et approche d’analyse

• Le code source de l’AGC a été rendu public en 2003, lorsque Ron Burkey et des bénévoles ont retranscrit manuellement les imprimés du MIT Instrumentation Laboratory
  • En 2016, le dépôt GitHub de Chris Garry a été publié, permettant à des développeurs du monde entier d’examiner ce code assembleur pour 2 KB de RAM et un CPU à 1 MHz
• Le programme était stocké dans 74 KB de core rope memory, où des fils de cuivre étaient tissés à la main à travers des tores magnétiques pour représenter les 1 et les 0
  • Les techniciennes qui effectuaient ce travail étaient surnommées « Little Old Ladies », et cette mémoire était appelée LOL memory
• Jusqu’ici, il n’existait aucun historique de vérification formelle, model checking ou analyse statique appliqué à l’AGC
  • L’essentiel de la vérification s’était concentré sur la lecture du code, l’émulation et la validation de la fidélité de la transcription
• JUXT a rédigé en Allium une spécification comportementale du sous-système IMU (Inertial Measurement Unit)
  • En modélisant le moment d’acquisition et de libération de chaque ressource partagée, l’équipe a pu identifier le défaut

Omission de libération du verrou dans la routine de contrôle des gyroscopes

• L’AGC gère l’IMU à l’aide d’un verrou partagé nommé LGYRO
  • Lorsqu’il applique un couple aux gyroscopes, il acquiert ce verrou, puis le libère une fois les trois axes terminés
  • Cela empêche que deux routines manipulent le matériel en même temps
• Cependant, dans le chemin de terminaison anormale, le verrou n’est pas libéré
  • En cas de terminaison normale, la routine STRTGYR2 libère LGYRO, mais si un « Caging » (verrouillage physique de protection du gyroscope) se produit, l’exécution bifurque vers la routine BADEND
  • Dans BADEND, il manque les deux instructions CAF ZERO et TS LGYRO (4 octets au total), ce qui laisse le verrou actif
• Si LGYRO n’est pas libéré, toutes les routines ultérieures de couple gyroscopique se bloquent en attente du verrou
  • L’alignement fin, la correction de dérive, le couple manuel et toutes les autres fonctions liées aux gyroscopes s’arrêtent alors

Impact potentiel derrière la Lune

• Le 21 juillet 1969, Michael Collins exécutait périodiquement Program 52 (programme d’alignement par observation d’étoiles) en orbite lunaire
  • Si la plateforme dérivait, l’orientation du moteur de retour risquait d’être incorrecte
• Si, pendant une opération de couple, l’interrupteur Cage avait été actionné par erreur, forçant le passage dans le chemin BADEND, LGYRO aurait pu ne jamais être libéré et tous les P52 suivants auraient pu se bloquer
  • Le DSKY (affichage-clavier) aurait accepté les entrées sans réagir
  • Comme les autres fonctions continuaient à fonctionner normalement, Collins aurait pu l’interpréter comme une panne matérielle
• Un redémarrage (hard reset) aurait résolu le problème, mais après l’expérience de l’alarme 1202 durant l’alunissage, il aurait été difficile de décider immédiatement d’un reset

Conception défensive du système et ses limites

• L’équipe du MIT dirigée par Margaret Hamilton a introduit des concepts fondateurs du génie logiciel moderne, comme l’ordonnancement par priorité, le multitâche asynchrone et la protection au redémarrage
  • C’est grâce à cette conception que l’alunissage a pu se poursuivre malgré les alarmes 1202
• La plupart des défauts majeurs relevaient d’erreurs de spécification et, comme l’a documenté Don Eyles, l’absence de synchronisation de phase entre matériels avait déjà entraîné une hausse de charge CPU
• Ce défaut suit une structure comparable
  • BADEND est une routine de fin générale pour les changements de mode de l’IMU ; elle libère des ressources communes comme MODECADR, mais ne traite pas LGYRO
  • Comme la logique de redémarrage réinitialise LGYRO, le système récupérait correctement pendant les tests, ce qui a masqué le défaut
• En revanche, dans une situation réelle sans redémarrage, le gyroscope aurait pu rester bloqué de façon permanente

Comment le défaut a été découvert avec Allium

• Les spécifications Allium modélisent le cycle de vie (lifecycle) de chaque ressource
  • Le champ gyros_busy représente LGYRO, la règle GyroTorque définit l’acquisition du verrou, et la règle GyroTorqueBusy définit l’attente lorsque le verrou est déjà pris
• La spécification exprime l’obligation suivante : « si le verrou passe à true, il doit obligatoirement revenir à false »
  • En retraçant tous les chemins, Claude a constaté que la libération a bien lieu sur le chemin normal (STRTGYR2), mais manque sur le chemin d’erreur (BADEND)
• L’approche fondée sur les spécifications vérifie non pas ce que le code fait, mais ce qu’il devrait faire
  • Les tests confirment le comportement actuel du code, tandis que les spécifications valident le comportement intentionnel
• Les spécifications Allium et le code de reproduction du bug ont été publiés sur GitHub

Implications modernes et enseignements

• À l’époque, les programmeurs devaient libérer manuellement les verrous à l’aide des instructions CAF ZERO et TS LGYRO
  • Ils devaient mémoriser tous les chemins d’exécution et y insérer eux-mêmes le code de libération
• Les langages modernes préviennent structurellement ce type de problème de fuite de ressource
  • Le defer de Go, le try-with-resources de Java, le with de Python ou le système de propriété de Rust garantissent une libération automatique
• Malgré cela, les défauts de type CWE-772 (Missing Release of Resource after Effective Lifetime) existent toujours
  • Connexions à des bases de données, verrous distribués, descripteurs de fichiers, ordre d’arrêt d’infrastructures : autant de cas qui restent à la charge des programmeurs
• Toutes les missions Apollo sont revenues avec succès, mais ce défaut a ensuite été recopié tel quel dans les logiciels COMANCHE (module de commande) et LUMINARY (module lunaire), sans être corrigé
• Ce défaut resté caché pendant 57 ans illustre l’importance de l’analyse fondée sur des spécifications comportementales

[GN⁺]

Commentaires sur Hacker News

• Je suis Mike Stewart, j’ai dirigé le projet de restauration de l’AGC sur la chaîne CuriousMarc et je suis co-administrateur de VirtualAGC
  Le bug mentionné cette fois-ci était bien un défaut réel du logiciel AGC. Mais il n’est pas resté en l’état pendant toute la durée du programme. Il a été découvert pendant les tests de phase 3 de SATANCHE, consigné sous la référence L-1D-02, puis corrigé entre Apollo 14 et 15
  Les rapports correspondants sont consultables dans ibiblio document 1 et document 2
  La correction n’a pas consisté simplement à ajouter deux lignes pour remettre LGYRO à 0, elle incluait aussi une réorganisation de la structure du code et une logique pour réveiller les tâches en attente. En comparant le code d’Apollo 14 et d’Apollo 15 (code Apollo 14, code Apollo 15), on peut voir la différence
  Ce n’est pas un bug qui se produit silencieusement comme l’article le décrit. LGYRO est aussi initialisé dans STARTSB2, qui s’exécute à chaque changement de programme et résout automatiquement le problème. En pratique, cela ne se produisait donc que rarement, uniquement lors d’une manœuvre de couple pendant BADEND
  Si le bug persiste, plusieurs tâches s’accumulent et finissent par provoquer une erreur 31202, la version ultérieure du 1202. Le problème a été identifié avant le vol d’Apollo 14 et une procédure de récupération a été ajoutée dans les Apollo 14 Program Notes
  Par ailleurs, même si Ken Shirriff est crédité pour l’analyse au niveau des portes logiques, c’est en réalité moi qui en ai fait la plus grande partie
  Virtual AGC n’a pu vérifier la correspondance octet par octet avec les dumps originaux de core rope que pour certains programmes, pas pour l’ensemble. La majeure partie des sources a été restaurée à partir d’imprimés ou de checksums
  Margaret Hamilton était la « rope mother » de Comanche, le logiciel du module de commande, tandis que Luminary, le module lunaire, relevait de Jim Kernan. On peut le vérifier dans l’organigramme de 1969
  Au moment de l’alarme 1202, l’AGC n’avait pas été conçu pour supprimer les tâches de faible priorité. En réalité, le guidage d’atterrissage était la tâche de plus faible priorité, alors que le contrôle d’antenne ou la mise à jour de l’affichage avaient une priorité supérieure. Ce document récapitule les priorités des différentes tâches
  Enfin, des tests sur le matériel réel ont confirmé que la cause de l’alarme 1202 n’était pas un décalage de phase, mais une différence de tension (28V vs 15V). Une vidéo de l’expérience est disponible via ce lien YouTube

  • J’attendais votre commentaire. Merci d’avoir partagé des détails historiques vraiment remarquables
  • La page d’accueil est déjà passée à autre chose, mais ces informations sont un vrai trésor. Merci d’avoir pris le temps

• Si l’Apollo AGC vous intéresse, je recommande vivement la chaîne YouTube CuriousMarc. Une équipe techniquement brillante y documente la restauration et l’analyse de plusieurs composants de l’AGC
  Le point le plus fascinant est sans doute la réinterprétation de la fameuse alarme 1202. On la présente généralement comme une simple erreur capteur sans conséquence, alors qu’elle aurait en réalité pu être très grave dans certaines conditions

  • On peut donc considérer qu’aujourd’hui, retenter le même atterrissage serait soit plus difficile, soit plus facile. Nous connaissons bien davantage de modes de défaillance qu’à l’époque
  • Ce qui est « expliqué au grand public » et ce qui est « réellement compris » sont deux choses différentes. Il existe beaucoup d’explications simplifiées, mais le phénomène est déjà bien compris chez les spécialistes
  • La discussion de l’équipe CuriousMarc sur la restauration de l’AGC se poursuit aussi dans ce fil

• Mon extrait de code préféré est celui-ci

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

  Lien GitHub

  • Ce code est aussi mentionné dans The Codeless Code
  • Ici, CADR n’a rien à voir avec la fonction cadr de Lisp
  • Quelqu’un peut expliquer pourquoi ce code est drôle ?
  • Je crois me souvenir avoir vu autrefois un poème XKCD à propos de ce code, mais je me trompe peut-être

• Je me demande si quelqu’un a vérifié que ce bug existe vraiment. L’IA est forte pour ce type d’analyse exploratoire, mais elle a encore un taux de faux positifs élevé
  Selon le contexte, cela peut être important… ou non. Et il y a aussi beaucoup de bugs que l’IA ne détecte pas
  Je n’ai pas l’expertise pour le vérifier moi-même, mais je trouve ça très intéressant

  • En fait, il n’est même pas clair que ce soit l’IA qui ait trouvé le bug. Le texte dit seulement que cela a été « modélisé dans un langage natif pour l’IA »
    Cela dit, l’explication de la prise de verrou et du scénario d’échec était assez convaincante

• Le fait qu’ils aient trouvé un vrai bug est intéressant. Mais la mise en scène dramatique du texte relève presque de la fiction
  Par exemple avec l’idée d’actionner un interrupteur avec le coude, ou d’exagérer un problème qu’un reset permettrait de résoudre. Cela rend le texte plus sensationnaliste, mais moins crédible. En plus, le style fait penser à un texte écrit par une IA, ce qui est agaçant

  • Cela dit, c’était bien sûr un interrupteur avec capot de protection.
    Mais pour expliquer un bug subtil à un lectorat généraliste, il faut un minimum de storytelling. Si c’est trop technique, les gens décrochent ; si c’est trop dramatique, les experts critiquent. Je pense que trouver cet équilibre est difficile

• J’ai exécuté moi-même le code de reproduction (repro) inclus dans l’article
  Lien GitHub
  Ça s’exécute, mais la phase 5 (démonstration du deadlock) est une sortie entièrement factice. Elle n’exécute pas réellement l’émulateur et affiche seulement un résultat attendu
  J’ai donc soumis ma propre PR, pour corriger cela afin que ça fonctionne vraiment dans l’émulateur, et j’ai aussi vérifié que le patch de deux lignes résout bien le bug

  • Je vois souvent ce genre de « code IA ». Ça imite le test-driven development, mais en pratique ça produit surtout du faux code qui ne fait que passer les tests
    Le code généré par IA a tendance à s’arrêter en proclamant « c’est parfait maintenant ! », et des gens y croient puis le déploient tel quel. C’est ça, le vrai problème

• L’article lui-même est intéressant, mais il dégage une impression artificielle, comme s’il avait été écrit par un LLM

  • Moi, ça ne m’a donné aucune impression de LLM. Ça ressemble plutôt à un style de publication scientifique
  • Juxt écrit d’excellents articles depuis longtemps et a toute l’expertise nécessaire. Donc je pense qu’il est peu probable que ce texte ait été rédigé par une IA
  • À titre d’info, selon l’analyse Pangram, ce texte est classé comme écrit par un humain
  • Cela dit, un autre article de Juxt précise explicitement qu’il a été écrit par Claude. C’est indiqué dans le dernier paragraphe de cet article
  • En outre, la partie sur Rust et les verrous est factuellement incorrecte. C’est signalé dans ce commentaire

• Le fait qu’un logiciel qui a envoyé des humains sur la Lune avec seulement 4 KB de mémoire puisse encore contenir des bugs non découverts montre bien que même un petit code peut cacher une vraie complexité

  • Moins il y a de mémoire, plus la corrélation entre longueur du code et taux de bugs est faible. Au contraire, vouloir compresser la complexité tend à augmenter le nombre de bugs
  • Ce genre de remarque sonne juste comme un lieu commun creux

• Dire qu’ils ont « dérivé une spécification à partir du code » est inexact. Il faudrait revoir ce que signifie vraiment le terme specification

  • En réalité, cela veut simplement dire rétro-ingénierie

• L’article comme le dépôt sont des résultats bâclés (sloppy)
  Quand on regarde le dépôt, la prétendue « reproduction » n’exécute pas réellement le bug et se contente d’aligner des instructions d’affichage disant « voilà ce qui se passerait »