💻 computer science

Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

이 논문은 117 만 게이트 규모의 양자내성 암호 가속기 (ML-DSA/ML-KEM) 에 대해 구조적 의존성 분석과 다중 단계 검증 계층을 적용하여 수학적 증명을 기반으로 한 사일icon 전 사이드채널 보안 검증을 가능하게 하고, 수백 개의 구조적 플래그를 165 개의 검증 가능한 후보로 축소하여 FIPS 140-3 인증에 필요한 증거 생성을 실현했습니다.

원저자: Ray Iskander, Khaled Kirah

게시일 2026-04-17

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Ray Iskander, Khaled Kirah

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

1. 배경: 왜 이런 연구가 필요한가요?

미래의 양자 컴퓨터는 현재의 암호를 쉽게 뚫을 수 있습니다. 그래서 과학자들은 '양자 내성 암호 (PQC)'라는 새로운 암호 방식을 개발했습니다. 이 암호를 하드웨어 (칩) 로 빠르게 실행하려면 '가속기'라는 특수한 칩이 필요합니다.

하지만 이 칩을 만들면 전력 소모 패턴을 분석하는 해커들이 등장할 수 있습니다. 칩이 계산할 때 전기를 얼마나 쓰는지 보면, 내부의 비밀 키를 추측할 수 있기 때문입니다.

이를 막기 위해 개발자들은 **'마스킹 (Masking)'**이라는 기술을 씁니다.

비유: 중요한 비밀 (비밀 키) 을 한 장의 종이에 적는 대신, **두 장의 반쪽짜리 조각 (Share)**으로 나누어 다른 사람에게 맡기는 것입니다.
원리: 두 조각이 다시 합쳐지기 전까지는 아무도 비밀을 알 수 없습니다. 만약 두 조각이 합쳐지는 순간이 있다면, 그 순간에 해커가 전기를 측정해 비밀을 알아낼 수 있습니다.

2. 문제점: 너무 크고 복잡한 공장은 어떻게 검사할까요?

지금까지의 검사 도구들은 **작은 부품 (수천 개)**만 검사할 수 있었습니다. 하지만 이번 논문에서 다루는 '아담스 브리지 (Adams Bridge)'라는 칩은 117 만 개의 부품으로 이루어진 거대한 공장입니다.

기존 방법의 한계: 모든 부품을 하나하나 세밀하게 검사하려면 시간이 너무 오래 걸려서, 칩을 만들어서 실제 실험을 해보기 전에 검사를 끝낼 수 없습니다.
새로운 접근법: "모든 것을 완벽하게 검사할 순 없다면, 가장 위험한 곳 (비밀 조각이 합쳐지는 곳) 을 먼저 찾아내고, 그중 진짜 위험한 곳만 골라내자"는 전략입니다.

3. 해결책: QANARY (퀸어리) 라는 4 단계 검사 시스템

저자들은 **'QANARY'**라는 새로운 검사 도구를 만들었습니다. 이는 광산에서 유독 가스를 감지했던 '참새 (Canary)'에서 이름을 따왔습니다. 위험을 미리 알려주는 역할을 합니다.

이 도구는 4 단계의 필터를 통해 칩을 검사합니다.

1 단계: 구조적 스캐닝 (D0/D1) - "누가 누구와 만났나?"

비유: 공장 전체를 빠르게 훑어보며, "비밀 조각 A 와 비밀 조각 B 가 만나는 통로가 있나?"를 찾는 것입니다.
결과: 매우 빠릅니다 (수 초). 하지만 "만난다고 해서 무조건 위험한 건 아닐 수도 있다"는 오해 (위양성) 가 생길 수 있습니다. 마치 "두 사람이 만났다고 해서 반드시 범죄를 저지르는 건 아니니까"요.
성능: 117 만 개의 부품 전체를 8.7 초 만에 검사했습니다.

2 단계: 멀티사이클 확장 (MC-D1) - "시간을 두고 추적하기"

