수학 증명을 기계적으로 검증하는 증명 보조 도구 Lean에서 지난 7월 하순 커널 건전성(soundness) 버그가 보고되고 수정됐다. Lean과 Z3의 개발자 레오나르도 데 모우라가 공개한 사후 분석에 따르면, 발단은 7월 25일 라마나 쿠마르가 AI의 도움을 받아 만든 콜라츠 추측의 'sorry 없는 반증' 저장소였다. 콜라츠 추측은 아직 아무도 증명하지 못한 미해결 난제인 만큼, 이를 반증했다는 결과물은 그 자체로 의심의 대상이었다. 실제로 이 '증명'은 정당한 것이 아니라 커널이 중첩 귀납 타입(nested inductive type)을 다루는 과정의 결함을 파고든 것이었다. 7월 28일 키란 고피나탄이 이를 거짓(False)을 유도하는 작은 증명으로 축약해 이슈 #14576을 열었고, 보고 한 시간 만에 수정 PR이 올라와 검토를 거쳐 병합됐다.
버그의 정체와 도달 경로
문제의 핵심은 '팬텀 파라미터'에 있다. 커널이 귀납 타입 T의 중첩 항목을 소거할 때, T의 파라미터 중 생성자 필드에 전혀 등장하지 않는 것들은 자동 생성되는 보조 타입에서 사라진다. 그 결과 해당 위치의 인자는 타입 검사를 그대로 빠져나가고, 형(型)이 맞지 않는 항을 그 자리에 끼워 넣으면 커널이 거짓의 증명을 받아들이게 만들 수 있었다. 다만 이 버그는 메타프로그래밍으로 귀납 선언을 커널에 직접 전달할 때만 도달 가능하다. 일반 사용 경로인 프론트엔드(엘라보레이터)는 인자를 검사하기 때문에 형이 맞지 않는 항을 걸러낸다. 데 모우라는 이것이 구현상의 버그일 뿐 Lean의 메타이론에 뚫린 구멍은 아니라는 점을 분명히 했다.
주목할 대목은 이 반증이 독립 검증기까지 통과했다는 사실이다. Lean에는 크리스 베일리가 러스트로 구현한 별도의 커널 nanoda가 있는데, 일주일 전 버전의 nanoda 역시 이 증명을 통과시켰다. 그러나 원인은 서로 무관한 두 개의 버그였다. 공식 커널은 중첩 귀납 타입 지원에서 검사가 빠져 있었고, nanoda는 그 지점은 검사했지만 사영(projection) 노드에서 타입 이름을 확인하지 않는 별개의 결함이 있었다. nanoda 쪽 버그는 제레미 첸이 보고해 Lean 버그가 알려지기 일주일 전에 이미 고쳐진 상태였다. 문제의 증명은 공교롭게도 커널이 결코 들여다보지 않는 표현식이 옛 nanoda가 받아들이던 형태가 되도록 구성돼 있었다.
독립 검증의 의미와 조건
이 우연을 두고 쿠마르는 타이밍이 우연의 일치라고 보면서도 모델이 nanoda 보고를 봤을 가능성을 배제하지는 못한다고 밝혔다. 요아힘 브라이트너는 이런 버그를 찾아낼 만큼 강력한 모델이 등장했기 때문에 타이밍이 겹쳤을 것이라는 가설을 제시했다. 실무적으로 얻을 교훈은 명확하다. 독립 커널로 교차 검증하는 방식은 여전히 유효하다. 이번 공격이 성립하려면 서로 다른 두 구현에 있는 두 개의 별개 버그가 동시에 필요했기 때문이다. 다만 그 안전장치를 신뢰하려면 두 검증기 모두 최신 버전을 써야 한다는 조건이 붙는다. 한편 참조 구현의 귀납 타입 처리를 이식한 lean4lean은 같은 커널 버그의 영향을 받았다.
마리오 카르네이로의 lean4lean은 Lean의 타입 이론을 Lean 안에서 형식화하고 커널이 그 이론을 구현함을 증명하려는 작업인데, 아직 귀납 타입에 대한 일관성 증명은 완성되지 않았고 검증 대상 구현도 공식 커널과 같은 버그를 안고 있었다. 데 모우라는 이 부분의 검증을 마무리하려는 시점에 결국 버그가 발견됐을 것이라고 봤다. 형식 검증이 진행 중인 구성 요소일수록, 검증이 끝나기 전까지는 그 자체가 신뢰의 근거가 될 수 없다는 점을 보여주는 대목이다.
메타프로그래밍을 막자는 제안은 왜 틀렸나
논의 과정에서 이런 공격이 아예 표현되지 못하도록 메타프로그래밍을 제거하거나 제한하자는 의견이 나왔지만, 데 모우라는 이를 방향이 잘못된 처방이라고 못 박았다. 엘라보레이터는 설계상 신뢰되지 않는 컴포넌트이며, 건전성이 신뢰되지 않는 요소가 나쁜 항을 만들지 않으리라는 기대에 의존해서는 안 된다는 것이다. 악의적 증명을 넣으려는 공격자는 .olean 파일을 직접 작성하거나 메모리를 수정하는 식으로 엘라보레이터를 아예 우회할 수 있다. 따라서 커널은 자기 프로세스 안에서 스스로 형이 맞지 않는 선언을 거부해야 하며, 이러한 관심사의 분리와 격리야말로 증명 항(proof term) 방식이 갖는 핵심 장점이라는 설명이다. 검증 계층을 편의를 위해 신뢰 계층과 뒤섞는 순간 안전성의 근거가 무너진다는, 신뢰 컴퓨팅 기반(TCB) 설계의 원칙을 재확인한 셈이다.
수정 이후의 대응도 이어졌다. 익스플로잇과 아서 아제의 비균일 파라미터 사례에 대한 회귀 테스트가 Kernel Arena에 추가됐고, 후속 PR(#14582)은 중첩 항목의 파라미터를 단순히 재검사하는 데 그치지 않고 실제로 파라미터답게 동작하는지까지 확인하도록 했다. 오픈AI의 대니얼 셀삼은 사이버보안에 특화된 AI로 Lean FRO를 도와 커널의 다른 프로그래밍 실수들을 찾아냈는데, 이들 역시 모두 메타프로그래밍으로만 도달 가능했고 모두 nanoda가 잡아냈으며 이미 수정됐다. 커널 불변식 강화 작업도 별도로 진행됐다. comparator.live는 이제 기본으로 nanoda를 실행하고, nanoda는 매일 추적돼 상류 수정 이후에도 lean-eval과 comparator가 최신 상태를 유지한다. 형식 증명 도구조차 구현 버그로부터 자유롭지 않다는 사실, 그리고 그 방어선이 결국 독립 검증기의 다중화와 최신성 유지에 달려 있다는 점은 검증 인프라를 다루는 실무자에게 그대로 적용되는 교훈이다.