Apple corecrypto 형식 검증 청사진

출처: Hacker News

Apple 보안 엔지니어링 및 아키텍처(SEAR)와 하드웨어 기술 형식 검증 팀이 작성

iMessage에서 양자 보안 암호화 도입은 미래 양자 컴퓨터가 초래할 위협으로부터 Apple 사용자를 보호하기 위한 중요한 보안 전환의 시작을 알렸습니다. 모든 Apple 플랫폼에 걸쳐 이 새로운 세대의 알고리즘을 대규모로 배포하려면 높은 확신이 필요하므로, 구현의 수학적 정확성을 증명하기 위해 엄격한 새로운 형식 검증 방법을 개발했습니다. 이번 주에 공개된 corecrypto와 함께, 우리는 양자 보안 ML‑KEM 및 ML‑DSA 알고리즘 구현과 — FIPS 203 및 FIPS 204 사양에 충실함을 보장하기 위해 만든 수학적 증명 — 을 전문가들의 독립적인 평가를 위해 공개합니다. 또한, 중요한 소프트웨어의 신뢰성을 보장하기 위한 최첨단 기술을 더욱 발전시키고자, 우리는 해당 알고리즘의 널리 배포된 생산 구현에 대해 알려진 가장 강력한 정확성 결과를 달성하기 위해 만든 형식 검증 라이브러리와 도구도 공개합니다.

2024년에 우리는 Apple 운영 체제의 기본 암호화 라이브러리인 corecrypto에 포스트‑양자 암호화를 추가했습니다. 미래 양자 컴퓨터가 초래할 위협이 잘 알려진 만큼, 우리는 가장 큰 효과를 기대할 수 있는 영역—암호화된 통신 및 기타 민감한 정보를 다루는 애플리케이션—에 강력하고 양자 보안 암호화를 먼저 개발·배포해 왔습니다. 여기에는 iMessage, VPN, TLS 네트워킹 등이 포함됩니다. 또한, 지난해 가을에 출시한 Apple CryptoKit에는 양자 보안 API가 포함되어 있어 개발자들이 자신의 앱에 양자 보안 암호화와 인증을 손쉽게 도입할 수 있습니다.

corecrypto는 우리 제품 전반에 걸쳐 지속적으로 사용되며, 25억 대가 넘는 활성 기기에서 암호화·복호화, 해시, 난수 생성, 디지털 서명을 제공합니다. corecrypto에 중대한 버그가 발생하면 이를 기반으로 하는 모든 앱과 기능의 보안·신뢰성이 위협받을 수 있기 때문에, 우리는 라이브러리에 새로운 코드를 추가할 때 매우 보수적인 입장을 취하고 테스트를 포괄적으로 수행하기 위해 특별한 노력을 기울입니다.

새로운 암호 알고리즘을 corecrypto에 포함시키기 위해서는 다음 기준에 대한 철저한 평가를 거칩니다:

• 보안 향상. 알고리즘은 새로운 문제를 해결하거나 기존 알고리즘의 보안을 개선해야 합니다.
• 안전한 설계. 알고리즘은 강력한 이론적 보안을 가져야 하며, 전 세계 연구 커뮤니티의 엄격하고 지속적인 암호 해석을 견뎌냈어야 합니다. 또한 실용적으로는 우리가 의도한 사용 환경에서 안전하게 구현될 수 있어야 합니다.
• 높은 성능. 구현은 지연 시간과 전력 소비 측면 모두에서 매우 효율적이어야 하며, 모든 Apple 기기에서 동일하게 최적화돼야 합니다.
• 컴팩트한 파라미터. 키 크기, 서명, 암호문은 네트워크 지연에 미치는 영향을 최소화하고 기기 메모리 제한 내에 들어가야 합니다.

알고리즘이 corecrypto에 포함될 만큼 충분히 높은 기준을 만족하면, 우리는 다음 조건을 만족하는 구현을 개발합니다:

• 보안. 코드는 엄격한 보안 기준을 충족하고 정보를 누설해서는 안 됩니다. 이는 정확성뿐 아니라 타이밍 신호 누출 방지와 같은 강화 작업을 포함합니다.
• 최적화. 구현은 실행되는 실리콘의 명령어와 아키텍처를 최대한 활용해야 합니다.
• 정확성. 코드와 모든 관련 최적화는 암호학 커뮤니티가 검증한 표준 정의에 충실히 구현되어야 하며, 올바른 출력을 생성해야 합니다.

