Microsoft, Rust 암호 코드 검증 자료 공개…SymCrypt에 Lean·Aeneas 적용

Microsoft Research 공식 블로그에 따르면 회사는 7월 13일 SymCrypt의 Rust 기반 암호 구현을 Lean 형식 증명 프레임워크와 Aeneas 도구체인으로 검증하는 작업을 공개했다. SymCrypt는 Windows, Azure Linux 등 Microsoft 제품과 서비스에서 쓰이는 오픈소스 암호 라이브러리다.

이번 공개의 초점은 테스트와 코드 리뷰만으로는 확인하기 어려운 암호 구현의 정확성을 기계 검증으로 보강하는 데 있다. Microsoft는 암호 알고리즘이 표준 문서의 수학적 설명과 실제 제품 코드 사이에서 최적화, 저수준 비트 연산, 플랫폼별 명령어, 동적 디스패치 같은 차이를 갖기 때문에 별도의 검증 방법이 필요하다고 설명했다.

회사는 NIST 표준이나 RFC 같은 공개 표준을 Lean 명세로 옮기고, Rust 코드의 중간 표현을 Aeneas로 Lean 모델로 변환해 두 결과가 같은 수학적 의미를 갖는지 증명하는 방식을 제시했다. Rust의 소유권과 빌림 규칙은 포인터 별칭과 메모리 생존 기간을 둘러싼 복잡한 추론을 줄이는 데 활용된다.

Microsoft는 공개한 SymCrypt 브랜치에 형식 명세와 증명 자료를 함께 포함했다고 밝혔다. 첫 공개 범위에는 SHA-3와 포스트양자 키 캡슐화 알고리즘 ML-KEM의 Rust 코드에 대한 완전한 증명이 포함됐으며, 이 코드는 현재 Windows 인사이더 빌드에서 사용되고 있다고 설명했다. 회사는 같은 흐름을 AES-GCM, FrodoKEM, ML-DSA 등 다른 Rust 기반 알고리즘으로도 확장하고 있다고 밝혔다.

AI 에이전트도 검증 과정의 보조 수단으로 등장했다. Microsoft는 에이전트가 표준을 Lean 명세로 옮기거나 증명 스크립트를 작성하는 데 도움을 줄 수 있지만, 최종 증명은 Lean 커널이 독립적으로 확인한다고 설명했다. 이는 AI가 생성한 코드나 증명을 그대로 신뢰하는 방식이 아니라, 기계 검증 가능한 산출물로 제한하는 접근이다.

이번 발표는 포스트양자 암호 전환과 보안 소프트웨어 공급망 강화가 맞물리는 시점에 나왔다. 암호 라이브러리는 운영체제와 클라우드, 펌웨어, 메시징 프로토콜의 기반 계층에 해당한다. Microsoft의 접근은 Rust 전환, 형식 검증, AI 보조 증명 작성이 실제 제품 개발 흐름 안에서 결합될 수 있음을 보여주는 사례로 볼 수 있다.

다만 공개된 내용은 Microsoft가 설명한 방법론과 초기 공개 브랜치 기준이다. 검증 범위가 전체 SymCrypt로 얼마나 빠르게 확대되는지, 외부 연구자와 개발자가 증명 자료를 얼마나 재현하고 검토할 수 있는지, 플랫폼별 최적화 코드의 검증 범위가 어디까지인지가 향후 평가 지점으로 남는다.

출처: Microsoft Research https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/
출처: GitHub microsoft/SymCrypt verifiedcrypto 브랜치 https://github.com/microsoft/SymCrypt/tree/feature/verifiedcrypto