Nicht dokumentierter Bug im Code des Apollo-11-Bordcomputers entdeckt

• Im Code des Apollo Guidance Computer (AGC), der seit 57 Jahren als nahezu perfekt galt, wurde ein Bug durch fehlende Freigabe einer Ressourcensperre entdeckt
• Das JUXT-Team analysierte 130.000 Zeilen Assembler mit der KI-Spezifikationssprache Allium und Claude und identifizierte dabei einen Fehler, der mit bisherigen Verifikationsmethoden nicht sichtbar war
• Im abnormalen Beendigungspfad (BADEND) der Gyro-Steuerroutine wird die LGYRO-Sperre nicht freigegeben, wodurch danach alle gyrobezogenen Funktionen anhalten können
• Wäre während der echten Mission im Mondorbit der Cage-Schalter versehentlich betätigt worden, hätte die Ausrichtung mit Program 52 abbrechen können, und Collins hätte dies möglicherweise als Hardwaredefekt fehlinterpretiert
• Der Fall zeigt, dass verhaltensspezifikationsbasierte Analyse auch in altem Code ein leistungsfähiger Weg ist, neue Fehler zu finden

---

Potenzieller Defekt im Bordcomputer von Apollo 11 entdeckt

• Der Apollo Guidance Computer (AGC) gilt als eine der am gründlichsten untersuchten Codebasen der Geschichte, die von zahllosen Entwicklern und Forschern analysiert wurde
  • Dennoch wurde im Gyro-Steuercode ein Bug durch fehlende Freigabe einer Ressourcensperre bestätigt, der 57 Jahre lang unentdeckt blieb
  • In einem Fehlerpfad wird die Sperre nicht freigegeben, wodurch die Neuausrichtungsfunktion der Führungsplattform deaktiviert werden kann
• Das JUXT-Team wandelte mit der KI-basierten Spezifikationssprache Allium und Claude 130.000 Zeilen AGC-Assembler in 12.500 Zeilen Verhaltensspezifikation um
  • Die Spezifikation wurde direkt aus dem Code extrahiert, um alle Pfade der Ressourcenbelegung und -freigabe zu modellieren
  • Dabei wurde ein Defekt sichtbar, der durch klassisches Codelesen oder Emulation nicht auffiel

Codestruktur und Analyseansatz

• Der AGC-Quellcode wurde 2003 veröffentlicht, nachdem Ron Burkey und Freiwillige die Druckausgaben des MIT Instrumentation Laboratory manuell übertragen hatten
  • 2016 machte Chris Garrys GitHub-Repository den Code allgemein zugänglich, woraufhin Entwickler weltweit den Assemblercode für 2 KB RAM und eine 1-MHz-CPU studierten
• Das Programm war in core rope memory mit 74 KB gespeichert, wobei Kupferdrähte von Hand durch magnetische Kerne geflochten wurden, um 1 und 0 darzustellen
  • Die Technikerinnen, die diese Arbeit ausführten, wurden als „Little Old Ladies“ bezeichnet, und der Speicher erhielt den Namen LOL memory
• Bislang gibt es keine dokumentierten Fälle von formaler Verifikation, Model Checking oder statischer Analyse des AGC
  • Die meisten Prüfungen konzentrierten sich auf das Lesen des Codes, Emulation und die Überprüfung der Transkriptionsgenauigkeit
• JUXT erstellte mit Allium eine Verhaltensspezifikation des IMU-Subsystems (Inertial Measurement Unit)
  • Dabei wurden die Zeitpunkte des Erwerbs und der Freigabe jeder gemeinsam genutzten Ressource modelliert, um Defekte zu identifizieren

Fehlende Sperrenfreigabe in der Gyro-Steuerroutine

• Der AGC verwaltet die IMU mit einer gemeinsam genutzten Sperre namens LGYRO
  • Beim Ansteuern der Gyroskope wird die Sperre gesetzt und erst nach Abschluss aller drei Achsen wieder freigegeben
  • So wird verhindert, dass zwei Routinen gleichzeitig dieselbe Hardware bedienen
• Im abnormalen Beendigungspfad wird die Sperre jedoch nicht freigegeben
  • Beim normalen Ende gibt die Routine STRTGYR2 LGYRO frei, tritt jedoch Caging auf — eine physische Sperre zum Schutz der Gyroskope — verzweigt der Ablauf in die Routine BADEND
  • In BADEND fehlen die zwei Befehle CAF ZERO und TS LGYRO (insgesamt 4 Byte), sodass die Sperre bestehen bleibt
• Wenn LGYRO nicht freigegeben wird, bleiben anschließend alle Gyro-Torque-Routinen wartend an der Sperre hängen
  • Feinausrichtung, Driftkorrektur, manuelles Torque und alle anderen gyrobezogenen Funktionen kommen zum Stillstand