우리가 corecrypto에 포함할 양자 보안 알고리즘을 평가했을 때, 기준을 만족하는 두 가지 알고리즘—후에 NIST가 각각 ML‑KEM과 ML‑DSA(FIPS 203, FIPS 204)로 표준화한 것—에 빠르게 수렴했습니다. NIST가 다른 서명 방식을 표준화하기도 했지만, ML‑KEM과 ML‑DSA가 우리 요구에 가장 잘 부합했습니다. 암호학 커뮤니티가 수행한 방대한 작업 덕분에 ML‑KEM과 ML‑DSA에 대한 레퍼런스 구현이 존재했으며, 우리의 평가에서도 보안성과 성능이 탄탄한 기반을 가지고 있음을 확인했습니다.

corecrypto는 Apple 제품 전반—다양한 마이크로아키텍처를 갖춘 특수 칩 포함—에 사용되기 때문에, 우리는 먼저 알고리즘 구현을 이식 가능한 C 코드로 작성합니다. 구현이 배포되는 모든 환경에서 올바르고 안전하게 동작하도록 하기 위해, 우리는 다음과 같은 엄격한 가이드라인을 적용합니다: 비밀 값이 실행 시간에 의해 누출되지 않도록 코드를 작성하고, 컴파일러가 이러한 보호를 무심코 약화시키지 않도록 방지하며, Apple 프로세서의 Data‑Independent Timing(DIT) 및 Pointer Authentication(PAC) 같은 하드웨어 기능을 활용해 마이크로아키텍처 수준의 사이드 채널과 메모리 손상 공격을 방어합니다. 또한, 사용 사례별 위협 모델에 따라 내부 연산을 무작위화할 필요성을 평가합니다.

ML‑KEM과 ML‑DSA 설계에 동봉된 레퍼런스 구현을 검토한 결과, 우리는 상당한 개선 여지를 발견했습니다. 알고리즘 자체를 변경하지 않으면서 성능을 높이는 수학적 최적화를 적용했고, 가장 성능·보안에 민감한 서브루틴을 Apple의 선도적인 프로세서를 최대한 활용하도록 정교하게 재작성했습니다. Apple 실리콘에 대한 깊은 전문성을 바탕으로 만든 이러한 손수 최적화된 경로는 프로세서 동작을 정밀하게 제어함으로써, 공격자가 비밀을 추출할 수 있는 타이밍 사이드 채널을 방지하는 데 큰 도움이 됩니다.

이처럼 복잡한 알고리즘에 우리만의 대규모 개선을 통합한 새로운 구현을 도입하는 일은 상당한 과제입니다. 더욱이 ML‑KEM과 ML‑DSA의 수학적 기반 자체가 비교적 최신이어서, 산업 전반에 걸쳐 이러한 알고리즘을 실제 제품에 안전하게 구현한 경험이 아직 부족합니다. 우리는 각 단계마다, 초기 타원곡선 암호화 도입 시 산업이 겪었던 미묘하고 악용 가능한 버그들을 반복하지 않도록 깊이 고민했습니다.

우리의 최우선 과제는 손수 튜닝한 성능 최적화와 보안 강화가 적용된 새로운 알고리즘 구현이 기능적으로 정확하고 안전하다는 것을 보장하는 것이었습니다. 이를 위해 우리는 깊이 있는 기존 테스트, 시뮬레이션, 독립적인 검토를 포함한 뛰어난 검증 기준을 설정하고, 이를 엄격한 형식 검증과 결합했습니다.

우리의 형식 검증 요구 사항

형식 검증은 수학적 증명을 이용해 시스템이나 객체가 우리가 정의한 특정 속성을 만족한다는 것을 입증하는 방법입니다. Apple에서는 15년 이상 실리콘 개발 과정에서 광범위한 형식 검증을 수행해 왔으며, 2019년부터는 고전 암호화, 특히 타원곡선 공개키 연산을 수행하는 하드웨어 Public Key Accelerator(PKA)를 증명하는 데 형식 검증을 활용하기 시작했습니다.

corecrypto에 대해서는, 우리의 알고리즘 구현이 기존 소프트웨어 테스트가 제공할 수 있는 수준을 훨씬 뛰어넘는 확신을 갖고 정확함을 증명하기 위해 수학적 증명을 사용합니다. 간단히 말해, 구현의 수학식이 사양의 수학식과 동등함을 증명할 수 있다면, 구현이 올바른 출력을 생성한다는 것을 알 수 있습니다. 이론적으로 이는 구현이 정확한 출력을 생성한다는 강력한 확신을 제공하며, 우리의 implemen