Apollo 11 誘導コンピュータのコードで発見された文書化されていないバグ

 (juxt.pro)
2 ポイント 投稿者 GN⁺ 22 일 전 | 1件のコメント | WhatsAppで共有
  • 57年間ほぼ完璧だと考えられていた Apollo Guidance Computer(AGC) のコードで、リソース解放漏れバグが発見された
  • JUXTチームがAI仕様言語 Allium と Claude を用いて13万行のアセンブリを分析し、従来の検証方式では表面化しなかった欠陥を特定した
  • ジャイロ制御ルーチンの 異常終了経路(BADEND) で LGYRO ロックが解除されず、その後のすべてのジャイロ関連機能が停止しうる構造だった
  • 実際の任務中に月周回軌道で Cageスイッチ が誤って押されていた場合、Program 52 のアラインメント作業が中断され、Collins がハードウェア故障と誤認した可能性があった
  • この事例は、振る舞い仕様ベースの分析が古いコードでも新たな欠陥を見つけ出す強力な手法であることを示している

Apollo 11 誘導コンピュータで見つかった潜在的欠陥

  • Apollo Guidance Computer(AGC) は歴史上最も徹底的に精査されたコードベースの1つで、多くの開発者や研究者が分析してきた
    • しかし57年間発見されなかった リソースロック解除漏れバグ がジャイロ制御コードで確認された
    • エラー経路でロックが解除されないため、誘導プラットフォームの再アラインメント機能が無効化される問題
  • JUXTチームはAIベースの仕様言語 Allium と Claude を使って、13万行のAGCアセンブリを1万2,500行の振る舞い仕様へ変換した
    • コードから直接仕様を抽出し、リソース取得と解放のすべての経路をモデル化
    • この過程で、従来のコード読解やエミュレーションでは見つからなかった欠陥が明らかになった

コード構造と分析アプローチ

  • AGCのソースは2003年に Ron Burkey とボランティアたちがMIT Instrumentation Laboratory の印刷物を手作業で転記して公開された
    • 2016年には Chris Garry の GitHub リポジトリが公開され、世界中の開発者が2KB RAM、1MHz CPUのアセンブリコードを読み込んだ
  • プログラムは74KBの core rope memory に保存され、銅線を磁気コアに手作業で編み込んで1と0を表現していた
    • この作業を担った女性技術者たちは「Little Old Ladies」と呼ばれ、メモリは LOL memory と名付けられた
  • これまでAGCに対して 形式検証、モデル検査、静的解析 が行われた記録はなかった
    • 検証の大半はコードの読解、エミュレーション、転記精度の確認に集中していた
  • JUXTは IMU(Inertial Measurement Unit) サブシステムの振る舞い仕様をAlliumで記述した
    • 各共有リソースの 取得・解放タイミング をモデル化して欠陥を特定した

ジャイロ制御ルーチンのロック解除漏れ

  • AGCはIMUを LGYRO という共有ロックで管理していた
    • ジャイロスコープにトルクをかけるときにロックを取得し、3軸すべてが完了すると解除する
    • 同時に2つのルーチンがハードウェアを操作しないよう保護するための仕組み
  • しかし 異常終了経路 ではロックが解除されない
    • 正常終了時には STRTGYR2 ルーチンが LGYRO を解除するが、「Caging」（ジャイロ保護用の物理ロック）が発生すると BADEND ルーチンへ分岐する
    • BADEND には CAF ZERO と TS LGYRO の2命令（計4バイト）が欠けており、ロックが残ってしまう
  • LGYRO が解放されないと、その後のすべてのジャイロトルクルーチンがロック待ち状態で停止する
    • 微調整アラインメント、ドリフト補正、手動トルクなど、すべてのジャイロ関連機能が中断される

月の裏側での潜在的影響

  • 1969年7月21日、Michael Collins は月周回軌道で Program 52（恒星観測アラインメントプログラム）を定期的に実行していた
    • プラットフォームがドリフトすると、帰還用エンジンの向きが誤る危険があった
  • もしトルク制御中に誤って Cageスイッチ が押されて BADEND 経路に入っていたら、LGYRO が解除されず、その後のすべてのP52が停止した可能性がある
    • DSKY（表示・キーボード）は入力を受け付けるが反応しない
    • 他の機能は正常に動作するため、Collins はハードウェア故障と誤認した可能性があった
  • 再起動（ハードリセット）を行えば問題は解決したはずだが、月面着陸中に発生した 1202アラーム の経験から、即座にリセットを判断するのは難しかったと考えられる