Mögliche Auswirkungen auf der Mondrückseite

• Am 21. Juli 1969 führte Michael Collins im Mondorbit regelmäßig Program 52 aus, das Sternbeobachtungen zur Ausrichtung nutzte
  • Wenn die Plattform driftete, bestand die Gefahr, dass das Rückkehrtriebwerk falsch ausgerichtet war
• Wäre während eines Torque-Vorgangs versehentlich der Cage-Schalter betätigt worden und der Ablauf dadurch in den Pfad BADEND geraten, hätte LGYRO möglicherweise alle nachfolgenden P52-Läufe blockiert
  • Das DSKY (Display und Tastatur) hätte Eingaben angenommen, aber nicht reagiert
  • Da andere Funktionen normal weiterliefen, hätte Collins dies als Hardwaredefekt fehlinterpretieren können
• Ein Neustart (Hard Reset) hätte das Problem vermutlich behoben, doch aufgrund der Erfahrungen mit dem 1202-Alarm während der Mondlandung wäre eine sofortige Reset-Entscheidung nicht einfach gewesen

Defensive Architektur des bestehenden Systems und ihre Grenzen

• Das von Margaret Hamilton geleitete MIT-Team führte grundlegende Konzepte moderner Softwaretechnik ein, darunter Prioritätsscheduling, asynchrones Multitasking und Neustartschutz
  • Dieses Design ermöglichte es, trotz des 1202-Alarms weiter zu landen
• Die meisten schwerwiegenden Defekte waren Spezifikationsfehler; wie von Don Eyles dokumentiert, führte etwa fehlende Phasensynchronisation zwischen Hardwarekomponenten einmal zu erhöhter CPU-Last
• Der diesmalige Defekt hat eine ähnliche Struktur
  • BADEND ist eine allgemeine Abschlussroutine für IMU-Moduswechsel und gibt gemeinsame Ressourcen wie MODECADR frei, behandelt jedoch LGYRO nicht
  • Da die Neustartlogik LGYRO initialisiert, wurde der Fehler in Tests wieder bereinigt und blieb dadurch verborgen
• In einer realen Situation ohne Neustart hätte der Gyro jedoch dauerhaft in einem gesperrten Zustand verbleiben können

Wie der Defekt mit Allium gefunden wurde

• Die Allium-Spezifikation modelliert den Lebenszyklus jeder Ressource
  • Das Feld gyros_busy repräsentiert LGYRO, und die Regel GyroTorque beschreibt den Erwerb der Sperre, während GyroTorqueBusy den Wartezustand bei bereits gesetzter Sperre definiert
• Die Spezifikation formuliert die Verpflichtung, dass „eine Sperre, sobald sie true wird, zwingend wieder zu false werden muss“
  • Nachdem Claude alle Pfade verfolgt hatte, zeigte sich: Im Normalpfad (STRTGYR2) wird freigegeben, im Fehlerpfad (BADEND) jedoch nicht
• Der spezifikationsbasierte Ansatz prüft nicht, was der Code tut, sondern was er tun sollte
  • Tests prüfen das aktuelle Verhalten des Codes, Spezifikationen dagegen das beabsichtigte Verhalten
• Die Allium-Spezifikation und Code zur Reproduktion des Bugs wurden auf GitHub veröffentlicht

Moderne Implikationen und Lehren

• Die Programmierer damals mussten die Sperre mit den Befehlen CAF ZERO und TS LGYRO manuell freigeben
  • Sie mussten sich an alle möglichen Pfade erinnern und den Freigabecode von Hand an den richtigen Stellen einfügen
• Moderne Sprachen verhindern solche Probleme durch nicht freigegebene Ressourcen strukturell
  • Go mit defer, Java mit try-with-resources, Python mit with und Rust mit seinem Ownership-System sorgen für automatische Freigabe
• Trotzdem existieren Defekte des Typs CWE-772 (Missing Release of Resource after Effective Lifetime) weiterhin
  • Datenbankverbindungen, verteilte Sperren, File Handles oder die Abschaltreihenfolge von Infrastruktur liegen oft noch immer in der Verantwortung der Entwickler
• Obwohl alle Apollo-Missionen erfolgreich zurückkehrten, blieb dieser Defekt auch in der späteren Software COMANCHE (Kommandokapsel) und LUMINARY (Mondlandefähre) unverändert enthalten und wurde nie behoben
• Der 57 Jahre lang verborgene Defekt ist ein Beispiel dafür, wie wichtig verhaltensspezifikationsbasierte Analyse ist

[GN⁺]

Hacker-News-Kommentare

