Amazon의 양자내성 암호를 검증하고 최적화하는 방법

RSA와 ECC는 양자컴퓨터가 충분히 강력해지면 깨질 수 있다. 그래서 지금 암호문을 저장해 뒀다가 나중에 푸는 store-now-decrypt-later 공격에 대비하려면, 미리 post-quantum cryptography(PQC) 로 전환해야 한다.

Amazon은 NIST의 FIPS-203 표준인 ML-KEM을 대상으로, 오픈소스이면서도 형식 검증(formal verification) 과 성능 최적화를 동시에 만족하는 구현체 mlkem-native를 만들었다. 목표는 보안을 높이면서도, 고객 경험과 유지보수성을 해치지 않는 것이었다.

핵심은 단순한 C 레퍼런스 코드와 연구 수준의 최적화 기법을 하나의 생산용 코드베이스로 합친 점이다. 이를 위해 frontend는 ML-KEM의 고수준 로직을 담당하고, backend는 성능 민감한 연산을 맡는 모듈식 구조를 채택했다. AArch64, x86_64, RISC-V64용 백엔드와 기본 C 구현을 모두 제공해, 아키텍처별로 빠른 경로를 넣어도 전체 구조는 유지된다.

검증은 두 갈래로 진행된다.

• CBMC로 C 코드의 memory safety와 type safety를 증명한다.
• 각 함수에 기계/사람이 읽을 수 있는 contract를 붙여, 버퍼 오버플로와 산술 오버플로가 없음을 자동으로 확인한다.

특히 ML-KEM의 lazy modular arithmetic는 16비트 정수 범위를 넘지 않도록 최악의 경우 경계를 정확히 추적해야 한다. 평균값이 아니라 최악의 경우를 기준으로 봐야 하므로, 수작업 검토는 느리고 오류에 취약하다. CBMC는 이런 경계 추적을 자동화해, 복잡한 저수준 산술에서도 안전성을 확보한다.

가장 성능이 중요한 Keccak과 NTT는 손으로 짠 최적화 어셈블리로 구현했지만, 검증까지 포기하지 않았다. Amazon은 SLOTHY로 마이크로아키텍처별 스케줄링과 레지스터 할당을 최적화하고, HOL Light와 s2n-bignum으로 AArch64와 x86_64 어셈블리의 함수적 정확성을 증명한다. SLOTHY로 다시 최적화해도 증명은 instruction ordering과 register allocation에 독립적이어서, 성능 개선이 검증 부담으로 이어지지 않는다.

투명성도 강조한다. SOUNDNESS.md에는 무엇이 증명됐고, 무엇을 가정했으며, 남은 위험이 무엇인지 정리해 뒀다. 검증 도구와 아티팩트도 오픈소스로 공개해, 외부에서도 같은 결론을 재현할 수 있게 했다.

성과도 분명하다. mlkem-native는 AWS-LC에 통합됐고, EC2 인스턴스들에서 레퍼런스 구현 대비 초당 연산 수가 2.0배에서 2.4배까지 늘었다. 결론적으로 Amazon은 형식 검증, 최적화, 유지보수성을 서로 충돌하지 않는 목표로 증명해 보였다.