本篇文章更新時間：2026/04/08
如有資訊過時或語誤之處，歡迎使用 Contact 功能通知或向一介資男的 LINE 社群反應。
如果本站內容對你有幫助，歡迎贊助支持 。
內容目錄
月球背面的漏網之錯：阿波羅導航電腦的 57 年隱性漏洞
一段從 JUXT 部落格文章《A bug on the dark side of the Moon》獲得的深度閱讀筆記
編輯前言：這篇文章講述了一個在阿波羅導航電腦（AGC）中潛藏超過半世紀的錯誤——一個僅差四個 bytes 的資源鎖問題。更令人驚訝的是，它不是靠人工審查或模擬找到，而是透過行為規格語言與 AI 推導出的邏輯缺口。這不只是太空歷史故事，而是一堂現代軟體工程仍然需要的基本課。
核心觀點（Key Takeaways）
- AGC 的程式碼被無數人審視過，但仍潛藏未被發現的資源鎖錯誤。
- JUXT 使用 Allium（行為規格語言）與 Claude，把 13 萬行組語蒸餾成邏輯規格，逼出了問題路徑。
- 漏掉的一行資源釋放，使 IMU 的陀螺儀在特定錯誤路徑中永久「卡死」。這在 Apollo 11 上可能造成致命後果。
深入解析
阿波羅導航電腦（AGC）被視為史上最被細讀的程式碼之一。其組語從 2003 年被逐字轉錄後，無數開發者、學者、模擬器都對它進行過深入探究。然而，文章指出：這些檢查是「閱讀與模擬」的檢查，但不是「行為邏輯」的檢查。
JUXT 的方法完全不同：他們用 Allium 針對慣性測量單元（IMU）寫下「行為規格」。這類規格強制描述每個共享資源的生命週期：何時取得、何時釋放、哪些路徑必須完成。
漏掉的四個 bytes
文章指出 AGC 管理陀螺儀資源的鎖（LGYRO），正常流程會在完成三軸 torque 後釋放。但若在 torque 過程中被觸發「cage」（保護性機械制動），程式會從 BADEND 出口離開，而這裡缺了釋放 LGYRO 的指令：
Missing TS LGYRO — 僅需四個 bytes。
這造成什麼結果？之後任何 torque 嘗試都會因為看到 LGYRO 被佔用而沉睡等待「永不出現」的喚醒信號。外表看起來像：
- 程式接受指令
- DSKY 正常工作
- 但 IMU 完全不再 torque
也就是說，導航平台再也無法對準方向。
這不是理論問題——Apollo 11 的 Michael Collins 每兩小時就得跑一次星象校準程式 P52。如果剛好發生 cage 事件、再觸發這條錯誤路徑，他可能在月球背面面對一台「看似正常但陀螺儀實際卡死」的導航電腦。
“A dead gyro system behind the Moon… exactly that scenario.”
為什麼 57 年都沒發現？
原因在於 AGC 防禦式架構非常強：任何軟體重啟都會清掉 LGYRO。因此測試時如果剛好觸發重啟，看起來就像系統「自己修好了」。
這讓原始問題一直被掩蓋，並隨著 COMANCHE、LUMINARY 代代沿用。
規格語言是怎麼逼出錯誤的？
文章給了一段代表性的 Allium 規格：
GyroTorque ensures gyros_busy = true
這表示只要 torque 啟動，某處一定要把 gyros_busy 設回 false。AI 在行為規格推導下被迫追蹤每一條控制流程，直接定位到 BADEND 缺少釋放行為。
換句話說：
- 測試只能驗證「程式是否照寫的執行」。
- 規格則逼你回答「程式是否完成它應該做的事」。
筆者心得與啟發
讀完這篇文章，我最深刻的感想是：規格比程式碼更能揭露真正的問題。
AGC 的組語被讀過無數次，模擬也跑了幾十年，但因為大家都是沿著「程式碼表層」去看，問題始終隱形。反而是一份由 AI 協助產生的高階行為規格，讓一個四個 bytes 的缺失無所遁形。
這讓我重新思考軟體開發中的盲點：
- 我們常常「相信程式碼」，但很少問「它是否實現預期行為」。
- 靠測試捕捉邊界案例是一場機率遊戲，不可能涵蓋所有控制流程。
- 而資源釋放類錯誤（CWE-772）在現代軟體仍然頻繁出現。
文章最後提出一句耐人尋味的問題——
A fifty-seven-year-old bug hid in flight-proven assembly. What’s hiding in yours?
這對我來說不是恐嚇，而是一種提醒：
當系統越複雜、越關鍵，我們越需要用規格與形式化的方法來「逼問」程式碼的真正意圖，而不只是檢查它的字面行為。
這篇文章不只是太空歷史的冷知識，而是一堂關於現代軟體工程的反思課。