• Ich bin Mike Stewart, habe beim CuriousMarc-Kanal das AGC-Restaurierungsprojekt geleitet und bin Co-Maintainer von VirtualAGC.
  Der hier erwähnte Bug war tatsächlich ein Fehler in der AGC-Software. Er blieb jedoch nicht über die gesamte Laufzeit des Programms hinweg unentdeckt. Er wurde während der Tests der dritten Stufe von SATANCHE entdeckt, als L-1D-02 dokumentiert und zwischen Apollo 14 und 15 behoben.
  Die entsprechenden Berichte finden sich in ibiblio-Dokument 1 und Dokument 2.
  Die Korrektur bestand nicht einfach aus dem Hinzufügen von zwei Zeilen, die LGYRO auf 0 setzen, sondern umfasste auch eine Umstrukturierung des Codes sowie Logik zum Aufwecken wartender Aufgaben. Wenn man den Code von Apollo 14 und 15 vergleicht (Apollo-14-Code, Apollo-15-Code), sieht man den Unterschied.
  Es handelt sich auch nicht um einen still und heimlich auftretenden Bug, wie im Artikel beschrieben. LGYRO wird außerdem in STARTSB2 initialisiert, was bei jedem Programmwechsel ausgeführt wird und das Problem automatisch behebt. Daher trat es in der Praxis nur selten auf, nämlich nur bei Drehmomentoperationen während BADEND.
  Wenn der Bug bestehen blieb, sammelten sich mehrere Aufgaben an und führten schließlich zum Fehler 31202, einer Folgeverson von 1202. Dieses Problem wurde vor dem Flug von Apollo 14 entdeckt, und in den Apollo 14 Program Notes wurde ein Wiederherstellungsverfahren ergänzt.
  Außerdem heißt es, Ken Shirriff habe die Analyse auf Gate-Ebene durchgeführt, aber tatsächlich habe ich den größten Teil davon gemacht.
  Virtual AGC hat nur bei einigen Programmen eine Byte-für-Byte-Übereinstimmungsprüfung mit den ursprünglichen Core-Rope-Dumps abgeschlossen; für das Gesamtprogramm ist das noch nicht möglich. Der Großteil des Quellcodes wurde anhand gedruckter Exemplare oder Prüfsummen rekonstruiert.
  Margaret Hamilton war die „rope mother“ von Comanche, also der Software des Kommandomoduls, und Luminary, also das Mondlandemodul, lag in der Verantwortung von Jim Kernan. Das lässt sich im Organigramm von 1969 nachvollziehen.
  Zum Zeitpunkt des 1202-Alarms war der AGC nicht darauf ausgelegt, Aufgaben mit niedriger Priorität zu verwerfen. Im Gegenteil: Die Lande-Navigation war die Aufgabe mit der niedrigsten Priorität, während Antennensteuerung oder Display-Aktualisierung höher priorisiert waren. In diesem Dokument sind die Prioritäten der einzelnen Aufgaben zusammengefasst.
  Und schließlich wurde in realen Hardwaretests bestätigt, dass die Ursache des 1202-Alarms nicht eine Phasendifferenz, sondern eine Spannungsdifferenz (28V vs 15V) war. Ein Video des zugehörigen Experiments gibt es unter YouTube-Link.

  • Ich habe auf deinen Kommentar gewartet. Danke, dass du diese wirklich erstaunlichen historischen Details geteilt hast.
  • Die Hauptseite ist zwar schon beim nächsten Thema, aber das hier ist wirklich eine Fundgrube an Informationen. Danke, dass du dir die Zeit genommen hast.

• Wenn du dich für den Apollo-AGC interessierst, kann ich den CuriousMarc-YouTube-Kanal nur empfehlen. Dort dokumentiert ein technisch herausragendes Team die Restaurierung und Analyse vieler Komponenten des AGC.
  Besonders spannend ist die Neuinterpretation des berüchtigten 1202-Alarms. Üblicherweise wird er als vernachlässigbarer Sensorfehler beschrieben, tatsächlich hätte er unter bestimmten Bedingungen aber sehr kritisch werden können.

  • Man könnte also sagen, dass derselbe Landeversuch heute schwieriger oder leichter wäre. Wir kennen inzwischen viel mehr Fehlermodi als damals.
  • „Populär erklärt“ und „tatsächlich verstanden“ sind zwei verschiedene Dinge. Es gibt viele vereinfachte Darstellungen, aber unter Fachleuten war das Phänomen schon längst gut verstanden.
  • Die Diskussionen des CuriousMarc-Teams zur AGC-Restaurierung gehen auch in diesem Thread weiter.

• Mein Lieblings-Codefragment ist dieses hier:

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

  GitHub-Link

  • Dieser Code wird auch in The Codeless Code erwähnt.
  • CADR hat hier nichts mit der cadr-Funktion aus Lisp zu tun.
  • Kann jemand erklären, warum dieser Code so lustig ist?
  • Ich meine mich zu erinnern, einmal bei XKCD ein Gedicht über diesen Code gesehen zu haben, aber vielleicht täusche ich mich auch.