비유: 첫 번째 검사에서는 한 번에 만나지 않는 것 같아도, 시간이 지나고 (클록 사이클이 지나고) 레지스터를 거쳐 나중에 만나면 위험합니다. 이 단계에서는 시간을 두고 추적하여 숨겨진 만남을 찾아냅니다.
결과: 12 개의 모듈이 '안전'에서 '위험'으로 재분류되었습니다.

3 단계: 신선한 마스크 확인 (FM) - "새로운 가림막이 있나?"

비유: 두 조각이 만났더라도, 그 사이에 **새로운 무작위 가림막 (Fresh Randomness)**이 끼어들어 비밀을 다시 숨겼다면 안전합니다. 이 단계에서는 그런 '구원자' 같은 가림막이 있는지 확인합니다.

4 단계: 수학적 증명 (SADC) - "진짜로 위험한가?"

비유: 앞서 걸러진 '의심스러운 곳'들 중, **수학적 증명 (Z3, CVC5 라는 두 명의 수학자)**을 통해 "이건 정말로 비밀을 누출하는가?"를 따져봅니다.
결과:
- 198 개: "아, 이건 구조적으로 만났지만 수학적으로 비밀은 안전하군!" -> 안전 판정.
- 165 개: "이건 정말 위험해 보이니 설계자가 다시 확인해 봐야 함." -> 주의 대상.
- 0 개: "모르겠다" -> 없음. (모든 의심 대상에 대해 결론을 내렸습니다.)

4. 성과: 왜 이것이 혁신적인가요?

이 연구의 핵심 성과는 규모와 정확성의 균형을 잡은 것입니다.

거대 규모 처리: 117 만 개의 부품으로 된 칩을 수 분 안에 검사했습니다. 기존 도구로는 불가능했던 일입니다.
현실적인 triage (분류):
- 예전에는 설계자가 수백 개의 의심스러운 신호를 모두 손으로 확인해야 했습니다.
- 이제는 198 개는 "안전"이라는 증명서를 받고, 165 개만 집중해서 고치면 됩니다.
- 이는 설계자의 업무를 90% 이상 줄여주면서, 수학적으로 증명된 안전성을 제공합니다.
이중 검증: 모든 결론을 두 개의 다른 수학 프로그램 (Z3 와 CVC5) 으로 다시 확인하여, 오류가 없음을 보장했습니다.

5. 결론: 이 연구가 의미하는 바

이 논문은 **"완벽한 검사는 불가능할지라도, 현실적인 규모에서 '안전한 곳'과 '위험한 곳'을 빠르게 구분해 주는 지능형 필터"**를 제시합니다.

마치 공항 보안 검색과 같습니다.

예전에는 모든 승객을 수색하는 데 너무 오래 걸려서 비행기가 뜨지 못했습니다.
이 새로운 방법은 위험한 소지품 (비밀 조각의 합체) 을 가진 사람만 빠르게 찾아내고, 나머지는 "안전"이라고 증명해 줍니다.

이 덕분에 양자 시대를 대비한 암호 칩을 설계할 때, **실제 칩을 만들어보기 전 (Pre-silicon)**에 해킹 위험을 미리 발견하고 수정할 수 있게 되어, 더 안전하고 빠른 양자 내성 암호 시스템을 만들 수 있게 되었습니다.

1. 문제 제기 (Problem Statement)

배경: ML-KEM (FIPS 203) 과 ML-DSA (FIPS 204) 의 표준화 완료로 인해, 양자 내성 암호를 위한 하드웨어 가속기 개발이 가속화되고 있습니다. 이러한 하드웨어는 FIPS 140-3 인증을 받기 위해 사이드 채널 공격 (Side-Channel Attack) 에 대한 저항성을 입증해야 합니다.
현재의 한계:
- 기존 정밀한 마스크링 검증 도구들 (SILVER, Prover, Coco-Alma 등) 은 주로 부울 (Boolean) 마스크링과 소규모 회로 (수천 게이트) 에 국한되어 있습니다.
- PQC 하드웨어는 대규모 산술 연산 (Arithmetic Masking) 과 깊은 파이프라인을 포함하며, 단일 사이클 분석만으로는 레지스터를 넘어선 다중 사이클 의존성 (Multi-cycle dependency) 을 포착하지 못합니다.
- 수천만 게이트 규모의 생산급 (Production-scale) 회로에 대해 정밀한 형식 검증 (Formal Verification) 을 수행하는 것은 계산 비용이 너무 커서 현실적으로 불가능합니다.
목표: 대규모 NTT 하드웨어에서 1 차 프로빙 보안 (First-order Probing Security) 을 검증할 수 있는 확장 가능하면서도 엄밀한 (Sound) 자동화 도구 개발.

