Microsoft는 ML-KEM 및 SHA-3의 Rust 구현에 대한 형식 사양과 증명을 포함하는 SymCrypt 암호화 라이브러리의 브랜치를 오픈소스로 공개했습니다. 이 릴리스는 프로덕션 알고리즘을 안전한 Rust로 작성하고 Aeneas 툴체인을 사용하여 표준에서 파생된 Lean 모델에 대해 검증하는 방법론을 보여줍니다.
- 이 접근 방식은 Aeneas를 사용하여 Rust의 중간 수준 표현을 순수 Lean 모델로 변환하고, Rust의 소유권 규칙을 활용하여 메모리 안전성에 대한 추론을 단순화합니다.
- 형식 사양은 NIST 또는 IETF RFC와 같은 공개 표준에 가깝게 설계되어 공식 벡터에 대한 실행 가능한 테스트와 줄 단위의 인간 검토를 가능하게 합니다.
- 오픈소스화된 브랜치에는 현재 Windows Insider 빌드에서 사용되는 ML-KEM 및 SHA-3 코드에 대한 완전한 증명이 포함되어 있으며, 이 워크플로우를 AES-GCM, FrodoKEM 및 ML-DSA로 확장할 계획입니다.
이 방법론은 Rust의 메모리 안전성 보장과 Lean의 기능적 정확성 증명을 결합하여 2층의 보장을 제공하며, 프로덕션 암호화 알고리즘에 대한 형식 검증의 확장을 목표로 합니다.