AI, Lean으로 검증된 코드에서 버그를 찾아내다!
Lean을 사용해 zlib 구현을 검증했으나, AI 기반 퍼징을 통해 런타임 버그(Runtime Bug) 발견
검증된 코드 자체에는 버그가 없었지만, Lean 런타임(Lean Runtime)과 압축 해제 파서(Archive Parser)에서 취약점 발견
AI 에이전트(AI Agent)의 버그 탐지 능력 향상으로, 검증된 코드의 안전성에 대한 새로운 시각 제시
검증의 범위(Scope of Verification)와 신뢰성(Reliability)에 대한 근본적인 질문을 제기하며, spec의 중요성 강조
Lean 검증의 한계와 런타임 버그
본문에서는 Lean을 사용한 zlib 구현의 검증 성공에도 불구하고, Lean 런타임(Lean Runtime) 자체의 힙 버퍼 오버플로우(Heap Buffer Overflow) 취약점을 발견한 사례를 제시한다. 이는 Lean의 검증이 런타임의 정확성을 전제로 하기 때문에 발생한 문제로, 검증된 코드의 안전성을 보장하기 위해서는 신뢰할 수 있는 기반(Trusted Computing Base)의 중요성을 강조한다. 특히, 런타임의 C++ 코드에서 발생한 버그는 모든 Lean 4 프로그램에 영향을 미칠 수 있다는 점을 지적한다.
AI 기반 퍼징(Fuzzing)의 역할
저자는 AI 에이전트를 활용하여 퍼징(Fuzzing) 실험을 진행, 1억 회 이상의 실행을 통해 버그를 찾아냈다. 이는 AI가 취약점 탐지(Vulnerability Discovery)에 효과적임을 보여주는 사례로, 특히 검증된 코드에서 예상치 못한 버그를 발견했다는 점에서 주목할 만하다. AI 기반의 자동화된 테스트는 기존의 검증 방식으로는 발견하기 어려운 취약점을 찾아내는 데 기여할 수 있으며, 소프트웨어 보안(Software Security) 분야에서 중요한 역할을 할 것으로 예상된다.
스펙(Spec)의 중요성 및 완전성 문제
lean-zip의 압축 해제 파서(Archive Parser)에서 발생한 서비스 거부(Denial-of-Service) 취약점은 검증의 범위가 스펙(Spec)에 국한된다는 점을 보여준다. 압축 해제 파서가 검증되지 않아, 헤더의 압축 크기를 검증 없이 사용함으로써 메모리 할당 오류가 발생했다. 이는 스펙의 완전성(Spec Completeness)이 얼마나 중요한지를 보여주는 사례이며, 검증 과정에서 스펙의 정확성과 완전성을 확보하는 것이 중요함을 시사한다.
검증 도구의 신뢰성 및 한계
본문은 Lean과 같은 형식 검증 도구의 신뢰성에 대한 근본적인 질문을 제기한다. Lean은 코드의 정확성을 증명하는 데 유용하지만, 런타임과 같은 신뢰할 수 있는 기반(Trusted Computing Base)의 버그는 검증의 범위를 벗어난다. 또한, 스펙의 오류는 검증된 코드의 안전성을 보장하지 못한다. 따라서, 검증 도구의 사용과 함께 다양한 테스트 기법(Testing Techniques)과 지속적인 검증(Continuous Verification)을 병행하여 소프트웨어의 안전성을 확보해야 한다.
