KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
이 논문은 새로운 게임 기반 보안 프레임워크, 확률적 계산을 지원하는 상호작용 트리 의미론, 그리고 관계적 호어 논리를 통해 Signal에서 사용되는 고도로 최적화된 ML-KEM 구현에 대해 Jasmin 컴파일러가 기능적 정확성과 KEM-IND-CCA 보안을 모두 보존함을 Rocq 증명기(prover)를 통해 완전히 기계화된 방식으로 증명한다.
원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기
디지털 보안의 고위험 세계에서, 암호학은 개인적인 메시지부터 금융 거래에 이르기까지 모든 것을 보호하는 보이지 않는 자물쇠 역할을 합니다. 수십 년 동안 전문가들은 이러한 자물쇠가 깨지지 않음을 보장하기 위해 수학적 증명에 의존해 왔지만, 종이 위의 우아한 수학과 이를 실행하는 컴퓨터 코드라는 복잡한 현실 사이에는 결정적인 간극이 존재해 왔습니다. 암호 체계가 이론적으로는 안전하다고 증명되었을 때조차, 그 이론을 컴퓨터 프로세서가 이해하는 특정 명령어로 번역하는 과정에서 미묘한 오류가 발생할 수 있습니다. 이러한 오류는 주로 번역을 수행하는 컴파일러에 의해 도입되며, 공격자들이 악용할 수 있는 취약점을 만들어냅니다. 전 세계가 미래의 위협에 대비하여 새로운 양자 내성 암호 표준으로 전환할 준비를 함에 따라, 이 새로운 시스템들이 기계 코드 수준까지 안전하게 유지되도록 보장하는 것은 더 이상 단순한 이론적 관심사가 아니라, 글로벌 통신 네트워크의 안전을 위한 필수 과제입니다.
연구팀은 이제 이미 시그널(Signal)과 같은 인기 있는 보안 메시징 애플리케이션에서 사용되고 있는 가장 중요한 새로운 암호 표준 중 하나인 ML-KEM에 대해 이 간극을 메웠습니다. 그들의 연구는 고수준 보안 코드를 기계 명령어로 변환하는 데 사용되는 특정 소프트웨어 도구가 보안 보장을 실수로 깨뜨리지 않는다는 것을 입증했습니다. 본질적으로, 그들은 원래의 인간이 읽을 수 있는 코드에 대해 설정된 보안 속성이 컴퓨터가 실제로 실행하는 최종 최적화된 어셈블리 코드에서도 완벽하게 보존된다는 것을 증명했습니다. 이 성과는 컴파일러를 숨겨진 버그를 포함할 수 있는 '블랙박스'로 신뢰할 필요를 없애준다는 점에서 매우 중요합니다. 대신, 컴파일러 자체가 추상적인 보안 증명과 물리적 하드웨어 사이의 안전한 가교임을 수학적으로 검증되었습니다.
연구진이 직면한 과제는 현대 암호의 특성 때문에 매우 독특했습니다. 그들이 연구한 특정 알고리즘인 ML-KEM은 '거부 샘플링(rejection sampling)'이라 불리는 기술에 의단계적으로 의존하는데, 이는 컴퓨터가 특정 패턴에 맞는 숫자를 찾을 때까지 무작위 숫자를 반복해서 시도하는 방식입니다. 이 과정은 프로그램이 항상 고정된 시간 동안 실행되는 것이 아니라, 빠르게 끝날 수도 있고 예상보다 훨씬 많은 시도가 필요할 수도 있음을 의미합니다. 기존의 컴파일러 검증 방법들은 예측 가능하고 고정된 순서의 단계로 실행되는 프로그램을 위해 설계되었습니다. 따라서 이러한 확률적 동작, 즉 코드의 경로가 확률에 따라 달라지는 상황을 처리하는 데 어려움을 겪었습니다. 만약 컴파일러 검증 도구가 이러한 무작위 루프를 설명할 수 없다면, 최종 기계 코드가 원래의 설계와 동일하게 작동한다는 것을 보장할 수 없으며, 이는 보안 사슬에 잠재적인 구멍을 남기게 됩니다.
이를 해결하기 위해 연구진은 이러한 프로그램이 어떻게 작동하는지 이해하기 위한 새로운 프레임워크를 구축했습니다. 그들은 코드의 실행을 단순한 명령어 목록이 아니라, 모든 무작위 선택과 외부 세계와의 상호작용이 트리의 가지(branch)가 되는 가능한 상호작용의 트리로 취급했습니다. 이 접근 방식은 프로그램의 '거의 확실한(almost sure)' 종료, 즉 정확한 시간은 예측할 수 없더라도 확률 1로 결국 종료된다는 것을 모델링할 수 있게 해주었습니다. 이 새로운 모델을 사용하여, 그들은 확률적 환경에서 컴파일러가 올바르다는 것이 무엇을 의미하는지 정의할 수 있었습니다. 그들은 원래 코드가 취할 수 있는 모든 경로에 대해, 컴 compiled 코드가 일치하는 경로를 따르며 결과의 분포를 정확하게 보존한다는 것을 증명했습니다.
연구팀은 이 프레임워크를 고보증 암호 코드를 작성하기 위해 특별히 설계된 도구인 Jasmin 컴파일러에 적용했습니다. 그들은 수백만 명의 사용자가 사용하는 메시징 앱인 시그널에서 사용되는 ML-KEM 구현에 집중했습니다. 수학적 논증을 절대적인 엄격함으로 점검하는 소프트웨어 도구인 강력한 증명 보조기(proof assistant)를 사용하여, 그들은 컴파일러가 보안 속성을 변경하지 않고 소스 코드를 어셈블리 언어로 정확하게 번역함을 검증했습니다. 그들의 증명은 초기 고수준 설명부터 최종 기계 명령에 이르기까지 전체 컴파일 과정을 포괄합니다. 그 결과, 이전에는 소스 코드에 대해서만 증명되었던 암호의 보안이 이제 사용자의 기기에서 실제로 실행되는 코드에서도 유효하다는 보장이 확보되었습니다.
이 연구는 미래의 양자 컴퓨터 공격을 견딜 수 있는 암호화 방법으로의 글로벌 전환인 포스트 퀀텀(양자 내성) 전환에 최고 수준의 확신을 부여하려는 더 큰 노력의 일환입니다. 비록 연구진이 계산 시간이 얼마나 걸리는지 또는 전력 소모량이 얼마인지 관찰함으로써 비밀을 알아낼 수 있는 부채널 공격(side-channel attacks)까지는 아직 증명을 확장하지 않았지만, 그들은 향후 연구를 위한 필수적인 토대를 마련했습니다. 컴파일러가 핵심 보안 게임을 보존함을 입증함으로써, 그들은 더 복잡한 보안 보장을 구축할 수 있는 견고한 기반을 만들었습니다. 이 검증은 완전히 기계화되어 있어, 모든 증명 단계가 컴퓨터에 의해 체크되었으므로 논리 자체에 인간의 실수가 개입할 여지가 없습니다.
이 작업의 영향은 단 하나의 알고리즘에 국한되지 않습니다. 연구진이 개발한 프레임워크는 다른 암호 체계와 보안 속성에도 적용될 수 있을 만큼 일반적입니다. 그들은 컴파일러의 정확성이라는 관점을 통해 게임 기반 보안(game-based security, 암호의 강도를 정의하는 표준적인 방법)을 추론하는 것이 가능하다는 것을 보여주었습니다. 이는 새로운 암호 표준이 개발되고 구현됨에 따라, 동일한 엄격한 검증 과정을 거칠 수 있음을 의미합니다. 연구진은 자신들의 도구와 증명을 오픈 소스로 공개하여, 다른 전문가들이 그들의 작업을 검토, 검증 및 발전시킬 수 있도록 했습니다. 이러한 투명성은 현대 사회를 뒷받침하는 디지털 인프라에 대한 신뢰를 유지하는 데 매우 중요합니다.
결국, 이 논문은 우리가 데이터를 보호하는 디지털 자물쇠가 설계자인 수학자들이 약속한 것만큼 정확히 강력할 것이라고 확신할 수 있는 미래를 향한 중요한 진전을 나타냅니다. 추상적인 보안 증명과 기계 코드라는 구체적인 현실 사이의 간극을 메움으로써, 연구진은 암호 공급망에서 주요한 불확실성의 원인을 제거했습니다. 그들의 연구는 사용자가 보안 메시지를 보낼 때, 그들이 의존하는 보안 보장이 단지 이론적인 이상이 아니라, 사용자의 기기에 있는 실리콘 칩까지 수학적으로 보존되는 속성임을 보장합니다. 이러한 수준의 확신은 우리가 디지털 시대의 새롭고 진화하는 위협에 직면해 있음에도 불구하고, 우리를 연결하는 기술을 신뢰할 수 있게 해주는 것입니다.
연구 분야의 논문에 파묻히고 계신가요?
연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.