2. 방법론 (Methodology)

저자들은 4 단계 계층적 검증 프레임워크를 제안하며, 이는 구조적 분석의 확장성을 유지하면서 정밀도를 점진적으로 높이는 방식입니다.

1 단계: 구조적 의존성 분석 (D0/D1 Structural Dependency Analysis)

원리: 비밀 정보의 두 개 share( $s_0, s_1$ ) 가 조합 논리 경로를 통해 하나의 와이어 (Wire) 에 수렴하는지 확인합니다.
D0/D1 쿼리: 특정 와이어가 $s_0$ 에만 의존하거나 $s_1$ 에만 의존하는지 (즉, 두 share 모두에 의존하지 않는지) SMT 솔버 (Z3) 를 통해 확인합니다.
특징:
- 단일 사이클 (SC-D1): 한 클록 주기 내의 조합 논리만 분석.
- 다중 사이클 (MC-D1): 레지스터 (DFF) 를跨越하는 의존성을 고정점 반복 (Fixed-point iteration) 을 통해 분석. 이를 통해 레지스터 경계를 넘어 share 가 합쳐지는 "수렴점 (Convergence Points)"을 발견합니다.
- 성능: 117 만 셀 규모의 Adams Bridge 가속기 전체를 단 8.7 초 (SC-D1) 및 231.8 초 (MC-D1) 에 분석 완료.

2 단계: 신선한 마스크 정제 (Fresh Masking Refinement, FM)

구조적으로 insecure 로 판명된 와이어 중, 새로운 무작위성 (Fresh Randomness) 이 XOR 마스크 역할을 하여 보안을 보장하는 경우를 식별하여 'Secure'로 재분류합니다.

3 단계: 부울 SADC (Boolean SADC)

구조적 플래그가 남은 와이어에 대해, share 와 비밀 값의 대수적 관계를 재파라미터화 (Reparametrization) 하여 값의 독립성을 검증합니다. 부울 마스크링 ( $s_0 = x \oplus s_1$ ) 에 적용됩니다.

4 단계: 산술 SADC (Arithmetic SADC) - 핵심 기여

문제: PQC 는 모듈로 연산 ( $s_0 = (x - s_1) \mod q$ ) 을 사용하므로 부울 SADC 는 부적합합니다.
해결: 모듈로 뺄셈 semantics 을 유지하면서 $S_0 = (X - S_1) \mod q$ 형태로 재파라미터화하여, 와이어의 값이 비밀 $X$ 에 의존하지 않는지 (Value-independence) 검증합니다.
이중 솔버 검증: 모든 산술 SADC 쿼리는 Z3 와 CVC5 두 개의 독립적인 솔버로 교차 검증되어 결과의 신뢰성을 확보합니다.

3. 주요 기여 (Key Contributions)

생산급 규모의 구조적 의존성 검증: 117 만 셀 (30 개 모듈) 규모의 Adams Bridge ML-DSA/ML-KEM 가속기 전체를 분석 가능한 첫 번째 도구입니다.
다중 사이클 구조적 재분류 (MC-D1): 단일 사이클 분석에서는 'Clean'으로 분류되던 12 개의 모듈이 다중 사이클 분석을 통해 'Insecure'로 재분류되었습니다. 이는 레지스터 경계를 넘는 share 수렴을 포착했기 때문입니다.
산술 마스크링을 위한 4 단계 계층 및 SADC: 5,543 셀 규모의 ML-KEM Barrett 모듈에서 363 개의 구조적 플래그 중 198 개 (54.5%) 를 기계적으로 검증된 'Secure'로 판명하고, 나머지 165 개를 '검토 대상 (Candidate Insecure)'으로 좁혔습니다. 이는 정밀한 검증 도구의 한계를 극복하고 설계자가 수동 검토해야 할 범위를 획기적으로 줄였습니다.
이중 솔버 검증 및 재현성: 모든 산술 검증 결과를 Z3 와 CVC5 로 일치시켰으며 (0 건의 불일치), 모든 실험 환경과 버전이 고정된 Docker 이미지를 제공하여 재현성을 보장합니다.

