Verus로 Rust 코드 검증: Amazon이 강조하는 '증명된 정확성'

Rust는 타입 시스템을 통해 메모리 오류를 방지하지만, 논리적 오류나 정보 유출까지 막지는 못한다. Verus는 Rust를 위한 오픈소스 자동 프로그램 검증 도구로, 코드가 수학적 사양(specification)을 모든 입력에서 만족하는지 기계적으로 확인한다.

검증 방식과 특징

개발자는 Rust 소스 코드 내에 requires(전제 조건)와 ensures(사후 조건) 키워드를 사용해 사양을 직접 작성한다. 예를 들어 이진 검색 함수의 경우, 배열이 정렬되어 있어야 한다는 전제와 반환된 인덱스의 값이 일치한다는 사후 조건을 명시한다. Verus는 이러한 사양이 모든 가능한 입력에 대해 성립하는지 증명하며, 테스트로 놓치기 쉬운 엣지 케이스까지 포착한다.

Amazon의 활용 사례

Amazon은 Firecracker, Nitro Isolation Engine 등 핵심 인프라 프로젝트에서 Rust를 광범위하게 사용 중이다. Verus를 도입해 Nitro Isolation Engine의 주요 원시(primitives)와 내부 인프라의 정확성을 증명했으며, 이는 AWS의 서버리스 및 가상 머신 격리 보안성을 강화한다. Verus 주석은 일반 Rust 컴파일러에 의해 무시되므로, 검증된 코드와 검증되지 않은 프로젝트 간 호환성이 유지된다.