AI, 형식 검증된 코드에서 버그를 찾아내다!

본문은 형식 검증(Formal Verification)이 코드의 정확성을 보장하지만, 검증 범위(Verification Scope) 밖의 문제는 여전히 발생할 수 있음을 보여준다. 특히, Lean으로 검증된 zlib 구현에서 발견된 힙 버퍼 오버플로우(Heap Buffer Overflow)는 런타임(Runtime) 자체의 문제로, 형식 검증이 적용되지 않은 부분에서 발생했다. AI 기반 퍼징(Fuzzing) 도구는 이러한 사각지대(Blind Spot)를 효과적으로 공략하여, 검증된 코드에서도 취약점을 찾아내는 데 기여했다.

발견된 힙 버퍼 오버플로우(Heap Buffer Overflow)는 Lean 4 런타임의 `lean_alloc_sarray` 함수에서 발생했다. 이 함수는 바이트 배열(ByteArray) 할당 시, 크기 계산 과정에서 정수 오버플로우(Integer Overflow)가 발생하여 작은 버퍼를 할당하는 문제를 가지고 있었다. 이로 인해, `lean_io_prim_handle_read` 함수를 통해 데이터를 읽어올 때, 버퍼 오버플로우가 발생할 수 있었다. 이는 안전하지 않은 메모리 할당(Unsafe Memory Allocation)의 전형적인 사례로, 모든 Lean 4 프로그램에 영향을 미칠 수 있는 심각한 문제였다.

저자는 Claude AI 에이전트를 활용하여 lean-zip 코드를 퍼징(Fuzzing)했다. 16개의 병렬 퍼저(Fuzzer)를 통해 1억 회 이상의 실행을 수행했으며, AFL++, AddressSanitizer, Valgrind, UBSan 등의 도구를 사용하여 취약점을 탐지했다. 특히, AI 에이전트의 자율적인 취약점 탐지 능력(Autonomous Vulnerability Discovery)은 기존의 수동적인 방식보다 훨씬 효율적임을 보여주었다. 이는 AI가 소프트웨어 보안 분야에서 중요한 역할을 할 수 있음을 시사한다.

lean-zip의 Archive.lean 모듈에서 ZIP 아카이브 파서(Parser)의 `readExact` 함수는 압축된 크기(compressedSize)를 검증 없이 사용했다. 이로 인해, 악의적인 ZIP 파일을 통해 서비스 거부(DoS) 공격이 가능했다. 특히, 압축된 크기를 파일 크기보다 크게 설정하면, 메모리 할당 오류(Memory Allocation Error)가 발생하여 프로그램이 종료된다. 이는 입력값 검증 부재(Input Validation Failure)로 인한 전형적인 보안 취약점이며, 형식 검증의 적용 범위를 벗어난 부분에서 발생했다.

본 사례는 형식 검증의 성공 여부가 신뢰할 수 있는 컴퓨팅 기반(Trusted Computing Base)의 정확성에 달려 있음을 보여준다. Lean의 경우, 런타임(Runtime) 자체가 TCB에 해당하며, 런타임에 버그가 존재하면 형식 검증의 의미가 퇴색된다. 따라서, TCB의 안전성을 확보하는 것이 소프트웨어 보안의 핵심 과제이다. 이는 보안 취약점(Security Vulnerability)을 줄이기 위한 근본적인 접근 방식의 중요성을 강조한다.