既存システムの防御的設計と限界

  • Margaret Hamilton が率いたMITチームは、優先度スケジューリング、非同期マルチタスク、再起動保護など、現代ソフトウェア工学の基盤となる概念を導入した
    • この設計により、1202アラーム発生中でも着陸が可能だった
  • 主要な欠陥の多くは 仕様の誤り であり、Don Eyles が文書化した事例のように、ハードウェア間の位相同期漏れによってCPU負荷が増大したこともあった
  • 今回の欠陥も似た構造を持つ
    • BADEND はIMUモード切り替えの共通終了ルーチンで、MODECADR などの共通リソースは解放するが LGYRO は処理しない
    • 再起動ロジックが LGYRO を初期化するため、テスト中は問題なく復旧し、欠陥が隠れていた
  • しかし 再起動がない実運用環境 では、ジャイロが恒久的なロック状態に陥る可能性があった

Allium による欠陥発見の過程

  • Allium仕様は各リソースの ライフサイクル(lifecycle) をモデル化する
    • gyros_busy フィールドが LGYRO を表し、GyroTorque ルールはロック取得を、GyroTorqueBusy ルールはすでにロックされている場合の待機状態を定義する
  • 仕様は「ロックが true になったら、必ず false に戻らなければならない」という義務を明示する
    • Claude がすべての経路を追跡した結果、正常経路(STRTGYR2)では解除されるが、エラー経路(BADEND)では漏れていることが判明した
  • 仕様ベースのアプローチは、コードが 何をしているか ではなく 何をすべきか を検証する
    • テストはコードの現在の動作を確認するが、仕様は意図された振る舞いを検証する
  • Allium仕様とバグ再現コードはGitHubで公開されている

現代的な示唆と教訓

  • 当時のプログラマは CAF ZERO と TS LGYRO 命令で手動でロックを解除しなければならなかった
    • すべての経路を記憶し、手動で解放コードを挿入する必要があった
  • 現代の言語はこうした リソース解放漏れ問題 を構造的に防ぐ
    • Goの defer、Javaの try-with-resources、Pythonの with、Rustの 所有権システム などは自動解放を保証する
  • それでも CWE-772(リソース解放漏れ) 型の欠陥は今なお存在する
    • データベース接続、分散ロック、ファイルハンドル、インフラ停止順序などは依然としてプログラマの責任である
  • Apolloミッションはすべて無事に帰還したが、この欠陥はその後の COMANCHE(司令船) と LUMINARY(月着陸船) ソフトウェアにもそのまま含まれ、修正されなかった
  • 57年間隠れていたこの欠陥は、振る舞い仕様ベース分析の重要性 を示す事例である

関連記事

