アポロ11号の誘導コンピュータコードに未記録のバグを発見しました

33日前原文(juxt.pro)

概要

Apollo Guidance Computer (AGC) のコードに、57年間見逃されていたバグを発見
Allium という行動仕様言語を用いてAGCのIMUサブシステムを形式的に検証
バグは LGYROリソースロック の解放漏れによるもので、特定のエラーパスで発生
バグが発現すると ジャイロ操作が完全に停止 し、復旧にはリセットが必要
現代のプログラミング にも通じるリソース管理の重要な教訓

AGCコードベースの歴史と注目

Apollo Guidance Computer (AGC) は最も精査されたコードベースの一つ
2003年にRon Burkeyとボランティアが MIT Instrumentation Laboratory の印刷リストから手作業でコードを転記
2016年、Chris Garryの GitHubリポジトリ が話題となり、多数の開発者がAGCのアセンブリコードを閲覧
AGCは 2KBの消去可能RAM、 1MHzのクロック、 74KBのコアロープメモリ を搭載
- コアロープメモリは手作業で銅線を磁気コアに通して作成
- 作業者は"Little Old Ladies"、メモリ自体はLOL memoryと呼ばれた
Ken Shirriffによる回路レベルの解析、Virtual AGCプロジェクトによるエミュレーションとバイト単位での検証
これまで 形式的検証やモデルチェック は行われていなかった

Alliumによる新しい検証アプローチ

Allium を使い、IMUサブシステムから 行動仕様 を抽出
- 各共有リソースのライフサイクル（取得・解放）をモデル化
- コードの全経路でリソースが適切に解放されているかを明示的に検証
このアプローチで 従来の読解・エミュレーションでは発見できなかったバグ が浮上

発見されたバグの詳細

AGCはIMUの制御に LGYROロック を使用
- ジャイロのトルク操作開始時にロック取得、3軸のトルク完了後に解放
- 同時操作を防ぐための排他制御
異常経路（BADEND） でロック解放処理が抜け落ちていた
- "CAF ZERO"→"TS LGYRO"の2命令（4バイト）が欠落
- ロックが解放されず、以降のジャイロ操作はすべてブロック
- エラー発生時、再起動しない限り復旧不可

実運用での影響シナリオ

月周回中の Michael Collins がP52プログラムで星位置合わせを実施中、誤ってIMUのケージスイッチを作動
- ケージイベントでトルク処理中断、BADEND経由でロック未解放
- 再度P52や手動トルクを試みても応答なし、エラー表示もない
- 他の機能は正常、原因不明のままジャイロ操作不能に
- 再起動すれば復旧するが、状況からは必要性が判断できない

AGC開発チームの防御的設計とバグの隠蔽

Margaret Hamilton 率いるMITチームによる先進的なソフトウェア設計
- 優先度スケジューリング、非同期マルチタスク、リスタート保護、ソフトウェアエラー回復
- 1202アラーム時の負荷分散も設計通り動作
多くの重大バグは 仕様の誤り であり、コーディングミスではなかった
BADENDは一般的なリソース解放処理のみを行い、LGYROのような特定リソースには未対応
AGCのリスタートロジックが副次的にLGYROを初期化し、問題を隠蔽
- 再起動を伴わないケージイベントではバグが発現

Alliumによる仕様記述とバグ発見のメカニズム

Allium仕様では各リソース（例: gyros_busy）を 取得・解放の義務 として明示
仕様記述により、各パスで解放が抜けていないかを網羅的に検証
BADEND経由でのみLGYROが解放されないことを特定
テストではなく 仕様ベースの検証 がこの発見を導く

リソース管理の現代的意義

AGCではロック解放を 手動で明示的に記述 する必要
Goのdefer、Javaのtry-with-resources、Pythonのwith、Rustの所有権システムなど、現代言語はロック漏れを構造的に防止
しかし、 CWE-772（リソース解放漏れ） として依然として一般的なバグパターン
データベース接続、分散ロック、ファイルハンドルなど、手動管理が残る領域で再発の可能性

結論と教訓

Apolloの全クルーは無事帰還したが、この IMUモード切替バグ は複数ミッションに渡って未修正のまま
57年間隠れていた深刻なバグが形式的仕様から発見
現代のシステム開発 においても、リソース管理と仕様記述の重要性を再認識する必要
Allium仕様やバグ再現例は GitHub で公開中

謝辞

Farzad “Fuzz” Pezeshkpourによるバグの独立再現、Danny SmithおよびPrashant Gandhiによる初期ドラフトのレビュー

Hackerたちの意見

超面白いけど、この記事がLLMによって書かれたものでなければよかったな。なんか魂がない感じで、プラスチックみたい。

└

AIの文章を認識すると、身体的な反応が出てきそう。まるで、頭の中で静かに黒板を爪で引っかく音を聞いてるような、圧倒的なフラストレーションがある。

└

目立つ部分ってある？Juxtは昔からすごくいい記事を書いてたし、LLMが出る前からもそうだった。自分たちで書くための専門知識や知識が欠けてるわけじゃないって知ってるし、この記事をまだ全部読んでないけど、今の時点でLLMに記事を書かせてるとは思えないな。

└

参考までに、Pangramはこの記事が完全に人間によって書かれたと思ってるみたいだよ： https://www.pangram.com/history/f5f68ce9-70ac-4c2b-b0c3-0ca8...

