Bogue non documenté découvert dans le code de l'ordinateur de guidage d'Apollo 11 grâce à l'IA et à un langage de spécification

Découvrir un bogue dans l'un des codes les plus examinés de l'histoire

Le code de l'ordinateur de guidage Apollo (AGC) est disponible publiquement depuis 2003, transcrit à partir de listings imprimés du MIT Instrumentation Laboratory. En 2016, le dépôt GitHub de Chris Garry est devenu viral, et des milliers de développeurs ont examiné ce code assembleur fonctionnant sur un matériel avec 2 Ko de RAM effaçable et une horloge à 1 MHz. Malgré cet examen minutieux, aucune vérification formelle, vérification de modèle ou analyse statique n'avait été publiée sur le code de vol jusqu'à présent.

Le bogue : une fuite de verrouillage de ressource dans le contrôle gyroscopique

Le bogue se trouve dans le sous-système de l'unité de mesure inertielle (IMU), qui gère la plateforme basée sur gyroscope qui indique au vaisseau spatial dans quelle direction il pointe. L'AGC gère l'IMU via un verrouillage de ressource partagée appelé LGYRO. Lorsque l'ordinateur doit appliquer un couple aux gyroscopes (pour corriger la dérive de la plateforme ou effectuer un alignement stellaire), il acquiert LGYRO au début et le libère lorsque les trois axes ont été mis en couple.

Le problème survient pendant le « caging » - une mesure d'urgence où une pince physique verrouille les cardans de l'IMU en place pour protéger les gyroscopes des dommages. Lorsque le couple se termine normalement, la routine sort via STRTGYR2 et le verrou LGYRO est effacé. Mais lorsque l'IMU est cagée pendant qu'un couple est en cours, le code sort via une routine appelée BADEND, qui n'efface pas le verrou.

Deux instructions manquent : CAF ZERO TS LGYRO - seulement quatre octets. Une fois que LGYRO est bloqué, chaque tentative ultérieure de mettre en couple les gyroscopes trouve le verrou maintenu, entre en veille en attendant un signal de réveil qui ne viendra jamais, et se bloque. Cela désactiverait l'alignement fin, la compensation de dérive et le couple gyroscopique manuel.

Comment il a été trouvé : IA et spécifications comportementales

Les chercheurs ont utilisé Claude et Allium, leur langage de spécification comportementale open-source, pour condenser 130 000 lignes d'assembleur AGC en 12 500 lignes de spécifications. La spécification modélise le cycle de vie de chaque ressource partagée : quand elle est acquise, quand elle doit être libérée, et sur quels chemins. Cette approche a révélé une faille que la lecture et l'émulation avaient manquée.

Les spécifications ont été dérivées du code lui-même, et le processus a directement signalé le défaut. Cela représente une approche différente des examens précédents, qui se concentraient sur la lecture du code, l'émulation du code et la vérification de la transcription.

Contexte historique et impact potentiel

Le 21 juillet 1969, alors que Neil Armstrong et Buzz Aldrin marchaient sur la surface lunaire, Michael Collins orbitait seul dans le module de commande Columbia. Toutes les deux heures, il disparaissait derrière la Lune, hors de tout contact radio avec la Terre. Pendant chaque passage, il exécutait le Programme 52, un alignement par visée stellaire qui maintenait la plateforme de guidage pointée dans la bonne direction. Si la plateforme dérivait, la poussée du moteur pour le ramener à la maison pointerait dans la mauvaise direction.

Le bogue aurait pu se manifester si Collins avait accidentellement déclenché l'interrupteur de cage pendant que l'ordinateur mettait en couple les gyroscopes. Le code aurait géré cela élégamment en détectant la cage, en abandonnant le couple et en sortant - mais l'alignement P52 échouerait, et la plateforme de guidage pourrait perdre sa référence.