57년 만에 발견된 아폴로 11호 유도 컴퓨터(AGC)의 숨겨진 버그

AGC 코드에서 발견된 버그는 자원 잠금(Resource Lock) 문제로, 짐벌(Gimbal) 잠금 시 자원 해제가 누락되어 발생한다. 특히, 'Caging'이라는 비상 절차 수행 시, LGYRO 잠금(Lock)이 해제되지 않아 이후 짐벌 정렬(Gyro Alignment)이 불가능해진다. 이는 1969년 아폴로 11호 임무 중 발생할 수 있는 치명적인 상황을 초래할 수 있었다. 해당 버그는 코드의 방어적 설계(Defensive Coding)로 인해 쉽게 감지되지 않았다.

저자는 AI 기반 명세 언어(Specification Language)인 Allium을 사용하여 AGC 코드의 동작을 명세화했다. Allium은 코드의 행동 명세(Behavioral Specification)를 추출하여, 자원(Resource)의 생명주기를 모델링한다. 이를 통해, 코드의 모든 실행 경로를 분석하고, 자원 해제 누락과 같은 잠재적 결함을 발견할 수 있었다. AI 기반 분석(AI-powered Analysis)은 기존의 코드 검토 및 에뮬레이션 방식으로는 발견하기 어려웠던 버그를 찾아내는 데 기여했다.

이번 사례는 소프트웨어 검증(Software Verification)의 중요성을 강조한다. 기존의 코드 검토, 에뮬레이션, 그리고 트랜스크립션 검증(Transcription Verification)만으로는 모든 잠재적 결함을 찾아내기 어렵다는 것을 보여준다. Allium과 같은 도구를 활용한 형식적 검증(Formal Verification)은 코드의 정확성을 높이고, 잠재적인 오류를 사전에 방지하는 데 기여할 수 있다. 소프트웨어 엔지니어링(Software Engineering)의 발전은 더욱 정교한 검증 방법을 요구한다.

커뮤니티에서는 AI 기반 도구의 정확성(Accuracy)과 신뢰성(Reliability)에 대한 의문이 제기되었다. 특히, 명세가 코드 자체에서 파생된 경우, 모델이 코드의 의도를 제대로 파악하지 못할 수 있다는 지적이 있었다. 또한, AI가 발견한 버그의 실제성(Actuality)에 대한 검증 필요성도 강조되었다. 하지만, AI를 활용한 코드 분석이 새로운 버그 발견(New Bug Discovery) 가능성을 열었다는 점에는 긍정적인 평가가 이어졌다.