• Ich frage mich, ob verifiziert wurde, dass dieser Bug tatsächlich existiert. KI ist bei solchen explorativen Analysen stark, hat aber nach wie vor eine hohe False-Positive-Rate.
  Je nach Kontext kann das wichtig sein oder auch nicht. Es gibt auch viele Bugs, die KI nicht findet.
  Ich habe nicht selbst die Fachkenntnis, das zu verifizieren, finde es aber sehr interessant.

  • Eigentlich ist nicht einmal klar, ob die KI den Bug überhaupt gefunden hat. Es heißt nur, man habe ihn „in einer KI-nativen Sprache modelliert“.
    Die Erklärung des Lock-Erwerbs und der Fehlerszenarien wirkte allerdings ziemlich überzeugend.

• Dass sie einen echten Bug gefunden haben, ist interessant. Aber die dramatische Inszenierung des Textes grenzt an Fiktion.
  Da wird etwa so getan, als hätte jemand versehentlich mit dem Ellbogen einen Schalter berührt, oder ein durch Reset behebbares Problem wird überhöht dargestellt. Das macht den Text zwar zugespitzter, aber auch weniger glaubwürdig. Dazu kommt noch der KI-haft wirkende Stil, der zusätzlich stört.

  • Natürlich war das ein Schalter mit Schutzabdeckung.
    Aber wenn man normalen Leserinnen und Lesern einen subtilen Bug erklären will, braucht man ein gewisses Maß an Storytelling. Wird es zu technisch, verlieren sie das Interesse; wird es zu dramatisch, wird es von Fachleuten kritisiert. Diese Balance zu finden ist schwierig.

• Ich habe den im Artikel enthaltenen Repro-Code selbst ausgeführt.
  GitHub-Link
  Er läuft zwar, aber Phase 5, also die Deadlock-Demonstration, ist vollständig Fake-Ausgabe. Es wird kein echter Emulator ausgeführt, sondern nur ein erwartetes Ergebnis ausgegeben.
  Deshalb habe ich selbst ein PR eingereicht und es so korrigiert, dass es wirklich im Emulator läuft, und dabei auch verifiziert, dass der Zweizeilen-Patch den Bug behebt.

  • Solchen „KI-Code“ sehe ich oft. Er tut so, als sei er testgetrieben entwickelt, liefert in Wirklichkeit aber Fake-Code, der nur die Tests besteht.
    KI-generierter Code neigt dazu, mit „Jetzt ist es perfekt!“ stehenzubleiben, und Leute glauben das und deployen ihn unverändert. Das ist das eigentliche Problem.

• Der Text selbst ist interessant, fühlt sich aber stark künstlich an, als wäre er von einem LLM geschrieben.

  • Auf mich wirkte er überhaupt nicht wie von einem LLM. Vielleicht liegt es daran, dass er im Stil einer wissenschaftlichen Arbeit geschrieben ist.
  • Juxt hat schon früher hervorragende Texte veröffentlicht und verfügt über ausreichend Fachwissen. Deshalb halte ich es für unwahrscheinlich, dass dieser Text von einer KI geschrieben wurde.
  • Zur Referenz: Laut Pangram-Analyse wurde der Text als menschengeschrieben eingestuft.
  • Allerdings ist bei einem anderen Text von Juxt ausdrücklich vermerkt, dass er von Claude geschrieben wurde. Das steht im letzten Absatz von diesem Beitrag.
  • Außerdem stimmt der Teil über Rust und Locks sachlich nicht. Darauf wird in diesem Kommentar hingewiesen.

• Dass selbst in der Software, die mit nur 4 KB Speicher Menschen zum Mond brachte, noch unentdeckte Bugs stecken können, zeigt, wie viel Komplexität auch in kleinem Code verborgen sein kann.

  • Je weniger Speicher vorhanden ist, desto schwächer ist die Korrelation zwischen Codeumfang und Bugrate. Im Gegenteil: Der Versuch, Komplexität zu komprimieren, erhöht eher die Zahl der Bugs.
  • Solche Aussagen klingen für mich einfach nach einer leeren Floskel.

• Die Formulierung „Wir haben eine Spezifikation aus dem Code abgeleitet“ ist falsch. Man sollte noch einmal nachsehen, was mit Spezifikation gemeint ist.

  • Tatsächlich bedeutet das einfach nur Reverse Engineering.

• Sowohl der Artikel als auch das Repository sind schlampige Arbeiten.
  Im Repository-Link sieht man, dass als „Reproduktion“ der Bug gar nicht wirklich ausgeführt wird, sondern nur Ausgabezeilen nach dem Muster „so würde es aussehen“ aufgelistet werden.