57년간 숨어있던 4바이트 버그, Apollo 11 AGC의 리소스 락 누수 분석

Context

Apollo Guidance Computer(AGC)의 자이로 제어 코드 내 공유 락(LGYRO) 관리 결함 발견. 특정 비상 상황에서 락 해제가 누락되는 리소스 락 누수(Resource Lock Leak) 발생. 시스템 재시작 시 메모리 초기화 과정에서 락이 강제 해제되어 결함이 은폐된 구조.

Technical Solution

• 자이로스코프 드리프트 보정 및 별 정렬 시 LGYRO 락을 획득하고 작업 완료 후 해제하는 기본 제어 흐름 설계
• 물리적 클램프로 짐벌을 고정하는 Caging 비상 조치 시 BADEND 루틴을 통해 예외 처리 수행
• BADEND 루틴 내 대부분의 공유 리소스는 정리하나 LGYRO 락 해제 명령 2개(4바이트)가 누락된 로직 설계
• 락 누수 발생 시 이후 모든 자이로 관련 작업이 무한 대기 상태에 빠지며 시스템 전체가 아닌 특정 기능만 마비되는 Silent Failure 구조
• Allium 도구를 활용해 13만 라인의 Assembly 코드를 1.2만 라인의 동작 명세(Behavioral Specification)로 추상화
• 리소스의 획득-보유-해제 생명주기를 모델링하여 모든 실행 경로에서 락 해제 여부를 전수 검증하는 정적 분석 기법 적용

Key Takeaway

단순한 코드 리뷰나 에뮬레이션만으로는 모든 예외 경로의 리소스 생명주기를 검증하기 어려우며, 정형 명세(Formal Specification)를 통한 상태 전이 분석이 필수적임.