AI와 명세 언어를 사용하여 아폴로 11 유도 컴퓨터 코드에서 미등록 버그 발견

역사상 가장 면밀히 검토된 코드베이스에서 버그 찾기

아폴로 유도 컴퓨터(AGC) 코드는 2003년부터 공개되었으며, MIT 계측 연구소의 인쇄 목록에서 전사되었습니다. 2016년 크리스 개리의 GitHub 저장소가 바이럴되면서 수천 명의 개발자들이 2K의 지울 수 있는 RAM과 1MHz 클록을 가진 하드웨어에서 실행되는 이 어셈블리 코드를 검토했습니다. 이러한 면밀한 검토에도 불구하고, 비행 코드에 대한 형식 검증, 모델 검사 또는 정적 분석은 지금까지 발표된 바 없었습니다.

버그: 자이로 제어의 자원 잠금 누수

버그는 관성 측정 장치(IMU) 하위 시스템에 있으며, 이는 우주선이 어느 방향을 향하고 있는지 알려주는 자이로스코프 기반 플랫폼을 관리합니다. AGC는 LGYRO라는 공유 자원 잠금을 통해 IMU를 관리합니다. 컴퓨터가 자이로스코프에 토크를 가해야 할 때(플랫폼 드리프트를 수정하거나 별 정렬을 수행하기 위해), 시작 시 LGYRO를 획득하고 세 축 모두에 토크가 가해지면 이를 해제합니다.

문제는 '케이징' 중에 발생합니다. 이는 물리적 클램프가 IMU의 김벌을 고정하여 자이로스코프를 손상으로부터 보호하는 비상 조치입니다. 토크가 정상적으로 완료되면, 루틴은 STRTGYR2를 통해 종료되고 LGYRO 잠금이 해제됩니다. 그러나 토크가 진행 중일 때 IMU가 케이징되면, 코드는 BADEND라는 루틴을 통해 종료되는데, 이 루틴은 잠금을 해제하지 않습니다.

두 개의 명령어가 누락되었습니다: CAF ZERO TS LGYRO - 단 4바이트입니다. LGYRO가 고정되면, 이후 자이로에 토크를 가하려는 모든 시도는 잠금이 유지된 상태를 발견하고, 결코 오지 않을 깨움 신호를 기다리며 슬립 상태에 들어가고, 멈춥니다. 이는 미세 정렬, 드리프트 보상, 수동 자이로 토크를 비활성화할 것입니다.

발견 방법: AI와 행동 명세

연구진은 클로드와 그들의 오픈소스 행동 명세 언어인 Allium을 사용하여 13만 줄의 AGC 어셈블리를 12,500줄의 명세로 정제했습니다. 이 명세는 모든 공유 자원의 수명 주기를 모델링합니다: 언제 획득되고, 언제 해제되어야 하며, 어떤 경로에서인지. 이 접근 방식은 읽기와 에뮬레이션으로는 놓쳤던 결함을 표면화했습니다.

명세는 코드 자체에서 파생되었으며, 이 과정은 결함을 직접 가리켰습니다. 이는 코드 읽기, 코드 에뮬레이션, 전사 검증에 초점을 맞춘 이전의 검토와는 다른 접근 방식을 나타냅니다.

역사적 맥락과 잠재적 영향

1969년 7월 21일, 닐 암스트롱과 버즈 올드린이 달 표면을 걸을 때, 마이클 콜린스는 커맨드 모듈 컬럼비아에서 혼자 궤도를 돌고 있었습니다. 그는 두 시간마다 달 뒤편으로 사라져 지구와의 무선 통신이 끊겼습니다. 각 통과 동안 그는 항법 플랫폼이 올바른 방향을 가리키도록 유지하는 별 관측 정렬인 프로그램 52를 실행했습니다. 플랫폼이 드리프트되면, 그를 집으로 데려올 엔진 연소가 잘못된 방향을 가리킬 것입니다.

이 버그는 콜린스가 컴퓨터가 자이로스코프에 토크를 가하는 동안 실수로 케이지 스위치를 작동시켰을 경우 나타났을 수 있습니다. 코드는 케이지를 감지하고, 토크를 포기하고, 종료함으로써 우아하게 이를 처리했을 것입니다. 그러나 P52 정렬은 실패했을 것이고, 항법 플랫폼은 기준을 잃었을 수 있습니다.