Rust에서 확률적 프로그램 검증

요약

본 논문은 기존 검증 프레임워크가 이상적인 언어에 국한되어 상용 코드를 검증하기 어렵다는 문제를 해결하고자 합니다. 이를 위해 Rust 기반의 확률적 프로그램 검증 프레임워크인 Alerus를 제시합니다. Alerus는 Verus를 확장하여, 확률적 오류 크레딧을 도입함으로써 무작위 샘플링 알고리즘의 정확성 검증을 지원합니다.

핵심 포인트

• Rust 기반의 확률적 프로그램 검증 프레임워크 Alerus 제안
• Verus에 확률적 추론 기능을 추가하여 상용 코드 적용 가능하게 함
• 확률적 오류 크레딧(probabilistic error credits)을 사용하여 샘플링 알고리즘 검증 지원
• Rocq에서 완전히 기계화된 건전성 증명 제시