Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

"마스크된 바렛 감소에 대한 기계 검증된 카디널리티 경계: 포스트 양자 암호 하드웨어의 1 비트 사이드 채널 누출 장벽"에 대한 상세 기술 요약입니다.

1. 문제 제기

ML-KEM (FIPS 203) 및 ML-DSA (FIPS 204) 와 같은 포스트 양자 암호 (PQC) 표준은 수론적 변환 (NTT) 파이프라인에 크게 의존합니다. 이러한 파이프라인은 선형 "버터플라이" 단계와 비선형 모듈러 감소 단계를 포함하며, 일반적으로 **바렛 감소 (Barrett reduction)**를 사용하여 구현됩니다.

기존의 형식적 검증 프레임워크 (ISW, t-SNI, PINI, DOM) 는 $GF(2)$에 대한 부울 마스크에 대한 강력한 보장을 제공하지만, 특히 바렛 감소에 대한 **소수 필드 ($\mathbb{Z}_q$) 에 대한 산술 마스크**에 대한 기계 검증된 특성화는 부족합니다.

• 격차: 하드웨어 구현 (예: "Adams Bridge" 설계) 은 종종 사이드 채널 취약점에 시달리는데, 이는 바렛 감소의 비선형 조건부 뺄셈이 표준 합성 정리가 가정하는 아핀 구조를 깨뜨리기 때문입니다.
• 질문: 1 차 산술 마스크 하에서 바렛 감소 회로의 내부 와이어의 정확한 누출 경계는 무엇입니까? 이전 도구들은 보편적이고 기계 검증된 답변을 제공할 수 없어 FIPS 140-3 인증에 불확실성이 존재했습니다.

2. 방법론

저자들은 Lean 4 증명 어시스턴트와 Mathlib 라이브러리를 활용한 형식적 검증 접근법을 사용합니다.

• 형식화: 그들은 $\mathbb{Z}_q$ (여기서 $q$는 모듈러스) 위에서 바렛 내부 와이어 맵을 대수적으로 정의합니다. 맵 $f_x(m)$ 은 비밀 $x$와 무작위 마스크 $m$을 입력받아 조건부 뺄셈에 의해 결정되는 두 가지 분기 구조를 기반으로 출력을 생성합니다.
• 증명 전략: 특정 인스턴스를 시뮬레이션하는 대신, 모든 $q > 0$ 및 시프트 매개변수 $s$에 대해 성립하는 보편적 정리를 증명합니다.
• 핵심 개념: 그들은 **역상 카디널리티 (preimage cardinality)**를 분석합니다. 고정된 비밀 $x$와 특정 출력 값 $v$에 대해, 몇 개의 서로 다른 마스크 $m$이 $v$를 생성할 수 있는지 확인합니다.
• 툴체인: 아티팩트에는 sorry가 없는 (불완전한 증명 없음) 12 개의 증명된 결과가 포함되어 있어 모든 단계가 Lean 에 의해 커널 검증되었음을 보장합니다.

3. 주요 기여

A. 삼분성 정리 (Trichotomy Theorem)

이 논문은 바렛 내부 와이어 맵이 3 값 역상 구조를 보인다고 증명합니다. 임의의 비밀 $x$와 임의의 출력 $v$에 대해, $f_x(m) = v$를 만족하는 마스크 $m$의 개수는 정확히 0, 1, 또는 2입니다.

• 메커니즘: 조건부 뺄셈은 두 개의 아핀 분기 ($\mathbb{Z}_q$ 내의 이동) 를 생성합니다. 임의의 값의 역상은 최대 두 개의 후보인 $\{x - v, x - v + r\}$의 부분집합입니다. 여기서 $r = 2^s \mod q$입니다.
• 보편성: 이는 특정 PQC 매개변수와 무관하게 임의의 모듈러스 $q$와 시프트 $s$에 대해 성립합니다.

B. 1 비트 장벽

삼분성에 기반하여 저자들은 보편적인 누출 경계를 확립합니다:

• 최대 중복도: 단일 출력을 생성하는 마스크의 최대 개수가 2 이므로, 특정 출력 값을 관찰할 확률의 최대치는 $2/q$입니다.
• 최소 엔트로피 경계: 조건부 최소 엔트로피 $H_\infty(\text{output} \mid x)$는 $\log_2(q) - 1$보다 크거나 같습니다.
• 해석: 바렛 감소는 1 차 프로빙 하에서 내부 와이어당 최대 1 비트의 최소 엔트로피를 누출합니다. 이는 많은 출력 값이 도달 불가능 (역상 개수 = 0) 하기 때문에 실제 누출은 종종 1 비트 미만이라는 점에서 "보수적인" 경계입니다.

C. PF-PINI 프레임워크

저자들은 $\mathbb{Z}_q$ 위의 산술 가젯에 대한 새로운 보안 지표인 **소수 필드 PINI (PF-PINI)**를 도입합니다:

• 정의: 가젯의 역상 카디널리티가 $k$로 제한되면 해당 가젯은 PF-PINI($k$) 입니다.
• 구현 예시:
  • 버터플라이 단계: **PF-PINI(1)**을 만족합니다 (완전한 전단사, 마스크 외의 누출 제로).
  • 바렛 감소: **PF-PINI(2)**를 만족합니다 (1 비트 장벽).
• 합성 관찰: 저자들은 (아직 형식적으로 증명되지는 않았지만) 파이프라인 단계가 신선한 단계 간 마스크로 분리되어 있다면, 합성된 파이프라인의 최대 중복도는 $\max(k_1, k_2)$라고 관찰합니다. 이는 1 비트 장벽이 전체 NTT 파이프라인을 통해 전파됨을 의미합니다.

4. 결과 및 분석

• 기계 검증 증명: 아티팩트에는 삼분성, 엄밀성 증명 (count=2 가 달성 가능함을 보임), 그리고 PF-PINI 구현 예시를 포함한 12 개의 검증된 정리가 포함되어 있습니다.
• 지원 격차 발견: 분석은 "도달 불가능한" 출력 값 (역상 개수 = 0) 을 드러냅니다. 이는 버그가 아닌 보안 기능으로, 공격자의 유효 정보를 줄입니다.
• Adams Bridge 사례 연구: 이 논문은 "Adams Bridge" 하드웨어 구현을 분석합니다:
  • 단계 내 실패: 이전 연구 (논문 1 및 2) 는 중간 마스크 없이 공유가 상호작용하여 취약점이 발생했음을 보였습니다.
  • 단계 간 실패: 이 논문은 Adams Bridge 가 단계 간에 신선한 마스크를 적용하지 못함을 식별합니다. 결과적으로 PF-PINI 합성 경계가 적용되지 않아 누출이 $\max(k_1, k_2)$로 제한되는 대신 곱해져 ($k_1 \times k_2$) 증가합니다. 이는 개별 바렛 게이트에 1 비트 장벽이 존재함에도 불구하고 설계가 취약한 이유를 설명합니다.
• 정량적 영향:
  • ML-KEM ($q=3329$) 의 경우: 누출 $\le 1$ 비트 (최소 엔트로피 $\ge 10.70$ 비트).
  • ML-DSA ($q=8,380,417$) 의 경우: 누출 $\le 1$ 비트 (최소 엔트로피 $\ge 21.99$ 비트).

5. 중요성

• 인증 준비성: 1 비트 장벽은 하드웨어 설계자를 위한 보편적이고 기계 검증된 인증서를 제공합니다. 이를 통해 평가자들은 특정 매개변수 세트를 재검증하지 않고도 FIPS 140-3 을 위한 바렛 기반 구현을 인증할 수 있습니다.
• 설계 지침: 보안에 대한 주요 아키텍처 요구사항이 신선한 단계 간 마스크임을 명확히 합니다. 이것이 구현된다면, 바렛 감소의 비선형 특성은 무시할 수 있는 1 비트 손실 이상으로 NTT 파이프라인의 보안을 훼손하지 않습니다.
• 방법론적 전환: 이 논문은 사이드 채널 분석을 경험적 시뮬레이션 및 SAT 기반 검사에서 커널 검증 대수적 증명으로 전환하여 PQC 하드웨어 검증의 새로운 표준을 설정합니다.
• 5 개 논문 프로그램 완성: 이 작업은 이전 논문들이 남긴 격차를 메워, 도구 구축 (논문 1) 과 공격 정량화 (논문 2) 에서 대수적 기초 (논문 3), 선형 합성 (논문 4), 그리고 마지막으로 비선형 특성화 (논문 5) 로 이어지는 과정을 마무리합니다.

6. 한계 및 향후 작업

• 합성 증명: 신선한 마스크가 있는 합성 파이프라인에 대해 $\max(k_1, k_2)$가 성립한다는 주장은 현재 관찰일 뿐 형식적 정리는 아닙니다.
• 고차 마스크: 결과는 1 차 마스크 ($t=1$) 로 제한됩니다. 고차 보안을 위해서는 여러 와이어에 걸친 결합 역상을 분석해야 합니다.
• 엔트로피 형식화: 대수적 경계는 증명되었지만, 정보 이론적 최소 엔트로피 경계는 아직 Mathlib 에 완전히 업스트림되지 않은 표준 정의에 의존합니다.
• 다른 감소법: 결과는 바렛 감소에 특화되어 있으며, 몬태고리 및 학교책 (schoolbook) 감소는 별도의 분석이 필요합니다.

요약하자면, 이 논문은 바렛 감소가 1 차 산술 마스크 하에서 근본적으로 안전하며, 파이프라인 단계 사이에 신선한 마스크가 적용된다면 와이어당 1 비트 이하의 정보만 누출함을 확립합니다. 이는 차세대 PQC 하드웨어를 보호하기 위한 엄격한 수학적 기초를 제공합니다.