Kani: Rust 모델 체커가 산업용 프로젝트에서 6개의 미지의 버그를 찾아내다

Kani: A Model Checker for Rust

Rust의 소유권 타입 시스템은 안전한 코드에서 메모리 오류를 방지하지만, unsafe 연산의 건전성, 기능적 정확성, 런타임 패닉 부재와 같은 속성은 컴파일과 별개로 보장되지 않습니다. Kani는 Rust용 오픈소스 모델 체커로, Rust의 MIR(Mid-level Intermediate Representation)을 CBMC의 비트 정밀 검증 엔진으로 컴파일하여 사용자 주석 없이 포괄적인 안전 속성을 자동 검사합니다. 함수 계약, 루프 계약, 양화사, 함수 스터빙을 포함한 사양 언어를 통해 유계 검증을 무계 검증으로 확장합니다. 산업용 Rust 프로젝트 사례 연구에서 계약을 통해 패닉 자유에서 기능적 정확성으로 검증을 업그레이드했고, 이전에 알려지지 않은 6개의 버그를 발견했습니다. Kani는 Rust 표준 라이브러리 검증 캠페인에서 코드 변경당 16,000개 이상의 하네스를 검증하며 프로덕션 CI에서 대규모로 운영됩니다.