Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

다음은 "소수체 PINI: 포스트 양자 NTT 마스킹을 위한 기계 검증 합성 정리" 논문에 대한 상세한 기술 요약입니다.

1. 문제 제기

이 논문은 NIST 표준 (ML-KEM 및 ML-DSA) 에 사용되는 정수론적 변환 (NTT) 구현을 위한 포스트 양자 암호 (PQC) 하드웨어의 형식적 보안 검증에서 중요한 공백을 다루고 있습니다.

• 배경: NTT 의 하드웨어 구현은 차분 전력 분석 (DPA) 과 같은 사이드 채널 공격을 방어하기 위해 소수체 ($\mathbb{Z}_q$) 에 대한 산술 마스킹 (arithmetic masking) 에 의존합니다.
• 공백: 부울 마스킹 ($GF(2^n)$) 은 기계 검증된 증명과 함께 성숙한 합성 이론 (NI, SNI, PINI) 을 가지고 있는 반면, 소수체에 대한 산술 마스킹은 이에 상응하는 합성 정리가 부족합니다.
• 구체적 문제: 산술 마스킹에서 모듈러 감소 (예: 바렛 감소) 와 같은 연산은 마스크와 비자명한 방식으로 상호작용합니다. 부울 XOR 과 달리 마스크가 완벽하게 균일성을 유지하는 것과 달리, 산술 마스킹은 비균일한 출력 분포 (다중도 > 1) 를 초래할 수 있습니다.
• 취약점: 이전의 경험적 분석과 구조적 연구는 마이크로소프트의 "Adams Bridge" PQC 가속기에서 파이프라인 단계 간의 중간 와이어가 비균일하여 DPA 공격을 허용한다는 취약점을 확인했습니다. 그러나 이것이 왜 발생하는지에 대한 형식적 이론적 설명과 합성 정리를 통해 이를 어떻게 수정할지에 대한 내용은 부재했습니다.

2. 방법론

저자들은 Lean 4 증명 도구를 사용하여 형식적 검증을 수행함으로써 산술 마스킹에 대한 합성 정리를 유도하고 증명합니다.

• 형식적 모델: 그들은 PF-PINI(k)(소수체 프로브 격리 비간섭성) 라는 정량적 보안 지표를 정의합니다.
  • 이진 보안 개념 (보안/비보안) 과 달리, PF-PINI 는 마스크 공간에 대한 출력 값의 다중도 (multiplicity) 를 측정합니다.
  • $k=1$은 완벽하게 균일한 분포를 의미합니다.
  • $k=2$는 최대 다중도가 2 임을 의미하며, 와이어당 최대 1 비트의 정보가 유출될 수 있음을 나타냅니다.
• "갱신 (Renewal) 논증": 핵심 이론적 통찰은 두 파이프라인 단계 사이에 새로운 무작위 마스크를 적용하면 첫 번째 단계의 중간 와이어에서 보안 매개변수 ($k_1$) 가 완전히 "지워져", 첫 번째 단계의 출력이 얼마나 비균일했는지와 관계없이 보안 매개변수가 초기화된다는 것입니다.
• 하드웨어 연결: 저자들은 RTL 설계에 사용되는 추상적 대수 모델 ($\mathbb{Z}_q$) 과 바렛 감소에 특화된 하드웨어 충실도 자연수 산술 (Nat) 간의 격차를 형식적으로 연결합니다.
• 검증 범위: 전체 작업은 18 개의 기계 검증된 정리로 구성되며, sorry 스텁 (미증명 가정) 이 전혀 없으므로 고신뢰 보장을 제공합니다.

3. 주요 기여

이 논문은 다음과 같은 여섯 가지 주요 기여를 합니다:

1. 갱신 정리 (Theorem 4.1): 두 단계 ($G_1 \to G_2$) 사이에 새로운 무작위 마스크가 적용되면 중간 와이어가 완벽하게 균일해짐을 증명합니다. 특정 중간 값을 생성하는 마스크 쌍의 집합의 크기는 정확히 $q$이며, $G_1$의 보안 매개변수와 무관합니다.
2. 긍정적 합성 정리 (Theorem 4.4): 새로운 마스킹이 적용된 2 단계 파이프라인이 PF-PINI($k_2$) 를 만족함을 보여줍니다. 합성된 출력의 보안은 두 번째 단계의 매개변수 ($k_2$) 에만 의존하며, 첫 번째 단계의 약점 ($k_1$) 은 완전히 지워집니다.
3. 부정적 합성 정리 (Theorems 5.1–5.3): 새로운 마스킹 없이 중간 와이어가 첫 번째 단계의 다중도 ($k_1$) 를 유지함을 증명합니다. $k_1 > 1$인 경우 와이어는 비균일해지며, 이는 DPA 공격에 필요한 조건을 만듭니다.
4. 대수 - 하드웨어 연결 (Theorem 6.1): 표준 범위 조건 ($q \le 2^s$) 하에서 대수적 바렛 감소 맵이 하드웨어 충실도 Nat 산술 맵과 동등함을 형식적으로 증명합니다. 이는 이론적 경계가 실리콘 구현에 직접 적용됨을 검증합니다.
5. Adams Bridge 진단: 정리를 형식적으로 구체화하여 마이크로소프트의 Adams Bridge 가속기를 진단합니다. 이 증명은 새로운 단계 간 마스킹의 부재가 바렛 출력 와이어를 비균일하게 (PF-PINI(2)) 만들어 이전의 경험적 DPA 공격이 성공한 이유를 설명합니다.
6. 보편적 1 비트 장벽: 모듈러 감소 (바렛과 몬트고메리 모두) 에 대해 PF-PINI(2) 경계가 보편적임을 계산적 증거로 제시하며, 이러한 연산에 대한 근본적인 "1 비트 장벽"을 시사합니다.

4. 주요 결과

• 합성의 형식적 증명: 이 논문은 새로운 단계 간 마스킹이 산술 가젯을 안전하게 합성하기 위한 필요충분 조건임을 확립합니다.
• 정량적 보안:
  • 새로운 마스킹 사용 시: 중간 와이어는 균일합니다 ($k=1$). 최종 출력은 두 번째 단계의 매개변수 ($k_2$) 로 제한됩니다.
  • 새로운 마스킹 미사용 시: 중간 와이어는 비균일합니다 (최대 $k_1$까지). 이 비균일성은 경험적 공격에서 관찰된 사이드 채널 유출의 근본 원인입니다.
• Adams Bridge 수정: 진단은 Butterfly 와 Barrett 단계 사이에 단일 새로운 무작위 마스크 레지스터와 뺄셈 연산을 추가하면 최종 출력 보안 매개변수를 변경하지 않고도 중간 와이어의 DPA 취약점을 제거할 수 있음을 확인합니다.
• 아티팩트 가용성: 18 개의 정리와 재생 스크립트를 포함한 전체 Lean 4 소스 코드가 공개되어 있어 증명의 독립적 검증을 가능하게 합니다.

5. 의의

• 최초의 기계 검증 산술 합성: 이는 소수체에 대한 산술 마스킹에 대한 기계 검증 합성 정리를 제공하는 첫 번째 작업으로, PQC 하드웨어 보안의 주요 이론적 공백을 메웠습니다.
• 이론과 실무의 연결: 추상적 대수 증명과 하드웨어 충실도 산술을 형식적으로 연결함으로써, 경험적 테스트를 넘어 실제 실리콘 설계를 검증하기 위한 엄격한 기반을 제공합니다.
• 설계 지침: PQC 하드웨어에 대한 명확하고 증명 가능한 설계 규칙을 확립합니다: 파이프라인 단계 사이에 항상 새로운 마스킹을 삽입하십시오. 이 간단한 구조적 변경은 합성된 파이프라인의 보안이 중간 단계가 아닌 최종 단계의 가장 약한 고리에 의해 결정됨을 보장합니다.
• 증거의 수렴: 형식적 증명은 세 가지 독립적인 이전 분석 (경험적 전력 분석, 코드 검토, 구조적 의존성 분석) 과 완벽하게 일치하여, Adams Bridge 가속기에서 식별된 구조적 결함이 실제로 취약점의 근본 원인임을 확인합니다.

요약하자면, 이 논문은 포스트 양자 암호의 새로운 시대를 위한 안전하고, 합성 가능하며, 사이드 채널에 강한 하드웨어 가속기를 설계하는 데 필요한 수학적 및 형식적 검증의 기반을 제공합니다.