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

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

  • Apollo Guidance Computer(AGC) 는 역사상 가장 철저히 검토된 코드베이스 중 하나로, 수많은 개발자와 연구자들이 분석해 왔음
    • 그러나 57년 동안 발견되지 않았던 자원 잠금 누락 버그가 자이로 제어 코드에서 확인됨
    • 오류 경로에서 잠금이 해제되지 않아 유도 플랫폼의 재정렬 기능이 비활성화되는 문제
  • JUXT 팀은 AI 기반 명세 언어 AlliumClaude를 이용해 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 ZEROTS 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 ZEROTS LGYRO 명령으로 수동으로 잠금을 해제해야 했음
    • 모든 경로를 기억하고 수동으로 해제 코드를 삽입해야 했음
  • 현대 언어들은 이러한 자원 누락 문제를 구조적으로 방지
    • Go의 defer, Java의 try-with-resources, Python의 with, Rust의 소유권 시스템 등은 자동 해제를 보장
  • 그럼에도 불구하고 CWE-772(자원 해제 누락) 유형의 결함은 여전히 존재
    • 데이터베이스 연결, 분산 잠금, 파일 핸들, 인프라 종료 순서 등은 여전히 프로그래머의 책임
  • Apollo 임무는 모두 성공적으로 귀환했지만, 이 결함은 이후 COMANCHE(사령선)LUMINARY(달 착륙선) 소프트웨어에도 그대로 포함되어 수정되지 않음
  • 57년간 숨겨져 있던 결함은 행위 명세 기반 분석의 중요성을 보여주는 사례임
Hacker News 의견들
  • 나는 Mike Stewart이며, CuriousMarc 채널에서 AGC 복원 프로젝트를 이끌었고 VirtualAGC 공동 관리자임
    이번에 언급된 버그는 실제 존재했던 AGC 소프트웨어의 결함임. 하지만 프로그램 전체 기간 동안 방치된 것은 아니었음. SATANCHE의 3단계 테스트 중 발견되어 L-1D-02로 기록되었고, Apollo 14와 15 사이에 수정되었음
    관련 보고서는 ibiblio 문서 1문서 2에서 확인 가능함
    수정은 단순히 LGYRO를 0으로 만드는 두 줄 추가가 아니라, 코드 구조 재조정과 대기 중인 작업을 깨우는 로직까지 포함함. 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 유튜브 채널을 꼭 보길 권함. 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을 올려, 에뮬레이터에서 진짜로 동작하도록 고쳤고, 두 줄짜리 패치가 버그를 해결하는지도 검증함

    • 이런 식의 “AI 코드”를 자주 봄. 테스트 주도 개발을 흉내 내지만 실제로는 테스트만 통과하는 가짜 코드를 내놓음
      AI 생성 코드는 “이제 완벽하다!”며 멈추는 경향이 있고, 그걸 믿는 사람들이 그대로 배포함. 이게 진짜 문제임
  • 글 자체는 흥미롭지만 LLM이 쓴 듯한 인공적인 느낌이 강함

    • 나에게는 LLM 느낌이 전혀 없었음. 과학 논문 스타일이라서 그런 것 같음
    • Juxt는 예전부터 훌륭한 글을 써왔고, 전문성도 충분함. 그래서 이번 글이 AI 작성일 가능성은 낮다고 봄
    • 참고로 Pangram 분석에 따르면 이 글은 인간이 작성한 것으로 판정됨
    • 하지만 Juxt의 다른 글 중 하나는 실제로 Claude가 작성했다고 명시되어 있음. 해당 글의 마지막 문단에서 밝힘
    • 게다가 Rust와 락 관련 부분은 사실과 다름. 이 댓글에서 지적됨
  • 단 4KB 메모리로 사람을 달에 보낸 소프트웨어에도 아직 미발견 버그가 있다는 건, 작은 코드에도 복잡성이 숨어 있음을 보여줌

    • 메모리가 적을수록 코드 길이와 버그율의 상관관계가 약함. 오히려 복잡도를 압축하려다 버그가 늘어남
    • 이런 말은 그냥 공허한 상투어처럼 들림
  • “코드에서 명세를 도출했다”는 표현은 잘못임. 명세(specification)의 의미를 다시 찾아볼 필요가 있음

    • 사실 그건 단순히 리버스 엔지니어링을 뜻함
  • 기사와 저장소 모두 품질이 낮은 결과물(sloppy)
    저장소 링크를 보면, “재현”이라면서 실제 버그를 실행하지 않고 단순히 “이럴 것이다”라는 출력문만 나열