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