애플, 양자 암호화 알고리즘 검증 기술 공개

애플은 미래의 양자 컴퓨터(Quantum Computer)가 야기할 수 있는 위협으로부터 사용자 데이터를 보호하기 위해 ML-KEM 및 ML-DSA와 같은 양자 암호화 알고리즘을 corecrypto에 통합했다. 특히, iMessage, VPN, TLS 네트워킹 등 암호화된 통신(Encrypted Communications)과 관련된 애플리케이션에 우선적으로 적용했다. 이는 데이터 미저장 정책(Zero-Retention Policy)을 통해 보안을 강화하려는 노력의 일환으로, GDPR 규제 준수(GDPR Compliance)를 위한 중요한 단계이다.

애플은 corecrypto의 안전성을 확보하기 위해 형식적 검증(Formal Verification)을 적극적으로 활용했다. 형식적 검증(Formal Verification)은 수학적 증명을 통해 구현의 정확성을 보장하며, 기존의 테스트 방식으로는 발견하기 어려운 미세한 오류(Subtle Bugs)를 찾아낸다. 애플은 이를 통해 ML-KEM 및 ML-DSA 알고리즘의 구현이 FIPS 표준을 준수하는지 확인하고, 제품의 신뢰성을 높였다.

애플은 corecrypto의 특수한 요구 사항을 충족하기 위해 Isabelle, SAW, Cryptol을 포함한 맞춤형 형식적 검증(Formal Verification) 접근 방식을 개발했다. 특히, C 코드와 ARM64 어셈블리 코드 모두를 검증할 수 있도록 지원하며, 코드의 빠른 변경과 최적화를 용이하게 했다. Cryptol-to-Isabelle 변환기를 자체 개발하여 Cryptol 모델을 Isabelle로 변환함으로써, 검증 과정의 효율성을 높였다.

애플은 C로 작성된 알고리즘 구현을 Cryptol로 변환하고, SAW를 사용하여 구현과 모델의 일치성을 검증했다. 이후, Cryptol 모델을 Isabelle로 변환하여 FIPS 명세와의 등가성을 증명했다. ARM64 어셈블리 코드의 경우, C 구현과의 등가성을 증명하여 검증의 정확성을 확보했다. 이러한 과정을 통해 애플은 최적화된 코드(Optimized Code)의 안전성을 보장하고, 잠재적인 보안 취약점을 제거했다.

애플은 형식적 검증(Formal Verification)을 통해 기존 테스트 방식으로는 발견하기 어려웠던 오류를 찾아내고 수정했다. 예를 들어, ML-DSA 구현에서 누락된 단계를 발견하여 잠재적인 오류를 방지했다. 애플은 이러한 검증 결과와 함께 사용한 도구들을 공개하여 암호학 커뮤니티(Cryptographic Community)의 발전을 지원하고, 보안 소프트웨어 개발의 수준을 높이는 데 기여하고 있다.