Microsoft：AI 에이전트와 Lean으로 SymCrypt의 Rust 암호화를 형식 검증

하나가 아닌 두 개의 보증 레이어

형식 검증은 코드가 명세서에 따라 정확하게 동작한다는 수학적 증명입니다——테스트된 경우뿐만 아니라 모든 가능한 입력에 대해. Microsoft는 SymCrypt——Windows, Azure 및 기타 제품을 지원하는 기반 암호화 라이브러리——에 이중 보호를 내장했습니다: Rust 언어는 메모리 관리와 관련된 오류의 전체 클래스를 제거하고（메모리 안전 버그）, Lean 증명 보조 도구는 기능적 정확성을 확인합니다——알고리즘이 표준이 요구하는 대로 정확하게 작동하는지.

Lean은 자체 신뢰할 수 있는 커널을 통해 수학적 증명을 검증하는 도구입니다. 선택된 시나리오를 다루는 단위 테스트와 달리, Lean 증명은 절대적으로 모든 가능한 입력을 다룹니다. 이 두 레이어의 결합은 검증된 코드를 기존 접근법보다 훨씬 더 강력하게 만듭니다.

이미 검증된 것은?

Microsoft는 SHA-3（널리 사용되는 해시 알고리즘）과 ML-KEM——NIST가 2024년에 표준화한 양자 이후 키 교환 알고리즘——의 검증된 코드를 발표했습니다. ML-KEM은 특히 중요합니다. 오늘날 대부분의 인터넷 트래픽을 보호하는 RSA와 ECDH를 해독할 수 있는 양자 컴퓨터의 공격을 견딜 수 있도록 설계되었기 때문입니다.

계획된 것으로는 AES-GCM（대칭 암호화）, FrodoKEM, ML-DSA——또 다른 두 양자 이후 알고리즘도 있습니다. 이 모든 알고리즘의 공통점은 복잡성과 오류의 높은 비용입니다: 암호화의 구현 결함은 일반적으로 프로그램 충돌이 아니라 악용 가능한 조용한 취약점을 만들어냅니다.

AI 에이전트가 증명 작성을 가속화

암호화 코드에 대한 Lean 증명 작성은 느리고 까다롭습니다. Microsoft는 AI 에이전트를 사용하여 이 과정을 가속화합니다: 에이전트가 증명 후보를 제안하면 Lean의 신뢰할 수 있는 커널을 통해 독립적으로 검증됩니다. 일반적인 코드 생성과의 핵심 차이는 AI 출력이 수학적 검사를 통과해야 한다는 것——정확해 보이는 것만으로는 충분하지 않습니다. 이는 AI 에이전트의 오류가 눈에 띄지 않게 통과할 수 없음을 의미합니다.

SymCrypt와의 통합은 이 접근법이 단순한 학문적 실험이 아니라 오늘날 이미 실용적인 의미를 가지게 합니다. Microsoft가 사용하는 툴체인——Aeneas——은 Rust 코드를 Lean이 분석할 수 있는 형태로 변환하여 프로덕션 코드와 형식적 방법 사이의 간극을 연결합니다.