아폴로 유도 컴퓨터에서 57년간 숨겨진 버그를 찾다
아폴로 유도 컴퓨터(Apollo Guidance Computer, AGC)는 역사상 가장 많은 검토를 받은 소스코드 중 하나입니다. 수천 명의 개발자가 이 코드를 읽었고, 학계에서는 신뢰성에 관한 논문도 발표했으며, 에뮬레이터는 한 줄씩 명령어를 실행해왔습니다. 그런데 우리는 57년 동안 아무도 발견하지 못한 버그를 찾았습니다. 자이로 제어 코드의 리소스 락 누수인데, 오류 경로에서 발생하면서 유도 플랫폼의 정렬 기능을 조용히 비활성화시키는 결함이었습니다.
우리는 Claude와 오픈소스 행동 명세 언어인 Allium을 사용해서 130,000줄의 AGC 어셈블리 코드를 12,500줄의 명세로 압축했습니다. 명세는 코드 자체에서 도출되었고, 이 과정을 통해 결함의 위치를 정확히 찾을 수 있었습니다.
코드의 여정
AGC의 소스 코드는 2003년 공개되었습니다. Ron Burkey와 자원봉사자들이 MIT 계기 실험실의 인쇄된 목록을 손으로 옮겨 적는 방식으로 코드를 복원한 거죠. 2016년에는 전직 NASA 인턴이었던 Chris Garry의 GitHub 저장소가 트렌드 1위에 올랐습니다. 수천 명의 개발자들이 2KB의 삭제 가능한 메모리와 1MHz 클록을 가진 기계의 어셈블리 언어를 살펴봤습니다.
AGC의 프로그램은 74KB의 코어 로프(core rope) 메모리에 저장되었는데, 이는 손으로 직접 짠 구리선이 자석 코어를 통과하는 방식이었습니다. 선이 코어를 지나가면 1, 우회하면 0이 되는 식이었죠. 이 작업을 수행한 여성들은 내부적으로 "Little Old Ladies"라고 불렸고, 메모리 자체도 LOL 메모리라는 별명이 붙었습니다. 프로그램이 물리적으로 하드웨어에 짜여 있었던 겁니다.
Ken Shirriff는 이 하드웨어를 개별 게이트 수준까지 분석했고, Virtual AGC 프로젝트는 소프트웨어를 에뮬레이션으로 구동하면서 복원된 소스를 원본 코어 로프 덤프와 바이트 단위로 비교 검증했습니다.
우리가 아는 한, 비행 코드에 대한 공식적인 검증(formal verification), 모델 검사(model checking), 정적 분석(static analysis)은 발표되지 않았습니다. 검토는 깊었지만, 특정한 방식의 검토였거든요. 코드를 읽고, 코드를 에뮬레이션하고, 옮겨 적은 내용을 검증하는 식이었습니다.
우리는 다른 접근을 시도했습니다. Allium을 사용해서 관성 측정 장치(Inertial Measurement Unit, IMU) 서브시스템의 행동 명세를 도출했습니다. IMU는 자이로스코프 기반의 플랫폼으로, 우주선이 어느 방향을 향하고 있는지 알려줍니다. 이 명세는 모든 공유 리소스의 생명 주기를 모델링합니다. 언제 획득되고, 언제 반드시 해제되어야 하며, 어느 경로에서 해제되는지 추적하는 거죠.
그 결과 읽기와 에뮬레이션이 놓친 결함이 드러났습니다.
기준점을 잃다
AGC는 LGYRO라는 공유 리소스 락을 통해 IMU를 관리합니다. 컴퓨터가 자이로스코프를 회전시켜야 할 때(플랫폼 드리프트를 보정하거나 별 정렬을 수행할 때), 시작할 때 LGYRO를 획득하고 세 축 모두가 회전한 후에 해제합니다. 이 락은 두 개의 루틴이 동시에 자이로 하드웨어를 놓고 경합하는 것을 방지합니다.
락은 들어올 때 획득되고 나올 때 해제됩니다. 그런데 세 번째 경로가 있는데, 여기서는 락을 해제하지 않습니다.
'케이징'(caging)은 긴급 조치입니다. IMU의 짐벌을 고정하는 물리적 클램프로, 자이로스코프를 손상으로부터 보호하죠. 승무원은 조종석의 보호 스위치로 이를 작동시킬 수 있었습니다.
회전이 정상적으로 완료되면 루틴은 STRTGYR2를 통해 빠져나가고 LGYRO 락이 해제됩니다. 회전 중에 IMU가 케이징되면 코드는 BADEND라는 루틴을 통해 빠져나가는데, 여기서는 락을 해제하지 않습니다. 두 개의 명령어가 빠져있습니다:
CAF ZERO
TS LGYRO단 4바이트입니다.
LGYRO가 고착되면, 그 이후 자이로를 회전시키려는 모든 시도는 락이 잡혀 있는 것을 발견하고, 절대 오지 않을 웨이크 신호를 기다리며 대기 상태에 빠집니다. 미세 정렬, 드리프트 보정, 수동 자이로 회전, 모두 차단됩니다.
1969년 7월 21일, Neil Armstrong과 Buzz Aldrin이 달 표면을 걸을 때, Michael Collins는 사령선 Columbia에서 혼자 궤도를 돌고 있었습니다. 2시간마다 그는 달 뒤로 사라져 지구와 무선 통신이 두절되었습니다. 그는 자신의 저서 《Carrying the Fire》에 이렇게 썼습니다. "나는 지금 혼자다, 정말로 혼자고, 알려진 모든 생명으로부터 완전히 고립되어 있다. 나는 '그것'이다. 계산해본다면, 달 저쪽에는 30억 플러스 2, 이쪽에는 1 플러스 신은 아시는 누군가가 있을 것이다."
매 통과마다 그는 프로그램 52(P52)를 실행했습니다. 이것은 별 관측 정렬로, 유도 플랫폼이 올바른 방향을 향하도록 유지해줍니다. 플랫폼이 드리프트되면, 지구로 돌아오는 엔진 분사가 잘못된 방향을 가리킬 테니까요.
무선 침묵 속에서
버그가 어떻게 나타났을 수 있는지 생각해봅시다.
Collins는 방금 하단 장비실의 광학 스테이션에서 별 관측을 마치고 최종 명령을 입력했습니다. 컴퓨터는 세 축 모두에 보정을 적용하기 위해 자이로스코프를 회전시키고 있습니다.
그는 협소한 조종석을 지나 주 패널로 돌아가는데, 뒤집개로 보호된 케이지 스위치 근처를 지나갑니다. 팔꿈치가 커버를 건드려 스위치를 작동시킵니다. 코드는 이를 우아하게 처리합니다. CAGETEST라는 루틴이 케이징을 감지하고 회전을 중단하고 빠져나옵니다. P52가 실패하고 그는 이유를 이해합니다. 케이징이 보정을 방해했던 거죠. 그는 IMU를 언케이징하고 다시 광학 스테이션으로 돌아가 정렬합니다.
새로운 P52를 시작합니다. 프로그램이 멈춥니다.
경보도 없고, 프로그램 표시등도 켜지지 않습니다.