1件のコメント

 
GN⁺ 22 일 전
Hacker News のコメント

  • 私は Mike Stewart で、CuriousMarc チャンネルで AGC 復元プロジェクトを率いており、VirtualAGC の共同管理者でもある。
    今回言及されているバグは、実際に存在した AGC ソフトウェアの欠陥だ。だが、プログラムの全期間を通して放置されていたわけではない。SATANCHE の第3段階テスト中に発見され、L-1D-02 として記録され、Apollo 14 と 15 の間に修正された。
    関連報告書は ibiblio 文書 1 と 文書 2 で確認できる。
    修正は単に LGYRO を 0 にする 2 行を追加しただけではなく、コード構造の再調整と待機中タスクを起こすロジックまで含んでいる。Apollo 14 と 15 のコードを比較すれば（Apollo 14 コード、Apollo 15 コード）、違いが分かる。
    記事で説明されているような静かに発生するバグではない。LGYRO は STARTSB2 でも初期化され、これはプログラム切り替えのたびに実行されるため、問題は自動的に解消される。したがって実際には、BADEND 中にトルク動作を行う場合にのみまれに発生していた。
    もしバグが継続すると、複数のタスクが蓄積され、最終的には 31202 エラー（1202 の後継版）を引き起こす。この問題は Apollo 14 の飛行前に発見され、Apollo 14 Program Notes に復旧手順が追加された。
    また、Ken Shirriff がゲートレベル解析を行ったとされているが、実際にはその大半を私が行った。
    Virtual AGC は一部のプログラムについてのみ、元のコアロープダンプとの バイト単位一致検証を完了しており、全プログラムではまだ不可能だ。ソースの大半は印刷物やチェックサムを基に復元されたものだ。
    Margaret Hamilton は Comanche（司令船ソフトウェア）の「rope mother」であり、Luminary（月着陸船）は Jim Kernan が担当していた。1969年の組織図 で確認できる。
    1202 アラーム当時、AGC は低優先度タスクを切り捨てるようには設計されていなかった。むしろ着陸誘導は 最も低い優先度のタスクで、アンテナ制御やディスプレイ更新のほうが高優先度だった。この文書 に各タスクの優先度がまとめられている。
    最後に、1202 アラームの原因は位相差ではなく、**電圧差（28V vs 15V）**だったことが実機ハードウェア試験で確認されている。関連実験の映像は YouTube リンク で見られる。

    • あなたのコメントを待っていた。本当に驚くべき 歴史的な詳細を共有してくれてありがとう。
    • メインページはすでに別の話題へ移ってしまったが、これは本当に 宝のような情報だ。時間を割いてくれて感謝している。

  • Apollo AGC に興味があるなら、CuriousMarc YouTube チャンネルはぜひ見るべきだ。AGC のさまざまな部品を復元・解析していく過程を、技術的に卓越したチームが記録している。
    特に興味深いのは、悪名高い 1202 アラームの再解釈だ。一般には無視できるセンサーエラーとして知られているが、実際には特定条件下で非常に致命的になりえた。

    • ということは、今日では同じ着陸を再挑戦するのは当時より難しいとも易しいとも言える。あの頃よりずっと多くの 故障モードを知っているからだ。
    • 「一般向けに説明されたこと」と「実際に理解されていること」は違う。単純化された説明は多いが、専門家の間ではすでによく理解されている現象だ。
    • CuriousMarc チームの AGC 復元に関する議論は このスレッド でも続いている。

  • 私が一番好きなコード断片はこれだ。

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

    GitHub リンク

    • このコードは The Codeless Code でも言及されている。
    • ここでの CADR は Lisp の cadr 関数とは関係ない。
    • このコードがなぜ面白いのか説明できる人はいる？
    • 昔 XKCD でこのコードについての詩を見た記憶があるが、たぶん勘違いかもしれない。

  • このバグが本当に存在するのか検証されたことがあるのか気になる。AI はこうした 探索的分析には強いが、依然として 誤検出率が高い。
    文脈によって重要かもしれないし、そうでないかもしれない。AI が見つけられないバグも多い。
    自分には直接検証する専門性はないが、とても興味深い。

    • そもそも AI がバグを見つけたのかどうかも不明だ。「AI native 言語でモデリングした」としか書かれていない。
      ただし、ロック取得と失敗シナリオの説明はかなり説得力があった。

  • 彼らが実際のバグを見つけたのは興味深い。だが、記事の 劇的な演出はほとんど虚構に近い。
    肘でスイッチに触れてしまうとか、リセットで解決可能な問題を大げさに描くとか。そうした点は記事を刺激的にしたが、信頼性は下げている。しかも AI が書いたような文体なのでなおさら気になる。

    • もちろんそのスイッチは 保護カバー付きのスイッチだった。
      ただ、一般読者に微妙なバグを説明するには、ある程度の ストーリーテリングが必要だ。技術的すぎると興味を失われるし、劇的すぎると専門家に批判される。そのバランスを取るのは難しいと思う。

  • 記事に含まれていた 再現コード（repro） を実際に走らせてみた。
    GitHub リンク
    動作はするが、Phase 5（デッドロック実演）は完全に 偽の出力だ。実際のエミュレータは動かしておらず、予想結果を出力しているだけだった。
    そこで私が自分で修正した PR を出し、エミュレータ上で本当に動くよう直し、2 行のパッチがバグを解決することも検証した。

    • こういう「AI コード」はよく見る。テスト駆動開発を真似しているが、実際には テストだけ通る偽コードを出してくる。
      AI 生成コードは「これで完璧だ！」と言って止まり、それを信じた人がそのままデプロイしてしまう。そこが本当の問題だ。

  • 記事自体は興味深いが、LLM が書いたような人工的な感じが強い。

    • 私にはまったく LLM っぽく感じなかった。科学論文風のスタイルだからそう見えるのかもしれない。
    • Juxt は以前から優れた記事を書いてきたし、専門性も十分ある。だから今回の記事が AI 作成である可能性は低いと思う。
    • ちなみに Pangram 分析 によれば、この記事は 人間が書いたものと判定されている。
    • ただし Juxt の別の記事のひとつは、実際に Claude が書いたと明記されている。その記事 の最後の段落で明かされている。
    • しかも Rust とロックに関する部分は 事実と異なる。このコメント で指摘されている。

  • わずか 4KB のメモリで人類を月に送ったソフトウェアにも、なお 未発見のバグがあるというのは、小さなコードにも複雑さが潜んでいることを示している。

    • メモリが少ないほど、コード長とバグ率の相関は弱くなる。むしろ 複雑さを圧縮しようとしてバグが増える。
    • こういう言い方はただの 中身のない決まり文句のように聞こえる。

  • 「コードから仕様を導き出した」という表現は誤りだ。specification の意味を調べ直したほうがいい。

    • 実際にはそれは単なる リバースエンジニアリングを意味している。

  • 記事もリポジトリも 雑な出来の成果物だ。
    リポジトリのリンク を見れば、「再現」と言いながら実際のバグは実行せず、単に「こうなるはずだ」という 出力文だけを並べている。