Rust 표준 라이브러리 검증

Rust의 타입 시스템 (type system)은 많은 종류의 메모리 오류를 방지하지만, 표준 라이브러리는 Miri 하에서의 동적 검사 (dynamic checks)를 포함한 테스트를 통해 정확성을 검증하는 unsafe 코드에 크게 의존하고 있으며, 정적 검증 (static verification)은 부족한 실정입니다. 본 논문에서는 우리가 아는 한 소프트웨어 라이브러리에 대해 보고된 가장 큰 규모의 검증 캠페인을 제시합니다. 이는 Rust 표준 라이브러리에서 포크 (fork)된 검증 저장소 (verification repository)의 지속적 통합 (continuous integration)에 상호 보완적인 검증 도구들을 통합하는 개방형 크라우드소싱 (crowdsourced) 노력입니다. 우리는 이 캠페인의 효과를 분석하고, 일부 정의되지 않은 동작 (undefined behaviors, 예: 범위를 벗어난 접근 (out-of-bounds access), null 및 댕글링 포인터 역참조 (null and dangling pointer dereferences), 초기화되지 않은 메모리 사용 (use of uninitialized memory))에 대한 기계 검증 증명 (machine-checked proofs)의 실질적인 가치를 논의하며, 남은 장애물들을 형식 방법론 (formal-methods) 커뮤니티를 위한 공개 과제로 제시합니다.