Reddit

Towards formal verification: mbrotli and mzstd

Brotli·Zstandard Rust 코덱, RFC 일부를 Lean으로 증명…디코더 전체는 과제

mbrotli와 mzstd가 Brotli·Zstandard RFC 규칙을 따르는지 일부 함수에 대해 Lean 4로 기계 검증하기 시작했습니다. 증명은 디코더 전체나 Brotli 블록 전환 규칙까지 다루지 않으며, Rust 코드와 증명 사이에는 번역기의 의미 보존 등 신뢰 가정이 남습니다.

본문

mbrotli와 mzstd 개발진이 두 Rust 코덱의 일부 함수에 대해 RFC 7932·8878을 기준으로 Lean 4 기계 검증을 시작했습니다. 기존 C 라이브러리 비교와 메모리 안전성 검사로는 규격 준수를 보장하기 어렵다는 점이 배경입니다. 현재 증명은 일부 코드에 한정되며 디코더 전체와 Brotli 블록 전환 규칙은 후속 과제로 남았습니다.

두 라이브러리는 Google Brotli 1.2.0과 zstd 1.5.7을 기준으로 차등 테스트를 하고 AFL++·ClusterFuzzLite 퍼징, Miri, AddressSanitizer도 사용합니다. 하지만 기준이 되는 C 라이브러리와 Rust 코드가 같은 규격 오류를 공유하면 두 구현의 결과가 일치해도 RFC 위반을 가려내지 못합니다. 글은 C Brotli 디코더가 단일 블록 유형에서 허용되는 블록 수를 넘긴 입력을 처리한 CVE-2026-111497 사례를 듭니다. mbrotli 0.5.16도 같은 규격 위반 입력을 받아들였고, 안전한 Rust 코드여서 메모리 손상 대신 잘못된 입력을 거부하지 않는 문제로 나타났습니다. mbrotli 0.5.17에서 수정했습니다.

지금 증명한 범위

mbrotli에서는 거리 코드, 마지막 거리 링, 삽입·복사 길이 코드와 명령어 패킹 등을 다룹니다. mzstd에서는 프레임·블록 헤더, 시퀀스 수와 길이·오프셋 코드표, 기본 분포, 반복 오프셋 규칙과 FSE 상태 등을 증명했습니다. 증명은 각 함수가 RFC가 정한 값을 계산하는지, 인코더가 기록한 값을 디코더가 되읽는지, 명시된 입력 조건에서 오버플로·잘못된 인덱스 접근·패닉이 발생하지 않는지 확인합니다.

현재 범위는 코덱 전체가 아니라 선정된 함수입니다. 비트 읽기·쓰기, 접두 코드와 허프만 코드, FSE 테이블, 컨텍스트 맵과 사전 변환 등이 남아 있습니다. CVE가 드러낸 Brotli의 블록 유형·블록 수 규칙도 아직 증명 대상에 포함되지 않았습니다. 개발진은 Lean으로 RFC를 옮긴 참조 디코더를 만들고, Rust 디코더가 그 참조 구현의 결과를 내는 정련 증명을 마쳐야 디코더 전체를 검증했다고 부를 수 있다고 설명합니다. SIMD 경로와 Google Brotli·zstd와의 바이트 단위 일치는 차등 테스트와 퍼징으로 계속 다룹니다. RFC가 매치 탐색, 블록 분할, 비용 모델을 정하지 않으므로 바이트 단위 결과의 동일성은 RFC 증명 범위에 들어가지 않습니다.

증명은 Rust 코드와 어떻게 연결되나

Charon이 Rust 컴파일러의 MIR에서 지정 함수와 그 함수가 호출하는 코드를 추출하고, Aeneas가 이를 Lean으로 번역합니다. 번역 결과를 손으로 수정하지 않으며 CI가 Rust 코드에서 번역을 다시 생성해 저장된 결과와 대조한 뒤 증명을 빌드합니다. 개발진은 mbrotli와 mzstd 코드에서 각각 산술 값을 바꿔 번역 차이가 감지되고 관련 증명이 실패하는 사례를 제시했습니다.

이 절차는 손으로 만든 별도 코드 모델을 증명하는 방식보다 실제 Rust 함수와 증명을 직접 연결합니다. 다만 개발진이 밝힌 가장 큰 신뢰 가정은 Charon과 Aeneas가 MIR을 충실히 번역한다는 점입니다. 코드 변형 검사는 이 가정을 시험하지만 증명하지는 않습니다. Charon이 보는 nightly MIR과 릴리스 빌드의 일치, 일부 표준 라이브러리 함수의 손작성 모델, RFC를 Lean으로 옮긴 내용도 신뢰 범위에 포함됩니다.

자료: M-Compressors / 정리·해설: Trawling

참고 자료

원문 보기 ↗토론 보기 ↗