The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

기술 요약: 1 비트 장벽의 보편성

문제 제기
수론 변환 (NTT) 은 NIST 양자내성암호 (PQC) 표준인 ML-DSA(FIPS 204) 와 ML-KEM(FIPS 203) 의 계산적 핵심 역할을 수행합니다. 이러한 표준의 하드웨어 구현은 사이드 채널 공격, 특히 차분 전력 분석 (DPA) 에 저항하기 위해 산술 마스킹에 의존합니다. $GF(2^n)$ 위의 부울 마스킹은 (PINI 와 같은) 구성 가능성 프레임워크를 확립해 왔으나, 소수 $q$에 대한 $\mathbb{Z}_q$ 위의 산술 마스킹은 고유한 어려움을 제시합니다.

QANARY 프로그램 (논문 1~6) 의 선행 연구는 구조적 의존성 분석을 수립하고 특정 구성 요소에 대한 보안 마진을 정량화했으며, 특히 Barrett 감축이 "1 비트 장벽"(PF-PINI(2)) 을 만족함을 증명했습니다. 그러나 두 가지 중요한 격차가 남아 있었습니다:

1. 임의의 파이프라인 깊이: 이전 구성 정리는 2 단계로 제한되었습니다. 새로운 단계 간 마스킹을 갖춘 임의의 $k$단계 파이프라인에 대한 공식적 보장이 없었습니다.
2. Montgomery 감축: Barrett 감축이 특징화되었으나, NTT 하드웨어에서 사용되는 두 번째 표준 모듈러 감축인 Montgomery 감축 (ML-DSA 및 일부 ML-KEM 구현에서 지배적임) 은 공식적인 PF-PINI 특징화가 부재했습니다.
3. 통합 종단 간 경계: 나비 연산, Barrett 감축, Montgomery 감축으로 구성된 임의의 파이프라인에 대한 결과를 통합한 단일 기계 검증 카디널리티 경계가 존재하지 않았습니다.

방법론
본 논문은 Lean 4 증명 보조 도구를 사용한 공식 검증을 활용합니다. 이 접근법은 엄격하게 구성적이며, sorry(증명되지 않은 가정) 와 비표준 공리는 전혀 포함하지 않습니다. 방법론은 다음에 의존합니다:

• PF-PINI 정의: 단일 산술 마스킹 하에서 단일 와이어 가젯의 누출을 정량화하는 소수 필드 프로브 격리 비간섭 (PF-PINI) 매개변수를 사용합니다. 가젯이 PF-PINI($M$) 이라는 것은 임의의 출력 값에 대한 전상 (preimage) 의 카디널리티가 최대 $M$임을 의미합니다.
• 파이프라인 모델링: 각 단계 $G_i$가 PF-PINI 가젯이며 새로운 무작위 마스킹으로 분리된 $k$단계 파이프라인을 정의합니다. 파이프라인 출력은 재귀적으로 계산됩니다.
• 조합 분석: 새로운 단계 간 마스킹이 중간 단계의 누출 매개변수를 "지워" 최종 경계가 마지막 단계의 매개변수에만 의존함을 증명합니다.
• 하드웨어 충실도 모델링: 하드웨어 레지스터 너비와 래핑 (wraparound) 동작을 고려하여 Montgomery 감축을 모델링하고, 특히 충돌 오프셋 $2^{w-s}$를 분석합니다.

주요 기여
본 논문은 Lean 4 에서 모두 공식화된 네 가지 주요 기여를 제공합니다:

