아폴로 11호 가이던스 컴퓨터서 57년만에 숨겨진 버그 발견...AI 지원 형식 검증으로 13만 줄 코드서 자원 관리 결함 찾아
2026년 4월 7일
2분
[한국정보기술신문] 영국 소프트웨어 업체 JUXT가 AI 기반 형식 검증 기술을 사용해 아폴로 11호 가이던스 컴퓨터 코드에서 57년간 발견되지 않았던 버그를 찾아냈다고 7일 발표했다.
13만 줄 어셈블리 코드서 4바이트 버그 발견
JUXT는 Claude AI와 Allium이라는 행동 명세 언어를 활용해 아폴로 가이던스 컴퓨터의 13만 줄 어셈블리 코드를 1만2500줄 사양서로 요약했다. 이 과정에서 자이로스코프 제어 코드의 자원 잠금 해제 누락 버그를 발견했다.
문제는 관성 측정 장치(IMU)가 토크 작업 중 케이지될 때 'LGYRO' 자원 잠금이 해제되지 않아 후속 자이로 정렬 시도가 무한 대기 상태에 빠지는 것이었다. 누락된 코드는 'CAF ZERO'와 'TS LGYRO' 명령어 두 개로 총 4바이트에 불과했다.
MIT 마가렛 해밀턴 팀이 개발한 코드
해당 버그가 발견된 코드는 MIT 계측연구소의 마가렛 해밀턴 팀이 1969년 이전에 작성한 것이다. 아폴로 가이던스 컴퓨터는 2KB 삭제 가능 RAM과 74KB 코어 로프 메모리를 갖춘 1MHz 클럭 시스템이었다.
JUXT CTO 헨리 가너는 "57년간 수천 명의 개발자가 검토하고 학술 논문의 대상이 된 코드에서 첫 번째 문서화된 버그를 발견했다"고 말했다.
달 뒤편에서 발생 시 위험 상황 가능
전문가들은 이 버그가 아폴로 11호가 달 뒤편에 있을 때 발생했다면 사령선의 가이던스 플랫폼이 마비될 수 있었다고 분석했다. 하드 리셋으로 문제를 해결할 수 있지만, 지상 관제센터와 연락이 끊긴 상황에서는 우주비행사들이 진단할 단서가 제한적이었을 것이다.
형식 검증의 효과 입증
이번 발견은 기존 코드 검토나 정적 분석으로는 찾지 못한 체계적 문제를 사양 기반 접근법이 드러낼 수 있음을 보여준다. 파르자드 페제쉬크푸르 박사가 독립적으로 이 버그를 재현해 검증했다.
버그는 공통 취약점 열거(CWE) 분류 체계의 CWE-772번에 해당하는 '자원의 생명주기 종료 후 해제 누락' 결함이다. 현대 프로그래밍 언어들은 defer, try-with-resources, with 문, Rust의 소유권 시스템 등으로 이런 문제를 해결하고 있다.
AI 지원 검증의 새 지평
이번 사례는 AI 지원 형식 사양 생성이 광범위하게 검토된 시스템에서도 결함을 식별할 수 있음을 입증했다. 실행 경로 관점보다는 자원 생명주기 관점에서 문제에 접근해 성과를 거뒀다.
전문가들은 이번 발견이 레거시 시스템과 런타임 관리되지 않는 자원들에 대한 재검토 필요성을 시사한다고 평가했다.
한국정보기술신문 인공지능분과 김성현 기자 news@kitpa.org
![[백준 서비스 종료 ⑧] 백준 이후 어디로 가나...이용자들 대체 플랫폼 찾기 분주](/_next/image?url=https%3A%2F%2Fkitpa.org%2Fstorage%2F41892086-06f3-4c10-99af-4152bdbdff39.webp%23w%3D1920%26h%3D710&w=384&q=75)
