아폴로 11 유도 컴퓨터 코드에서 발견된 문서화되지 않은 버그

• 57년간 완벽에 가깝다고 여겨졌던 Apollo Guidance Computer(AGC) 코드에서 자원 잠금 해제 누락 버그가 발견됨
• JUXT 팀이 AI 명세 언어 Allium과 Claude를 이용해 13만 줄의 어셈블리를 분석하며, 기존 검증 방식으로는 드러나지 않던 결함을 식별함
• 자이로 제어 루틴의 비정상 종료 경로(BADEND) 에서 LGYRO 잠금이 해제되지 않아, 이후 모든 자이로 관련 기능이 멈출 수 있는 구조임
• 실제 임무 중 달 궤도에서 Cage 스위치가 잘못 눌렸다면, Program 52 정렬 작업이 중단되고 Collins가 하드웨어 고장으로 오인할 가능성이 있었음
• 이 사례는 행위 명세 기반 분석이 오래된 코드에서도 새로운 결함을 찾아내는 강력한 방법임을 보여줌

Apollo 11 유도 컴퓨터에서 발견된 잠재적 결함

• Apollo Guidance Computer(AGC) 는 역사상 가장 철저히 검토된 코드베이스 중 하나로, 수많은 개발자와 연구자들이 분석해 왔음
  • 그러나 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라는 공유 잠금으로 관리
  • 자이로스코프를 토크할 때 잠금을 획득하고, 세 축 모두 완료되면 해제
  • 동시에 두 루틴이 하드웨어를 조작하지 않도록 보호
• 그러나 비정상 종료 경로에서 잠금이 해제되지 않음
  • 정상 종료 시 STRTGYR2 루틴이 LGYRO를 해제하지만, ‘Caging’(자이로 보호용 물리적 잠금)이 발생하면 BADEND 루틴으로 빠짐
  • BADEND에는 CAF ZERO와 TS LGYRO 두 명령(총 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년간 숨겨져 있던 결함은 행위 명세 기반 분석의 중요성을 보여주는 사례임