1. $k$단계 구성 정리 (정리 3.1):
   이 정리는 이전 2 단계 구성 결과를 임의의 깊이 $k \ge 1$로 일반화합니다. 새로운 단계 간 마스킹을 갖춘 가젯 $G_0, \dots, G_{k-1}$로 구성된 파이프라인의 경우, 출력의 전상 카디널리티가 다음과 같이 경계됨을 증명합니다:
   $$| \{ (m, f) : \text{파이프라인 출력} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   핵심적으로, 이 경계는 마지막 단계에 의해 결정되며, 모든 중간 단계의 매개변수는 새로운 마스킹에 의해 지워집니다.

2. Montgomery 감축은 PF-PINI(2) 이다 (정리 4.3):
   본 논문은 Montgomery 감축이 Barrett 감축의 구조를 반영하여 PF-PINI(2) 속성을 만족함을 공식적으로 증명합니다. 래핑 발생 여부에 의존하는 "2-분기" 구조를 가진 하드웨어 충실도 Montgomery 맵은 최대 2 의 전상 카디널리티를 가짐을 보여줍니다. 정리 4.7 은 이 경계의 tightness(tightness) 를 추가로 확립하여 표준 매개변수 (ML-KEM 및 ML-DSA) 의 경우 중복도가 정확히 2 임을 보여줍니다.

3. 종단 간 중복도 경계 (정리 5.1):
   $k$단계 구성 정리와 Barrett(논문 5), Montgomery(본 논문), 나비 연산 (논문 4) 에 대한 특정 PF-PINI(2) 결과를 결합함으로써, 논문은 통합 경계를 수립합니다. 모든 단계가 $\text{maxMult} \le 2$를 만족하는 임의의 $k$단계 파이프라인의 경우, 출력 전상 카디널리티는 다음과 같이 경계됩니다:
   $$2 \cdot q^{2k-2}$$
   균일한 마스킹을 사용한 1 차 프로빙 모델 하에서, 이는 파이프라인 깊이 $k$와 무관한 관찰당 조건부 확률 경계 $2/q$에 해당합니다.

4. 경험적 발견의 공식적 앵커링 (정리 5.4):
   논문은 파이프라인의 어떤 단계라도 $\text{maxMult} \ge 3$(예: 마스킹되지 않은 단계) 인 경우 종단 간 경계의 가설이 실패한다는 Lean 검증 조건을 제공합니다. 이는 "Adams Bridge"PQC 가속기 (논문 1, 2 및 외부 연구) 에 대한 이전 경험적 및 구조적 분석을 공식적으로 앵커링하여, 해당 설계의 특정 마스킹되지 않은 구성이 깊이 무관 경계의 충분 조건 범위에 속하지 않음을 확인합니다.

결과

• 1 비트 장벽의 보편성: 논문은 NIST PQC 하드웨어에서 사용되는 두 가지 표준 모듈러 감축 (Barrett 및 Montgomery) 모두에 "1 비트 장벽"(전상 카디널리티 2) 이 적용됨을 확인합니다.
• 깊이 무관성: 공식 증명들은 새로운 단계 간 마스킹이 사용되고 모든 단계가 PF-PINI($\le 2$) 를 만족하는 한, 파이프라인에 단계를 추가해도 관찰당 누출 경계가 저하되지 않음을 보여줍니다.
• 검증 상태: 전체 아티팩트는 세 개의 정리 모듈에 걸쳐 20 개의 선언으로 구성되며, 1,753 개의 작업에서 0 개의 오류, 0 개의 sorry, 그리고 네이티브 결정 절차 없이 빌드되었습니다.

의의 및 주장
본 논문은 마스킹된 NTT 하드웨어에 대한 공식 검증 프로그램의 완결로서 자신을 위치시킵니다. 그 의의는 하드웨어 설계자를 위한 정량적, 기계 검증 구성적 기초를 제공한다는 점에 있습니다.

• 인증 측면: 유도된 카디널리티 경계 ($2 \cdot q^{2k-2}$) 는 SILVER 및 maskVerif 와 같은 게이트 레벨 도구를 보완하는 아키텍처 수준에서 DPA 저항성 논증을 위한 구체적인 증거를 제공합니다.
• 설계자 측면: 깊이 무관 경계를 달성하기 위해 설계자는 모든 단계가 PF-PINI($\le 2$) 를 만족하도록 하고 단계 사이에 새로운 마스킹을 삽입해야 한다는 처방적 수정 경로를 제공합니다.
• 주장의 겸손함: 저자들은 확률 및 최소 엔트로피 해석 (예: $2/q$) 이 카디널리티 경계의 비공식적 의미적 결과이며 Lean 에서 기계적으로 공식화되지 않았다고 명시적으로 밝힙니다. 또한 Adams Bridge 분석과 관련하여, 논문은 특정 구성이 정리 5.1 의 충분 조건을 실패한다고만 주장할 뿐, 해당 하드웨어가 "고장 났다"거나 "불안전하다"고 주장하지는 않습니다. 대신 대안적 프레임워크나 더 강력한 모델이 다른 결론을 도출할 수 있음을 인정합니다. 이 작업은 특정 구현에 대한 결정적 보안 판정이 아니라 구성적 분석을 위한 도구로 제시됩니다.