4. 실험 결과 (Results)

대상: Adams Bridge (CHIPS Alliance/Caliptra 프로젝트) 의 30 개 마스크링 모듈 (총 117 만 셀).
분석 속도:
- SC-D1: 전체 27 개 모듈 분석 완료 (8.7 초).
- MC-D1: 전체 27 개 모듈 분석 완료 (231.8 초).
정확도 및 효율성 (Barrett Reduction 모듈 기준):
- D0/D1: 363 개의 insecure 와이어 플래그.
- FM: 0 개 개선 (산술 마스크링 특성상 적용 불가).
- 부울 SADC: 146 개를 'Insecure'로 확정, 217 개를 'Indeterminate'로 남김 (연산 비용 초과).
- 산술 SADC: 198 개를 'Secure'로 승격, 165 개를 'Candidate Insecure'로 확정, 0 개 Indeterminate.
- 결과: 설계자가 수동으로 검토해야 할 와이어를 363 개에서 165 개로 줄였으며, 198 개에 대해서는 수학적으로 검증된 'Secure' 인증서를 발급했습니다.
교차 검증:
- Coco-Alma (정밀 SAT 기반 도구) 와의 비교에서, 구조적 분석이 포착한 'Insecure' 영역은 모두 실제 누출과 일치함을 확인 (False Negative 0).
- DOM AND 게이트와 같은 표준 벤치마크에서는 구조적 오검증 (False Positive) 을 100% 제거하여 Ground Truth 와 일치함을 입증했습니다.

5. 의의 및 결론 (Significance)

확장성과 정밀도의 균형: 기존 정밀 검증 도구는 소규모 회로에 국한되었으나, 이 도구는 생산급 대규모 회로에서도 Sound (안전한 상한선) 한 검증을 제공합니다.
실무적 가치: 수백 개의 구조적 경고 (Structural Flags) 를 설계자가 즉시 조치할 수 있는 165 개의 'Actionable Candidates'와 198 개의 'Secure Certificates'로 변환하여, FIPS 140-3 인증을 위한 Pre-silicon (실리콘 전) 사이드 채널 증거 생성을 가능하게 합니다.
보완적 접근: 구조적 분석 (어디서 정보가 흐를 수 있는지), 정밀 형식 검증 (특정 와이어가 안전한지), 물리적 측정 (실제 누출 여부) 은 상호 보완적입니다. 이 도구는 대규모 설계에서 정밀 검증이 불가능한 영역을 선별하여 검증 비용을 절감하는 필터 (Filter) 역할을 수행합니다.
한계 및 향후 과제: 현재는 1 차 프로빙 모델과 표준 프로빙 모델 (Glitch 무시) 에 기반하며, 고차 마스크링 ( $d \ge 2$ ) 이나 Glitch 확장 모델로의 확장은 향후 과제로 남았습니다. 또한, 165 개의 'Candidate Insecure' 중 일부는 분포적 보안 (Distributional Security) 을 만족할 수 있으나, 현재 가치 독립성 (Value-independence) 기준으로는 상한선으로 처리됩니다.

요약하자면, 이 논문은 포스트 양자 암호 하드웨어의 보안 검증에 있어, 기존 정밀 도구의 확장성 한계를 극복하고 대규모 산술 회로에서도 신뢰할 수 있는 보안 증거를 생성할 수 있는 새로운 자동화 프레임워크를 제시했습니다.