└

俺にはLLMの警報が鳴らないな。ただの科学記事みたいに読めるし、そういうのはよく魂がない。

└

それがそうだった証拠はないよ。

└

これはHNの投稿のかなりの割合でトップの返信になってるけど、これをやめさせるべきだと思う。 - 嘲笑的 - 浅い否定（内容に触れて） - ひねくれた - 余計なイライラこういうのはサイトのガイドラインで明示的に禁止されてることだよ。[1] ダウンボートは、フロントページにふさわしくないと思うアイテムに使う道具だ。毎回同じコメントはいらないよ。[1] - https://news.ycombinator.com/newsguidelines.html

└

「LLMによって書かれた」って、どのデータや症状に基づいてるの？

└

もっとひどいのを見たことあるよ。誰かが既に書いたものをLLMで磨き直したか、自分で手動で編集したかのどっちかだね。短い文の構造が一番怪しいけど、実際には目立つものは見当たらないな。普通はすぐに気づくんだけど。

└

君のコメントを特に取り上げるわけじゃないけど、HNにはAI生成コンテンツについて文句を言うのを禁止するルールがあった方がいい気がする。ほとんどの議論で、元の投稿やコメントの中に「AIのゴミ」って文句を言ってる人がいる気がする。

これは本当に洞察に満ちて力強く書かれてて、最後には背筋がゾクゾクしたよ。こんな素晴らしい文章を書いた作者が「AIのゴミ」って非難されるなんて、なんてひどい世界なんだろう。文法やレトリックをうまく使ってるだけなのに。

└

読んでる間、完全に引き込まれたよ。コリンズのジレンマの描写は、彼が一人で地球に戻るかもしれない実際のシナリオが描かれたのを初めて見た。もしLLMがそれを書いたなら、もうLLMアートに反対する気はないな。

誰かこれが実際のバグだったか確認した人いる？AIの強みの一つは探索、つまりバグを見つけることなんだけど、偽陽性率が高いのが難点だよね。文脈によってはそれが重要だったり、そうじゃなかったりするし。AIが見つけられないバグもたくさんあるから、人間なら見つけられるかも。私はこのバグが実際に起きたか確認する専門知識はないけど、興味はあるな。

└

AIがバグを見つけるために使われたかどうかもはっきりしないね。「AIネイティブ」な言語でソフトウェアをモデル化したって言ってるけど、それが何を意味するのかも不明だし。最初にアポロコードのジャイロソフトウェアをモデル化することになった経緯も不明だよ。でも、ロック取得と失敗シナリオの説明はかなり明確で説得力があると思う。

誰かタイトルを修正して「claude codeを使って」と追加してくれない？最近はそれが普通だからさ。

└

それと「AIも間違えることがある」って追加しておいて。ありがとう。

4KBのメモリで動いて人間を月に送ったソフトウェアには、まだ発見されていないバグがあるんだ。それは、最小のコードベースの中にも隠れている複雑さを示してるよね。

└

俺の予想では、こんなにメモリが少ない環境では、プログラムの長さとバグの発生率はあんまり関係ないと思う。むしろ、数KBのメモリに複雑なものを詰め込もうとすると、バグが出る可能性がめっちゃ高くなるんじゃないかな。

これが好きな人には、CuriousMarcのYouTubeチャンネルをぜひ見てほしい。アポロのAGCのいろんな部分を保存して理解しようとする努力を、技術的に優秀で情熱的な仲間たちと一緒に記録してるんだ。彼らが取り組んでいる中で、特に面白いのは、悪名高い1202アラームの再解釈の可能性だよ。今のところ、これはセンサーの意味不明な読み取りに関係していると一般的に説明されていて、実際の月面着陸では無視しても安全だったんだ。でも、確か彼らの調査で、そのエラーが非常に重大で、宇宙飛行士たちを危険にさらす可能性があった条件がたくさんあったことがわかったんだ。めっちゃ興味深いよ。

└

だから、同じ着陸を再現するのが難しい（または簡単？）んだよね。今は当時よりもずっと多くの失敗モードがわかってるから。

いまだに俺のお気に入りのコードスニペット。 TC BANKCALL # TEMPORARY, I HOPE HOPE HOPE CADR STOPRATE # TEMPORARY, I HOPE HOPE HOPE TC DOWNFLAG # PERMIT X-AXIS OVERRIDE https://github.com/chrislgarry/Apollo-11/blob/master/Luminar...

└

これ、説明してくれる？

読んでて面白かった。よくできてるね。アポロ計画に関わった人たちはみんなすごかったし、知られざるヒーローもたくさんいたよね。

仕様はコードから導き出されたもので、元の要件からではないんだ。だから「コードが何をしているかをモデル化して、そのモデル通りにコードが動いてないことがわかった」ってことだよね。これは循環論法だよ、モデルがコードが表現していない意図を捉えている場合を除いては。逆コンパイルするときに失われるのがその意図だから、元の要件がまだ存在するコードベースにこれを適用してみたいな。

彼らの仕様言語の応用について、https://juxt.github.io/allium/ これと従来の仕様言語との違いは、Alliumの仕様が自然言語で書かれていて、実行はLLMによって行われることみたい。これにより、非構造的なプランファイルと形式的な仕様言語の中間に位置する感じだね。コードの品質を向上させるための低摩擦な方法として、これが見えてくるよ。

ハクソク