AIと仕様言語を使用してアポロ11誘導コンピュータコードで未文書化のバグを発見

史上最も精査されたコードベースのバグ発見

アポロ誘導コンピュータ（AGC）のコードは、MIT計測研究所の印刷リストから転写され、2003年から公開されています。2016年、Chris GarryのGitHubリポジトリが話題となり、消去可能RAM 2K、クロック1MHzのハードウェアで動作するこのアセンブリコードを、何千人もの開発者が検証してきました。しかし、これほどの精査にもかかわらず、飛行コードに対する形式的検証、モデル検査、静的解析はこれまで公表されていませんでした。

バグの内容：ジャイロ制御におけるリソースロックのリーク

このバグは、宇宙船の姿勢を把握するジャイロスコープベースのプラットフォームを管理する慣性計測装置（IMU）サブシステムに存在します。AGCは、LGYROと呼ばれる共有リソースロックを通じてIMUを管理します。コンピュータがジャイロスコープにトルクをかける必要があるとき（プラットフォームのドリフト補正や星の位置合わせを行うため）、開始時にLGYROを取得し、3軸すべてにトルクがかかった時点で解放します。

問題は「ケージング」の際に発生します。これは、ジャイロスコープを損傷から保護するためにIMUのジンバルを物理的に固定する緊急措置です。トルクが正常に完了すると、ルーチンはSTRTGYR2を経由して終了し、LGYROロックが解除されます。しかし、トルク実行中にIMUがケージングされると、コードはBADENDというルーチンを経由して終了し、このルーチンではロックが解除されません。

欠けているのはたった2つの命令：CAF ZERO TS LGYRO - わずか4バイトです。一度LGYROが固着すると、それ以降のジャイロへのトルク試行はすべてロックが保持されていることを検知し、決して来ないウェイク信号を待ってスリープ状態になり、ハングアップします。これにより、精密位置合わせ、ドリフト補償、手動ジャイロトルクが無効化されることになります。

発見方法：AIと行動仕様

研究者らは、Claudeとオープンソースの行動仕様言語Alliumを使用して、13万行のAGCアセンブリコードを1万2500行の仕様に凝縮しました。この仕様は、すべての共有リソースのライフサイクル（いつ取得され、いつ解放されるべきか、どのパスで行われるか）をモデル化しています。このアプローチにより、コードの読み取りやエミュレーションでは見逃されていた欠陥が浮き彫りになりました。

仕様はコード自体から導き出され、そのプロセスが直接欠陥を指し示しました。これは、コードの読み取り、エミュレーション、転写の検証に焦点を当てた従来の精査とは異なるアプローチを表しています。

歴史的経緯と潜在的な影響

1969年7月21日、ニール・アームストロングとバズ・オルドリンが月面を歩いている間、マイケル・コリンズは司令船コロンビアで単独で月を周回していました。2時間ごとに彼は月の裏側に消え、地球との無線通信が途絶えました。その間、彼はプログラム52を実行し、誘導プラットフォームが正しい方向を向くように星の観測による位置合わせを行っていました。もしプラットフォームがドリフトしていたら、帰還のためのエンジン噴射が誤った方向を向くことになります。

このバグは、コリンズがコンピュータがジャイロスコープにトルクをかけている最中に誤ってケージスイッチを起動した場合に発現した可能性があります。コードはケージングを検知し、トルクを中止して終了することで、この状況を適切に処理します。しかし、P52位置合わせは失敗し、誘導プラットフォームは基準を失う可能性がありました。