Lean Kernel Soundness Bug #14576 Postmortem

Overview

Lean은 Collatz conjecture에 대한 AI 지원 반증(purported AI-assisted disproof)을 포함하여, 잘못된 증명을 구성할 수 있게 했던 커널의 건전성 버그(#14576)를 해결했습니다. 이 버그는 Lean의 근본적인 메타 이론의 결함이 아니라, 커널이 중첩된 귀납적 타입(nested inductive types)을 처리하는 방식에서의 구현 오류였습니다. 이는 한 사용자가 중첩된 귀납적 타입의 phantom parameters를 커널이 제대로 검증하지 못하는 점을 악용한, sorry-free Collatz conjecture 반증을 게시한 후 발견되었습니다.

Technical Root Cause: Nested Inductive Type Handling

건전성 버그는 커널이 매개변수 Ds를 가진 귀납적 타입 T 하의 중첩된 발생(nested occurrence)을 제거(eliminate)할 때 발생했습니다. 만약 이 매개변수들이 "phantom"(즉, 생성자 필드에서 언급되지 않음)이라면, 생성된 보조 타입에서 사라지게 됩니다. 이로 인해 잘못된 타입의 인자가 타입 검사를 통과하여 False를 증명하는 데 사용될 수 있었습니다.

결정적으로, 이 버그는 귀납적 선언을 커널로 직접 보내는 메타프로그래밍을 통해서만 도달할 수 있었습니다. Lean 프론트엔드(the elaborator)는 자체적인 검사를 수행하며 잘못된 타입의 항(term)을 잡아냈겠지만, 설계상 elaborator는 신뢰할 수 없으므로 커널이 건전성의 유일한 진실의 원천(sole source of truth)으로 남아야 합니다.

Failure of Independent Verification (nanoda)

독립적인 검사기(independent checker)를 사용했음에도 불구하고, Rust 기반의 Lean 독립 커널인 nanoda의 특정 버전이 이 취약점을 통과했습니다. 이는 두 가지 별개의 버그가 우연히 일치했기 때문입니다:

Lean Kernel Bug: 중첩된 귀납적 타입 지원에서의 검사 누락.
nanoda Bug: 투영 노드(projection node)에서의 타입 이름을 검증하지 못함.

취약점을 악용한 코드가 Lean 커널이 무시한 표현식을 정확히 nanoda의 이전 버전이 수용하는 방식으로 작성되었기 때문에, 증명은 두 검사기를 모두 통과했습니다. 이는 독립 커널이 강력한 보안 계층을 제공하지만, 두 구현체가 모두 최신 상태를 유지해야만 효과적임을 보여줍니다.

Remediation and Kernel Hardening

버그 #14576의 발견 이후, Lean FRO (Formalization Effort)는 여러 강화 조치를 시행했습니다:

Immediate Fixes and Regression Testing

Patch Release: 보고 후 한 시간 만에 수정 패치가 배포되었습니다 (#14577).
Kernel Arena: 취약점 및 관련 non-uniform-parameter 사례에 대한 회귀 테스트가 Kernel Arena에 추가되었습니다.
Parameter Validation: PR #14582가 도입되어, 커널이 중첩된 발생의 매개변수가 단순히 재타입 검사를 하는 대신 실제로 매개변수로서 동작하는지 검증하도록 보장합니다.

AI-Driven Security Auditing

Lean FRO는 OpenAI의 Daniel Selsam과 협력하여, 사이버 보안에 특화된 AI를 사용하여 커널의 추가적인 프로그래밍 오류를 찾아냈습니다. 이 노력은 여러 다른 버그들(PRs #14607, #14608, #14609, #14613, #14615, #14616)를 발견했으며, 모두 수정되었습니다. 특히, 이 버그들은 nanoda에 의해 포착되었는데, 이는 독립 커널의 가치가 여전히 높음을 나타냅니다.

Infrastructure Improvements

Hardened Invariants: 커널 불변량(kernel invariants)을 강화하기 위해 새로운 PR들 (#14621, #14631, #14632)이 구현되었습니다.
Continuous Integration: comparator.live는 이제 기본적으로 nanoda를 실행하며, 참조 구현체와 독립 검사기 간의 동기화를 보장하기 위해 이를 매일 추적합니다.

Discussion and Community Insights

커뮤니티 구성원과 연구자들은 이 사건의 함의에 대해 몇 가지 사항을 제점을했습니다:

"검증된 결과는 절대적이고 깨지지 않는 보증이 아니라, (1) 건전성 문제의 표면적 영역이 고통스럽게 최소화되었고 (2) 발생한 건전성 문제는 매우 심각하게 다뤄져지고 신속하게 수정된다는 점에서 매우 강력한 보증이라는 관점으로 보는 것이 중요하다고 생각합니다."

다른 논의들은 AI에 의한 "reward hacking"의 가능성에 초도점을 맞추었습니다. 즉, 모델이 수학적 문제를 해결하는 대신 커널 버그를 악용하여 결과를 "증명"하는 것이 더 쉽다고 판단할 수 있습니다. 이는 AI가 생성한 형식적 증명(formal proofs)이 검사기를 통과하더라도, 검사기 자체가 구현 버그를 포함하고 있다면 AI 생성 증명을 암시적으로 신뢰할 수 없음을 강조합니다.