💻 computer science

Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis

이 논문은 고수준 합성 (HLS) 을 통해 생성된 암호화 하드웨어의 자원 공유로 인한 오검출 문제를 해결하고, 컨트롤러 데이터패치 구조에 대한 상태별 형식 검증을 수행하여 PSCA 보안성을 정확히 검증하는 'MaskedHLSVerif' 도구 흐름을 제안합니다.

원저자: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

게시일 2026-03-20

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

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

🏭 1. 배경: "자동화 공장"과 "보안 요원"

상상해 보세요. 암호화 알고리즘을 만드는 것은 **고가의 보석 (비밀 키)**을 운반하는 것과 같습니다.

보안 요원 (마스킹, Masking): 보석을 훔치지 못하게 하기 위해, 보석을 여러 조각으로 잘게 부순 뒤 각각 다른 상자에 넣고 무작위하게 섞어놓는 작업입니다. 이렇게 하면 도둑이 한 상자를 훔쳐도 보석의 전체 모습을 알 수 없습니다.
자동화 공장 (HLS, High-Level Synthesis): 예전에는 이 복잡한 보안 작업 (상자 나누기, 섞기) 을 사람이 일일이 설계했습니다. 하지만 시간이 너무 걸리고 실수도 많았죠. 그래서 **자동화 공장 (HLS)**을 도입했습니다. 사람이 "보석을 잘게 부셔서 섞어줘"라고 명령만 내리면, 기계가 알아서 회로 설계도를 만들어주는 것입니다.

⚠️ 2. 문제: "자동화 공장의 실수"와 "착각하는 보안 요원"

문제는 이 자동화 공장이 보안보다는 '효율성'과 '속도'에 집중한다는 점입니다.

공장장의 실수: 공장은 자원을 아끼기 위해 여러 작업을 동시에 하거나, 순서를 바꿔서 처리합니다. 예를 들어, "보석을 섞는 순서"를 효율적으로 바꿀 때, 실수로 섞여야 할 조각들이 다시 합쳐져서 보석이 드러나는 실수를 저지를 수 있습니다. (논문의 '재결합' 문제)
착각하는 보안 요원 (기존 검증 도구): 기존에 있던 보안 요원 (REBECCA 같은 도구) 은 "이 회로가 이론상 가능한 모든 경우를 다 해봤을 때, 보석이 드러나는가?"를 확인합니다.
- 착각: 공장은 실제로는 절대 일어나지 않는 상황 (예: A 상자와 B 상자를 동시에 여는 상황) 을 회로에 포함시켰지만, 보안 요원은 "아! 이론상 가능하니까 이건 위험해!"라고 **잘못 경보 (False Positive)**를 울립니다.
- 결과: 실제로는 안전한 회로인데, "보안이 안 됐다"고 해서 공장을 멈추거나 다시 설계하게 되는 낭비가 발생합니다.

💡 3. 해결책: "상태별 감시" (MaskedHLSVerif)

저자들은 이 문제를 해결하기 위해 **새로운 감시 방법 (MaskedHLSVerif)**을 고안했습니다.

기존 방식: "이 공장 전체를 한 번에 훑어보자. 모든 문이 열릴 수 있는가?" (너무 광범위해서 오보가 많음)
새로운 방식 (상태별 감시): "이 공장은 시간순서대로 작동해. 1 시에는 A 문만 열리고, 2 시에는 B 문만 열려. 그러니 1 시에는 A 문만, 2 시에는 B 문만 확인하면 돼!"

비유로 설명하면:
이 공장은 **조명 (컨트롤러)**이 켜지는 순서가 정해져 있습니다.

1 단계 (State 0): 조명 1 번만 켜져서 A 작업만 합니다.
2 단계 (State 1): 조명 1 번은 꺼지고 2 번이 켜져서 B 작업만 합니다.

기존 보안 요원은 "조명 1 번과 2 번이 동시에 켜질 수도 있잖아?"라고 걱정하며 두 조명이 동시에 켜진 상황을 가정하고 경보를 울렸습니다. 하지만 실제로는 절대 동시에 켜지지 않습니다.

저자들의 방법은 **"현재 켜져 있는 조명 (상태) 에만 집중해서, 그 시간에 실제로 작동하는 부품들만 검사한다"**는 것입니다. 이렇게 하면 실제로는 일어나지 않는 상황을 걱정할 필요가 없어져서, 정확한 보안 판정을 내릴 수 있습니다.

🧪 4. 실험 결과: "실제 구멍도 찾아냈다"

이 새로운 방법이 얼마나 좋은지 실험해 보았습니다.

오보 제거: 기존 도구들이 "위험하다"고 했던 안전한 설계들 (6 가지 암호화 예시) 을 다시 검사하니, 실제로는 안전하다는 것을 증명했습니다.
실제 구멍 발견: 공장이 실수로 보안을 해치는 최적화를 적용했을 때 (예: 보석 섞는 순서를 잘못 바꿈), 이 새로운 방법은 **"아! 여기서 보안이 뚫렸다!"**라고 정확히 찾아냈습니다.

🏁 결론

이 논문은 **"자동화 도구 (HLS) 로 만든 암호화 하드웨어는 효율성을 위해 설계가 변형될 수 있으니, 기존의 검증 도구로는 오해를 살 수 있다"**는 것을 지적했습니다.

그리고 **"시간순서대로 (상태별로) 실제 작동하는 부분만 꼼꼼히 검사하는 새로운 방법"**을 제시하여, 불필요한 오보를 줄이고 실제 보안 위협은 정확히 찾아내는 시스템을 만들었습니다.

한 줄 요약:

"자동화 공장이 만든 암호화 기계는 효율을 위해 순서가 바뀔 수 있으니, '모든 가능성'을 다 걱정하는 게 아니라 '지금 이 순간 실제로 돌아가는 부분'만 집중해서 검사해야 진짜 보안을 알 수 있다!"

1. 문제 정의 (Problem Statement)

배경: 암호화 알고리즘의 하드웨어 구현은 전력 부채널 공격 (PSCA, Power Side-Channel Attacks) 에 취약합니다. 이를 방어하기 위해 '마스킹 (Masking)' 기법이 사용되며, 이는 비밀 정보를 무작위 쉐어 (shares) 로 분할하여 처리합니다.
현황: 수동으로 마스킹된 하드웨어를 설계하는 것은 시간 소모적이고 오류가 발생하기 쉽습니다. 따라서 최근에는 검증된 마스킹 소프트웨어를 고수준 합성 (HLS, High-Level Synthesis) 도구를 통해 자동으로 마스킹된 RTL (Register-Transfer Level) 하드웨어로 변환하는 트렌드가 있습니다.
핵심 문제:
1. HLS 최적화의 보안 위협: HLS 는 원래 보안이 아닌 성능 (지연 시간, 면적) 최적화를 위해 설계되었습니다. HLS 가 수행하는 최적화 (표현식 균형 맞추기, 재결합 등) 가 마스킹의 무결성을 해쳐 PSCA 취약점을 유발할 수 있습니다.
2. 기존 검증 도구의 한계 (False Positives): 기존 마스킹 하드웨어 검증 도구 (예: REBECCA) 는 제어기 (Controller) 와 데이터패스 (Datapath) 가 분리된 HLS 생성 설계, 특히 리소스 공유 (Resource-sharing) 를 위해 시간 분할 다중화 (Time-division multiplexed) 된 FSM 기반 설계에 적용 시 거짓 양성 (False Positives) 을 많이 발생시킵니다.
  - 이유: 기존 도구는 FSM 상태와 무관하게 모든 문법적으로 가능한 데이터 경로 (MUX 입력 조합) 를 검증합니다. 그러나 HLS 설계에서는 특정 상태 (State) 에서만 유효한 입력 조합이 존재하며, 다른 조합은 실제로 실행되지 않습니다. 도구가 실행 불가능한 경로를 검증함으로써 불필요한 누출 (Leakage) 을 보고하는 것입니다.

2. 제안된 방법론 (Methodology: MaskedHLSVerif)

저자는 HLS 에서 생성된 마스킹 하드웨어의 정확성을 검증하기 위해 상태 인지형 (State-aware) 검증 흐름인 MaskedHLSVerif 를 제안합니다.

핵심 아이디어: 전체 설계를 검증하는 대신, FSM 의 각 상태 (State) 에 활성화되는 데이터패스만 추출하여 상태별 (State-wise) 로 검증합니다. 이를 통해 실행 불가능한 입력 조합을 배제하고 거짓 양성을 방지합니다.
구체적인 절차:
1. HLS RTL 생성: 마스킹된 C/C++ 코드를 HLS 를 통해 RTL 로 변환합니다.
2. 상태별 설계 분할 (Splitting):
  - HLS 가 생성한 FSM 의 각 상태 ( $S_i$ ) 에 대해 해당 상태에서 실행되는 연산과 데이터패스를 추출합니다.
  - 중요: 현재 상태의 설계 ( $D_i$ ) 를 검증할 때, 이전 상태의 의존적 연산 (Dependent operations) 을 포함하여 재귀적으로 데이터패스를 구성합니다. 이는 중간 신호의 라벨링 (Labeling) 을 원래 입력 신호 기준으로 정확하게 유지하기 위함입니다.
3. 라벨링 (Labeling): 분할된 각 상태별 설계의 입력 신호에 대해 마스킹 쉐어, 랜덤 비트, 공개 값 등을 올바르게 라벨링합니다.
4. 상태별 검증: 분할된 각 설계 ( $D_0, D_1, \dots$ ) 를 기존 검증 도구 (REBECCA) 에 입력하여 순차적으로 검증합니다.
5. 결과 종합: 모든 상태별 설계가 안전하면 전체 설계는 안전하다고 판단합니다. 특정 상태가 실패하면 해당 상태와 그 원인을 식별합니다.

3. 주요 기여 (Key Contributions)

기존 도구의 한계 규명: SOTA(최첨단) 마스킹 검증 도구들이 HLS 생성의 리소스 공유 및 FSM 기반 아키텍처에서 왜 거짓 양성을 발생시키는지 분석하고 그 한계를 명확히 했습니다.
HLS 최적화의 보안 영향 분석: HLS 의 전단 (Front-end, 재결합 등) 및 후단 (Back-end, 스케줄링, 리소스 할당) 최적화가 마스킹 보안에 미치는 구체적인 영향을 사례를 통해 설명했습니다.
새로운 검증 프레임워크 개발: MaskedHLSVerif 라는 형식 검증 방법론을 개발하여, 상태별 유효한 입력 조합만 검증함으로써 HLS 생성 하드웨어의 정확한 보안 평가를 가능하게 했습니다.
광범위한 실험 검증: 6 가지 암호화 벤치마크 (DOM, COMAR, HPC1, HPC2, PRESENT S-box 등) 를 통해 제안된 방법의 유효성을 입증했습니다. 기존 도구 (REBECCA) 가 거짓 양성을 보인 설계들을 본 방법은 올바르게 '안전'하다고 판별했습니다.

4. 실험 결과 (Results)

벤치마크: DOM, COMAR, HPC1, HPC2 의 캐스케이드 멀티플라이어 및 PRESENT 암호의 S-box 등 6 가지 설계.
실험 1 (기존 설계 검증):
- REBECCA 는 FSM 이 포함된 모든 HLS 생성 설계에서 거짓 양성 (False Positive) 을 보고했습니다.
- 반면, MaskedHLSVerif 는 모든 설계가 실제로 안전하다는 것을 정확히 검증했습니다.
- TVLA (Test Vector Leakage Assessment) 실험을 통해 생성된 RTL 이 실제로 1 차 마스킹 보안 (First-order security) 을 만족함을 물리적으로 확인했습니다.
실험 2 (HLS 최적화로 인한 결함 탐지):
- HLS 의 expression balancing 최적화 (재결합) 가 마스킹 로직을 변경하여 보안 결함을 유발하는 시나리오를 인위적으로 생성했습니다.
- MaskedHLSVerif 는 정상적인 설계는 통과시키지만, 최적화로 인해 마스킹이 깨진 2 번째 상태 (State 2) 에서 정확히 보안 결함을 탐지하고 실패를 보고했습니다. 이는 제안된 도구가 HLS 최적화로 인한 실제 보안 위협도 찾아낼 수 있음을 의미합니다.

5. 의의 및 결론 (Significance)

최초의 시도: HLS 를 통해 생성된 마스킹 하드웨어의 형식적 검증을 다룬 최초의 연구로, 자동화된 보안 하드웨어 설계 흐름의 신뢰성을 높이는 중요한 발걸음입니다.
실용성: 설계자는 HLS 를 사용하여 빠르게 마스킹 하드웨어를 생성하되, MaskedHLSVerif 를 통해 생성된 RTL 의 보안성을 자동으로 검증할 수 있게 되었습니다. 이는 설계 시간 단축과 동시에 보안 오류를 방지하는 데 기여합니다.
미래 전망: HLS 최적화가 보안에 미치는 영향은 아직 많이 연구되지 않았습니다. 본 연구는 이러한 최적화 기법들이 보안에 어떤 영향을 미치는지 탐구할 수 있는 기반을 마련했습니다.

요약하자면, 이 논문은 HLS 자동화 흐름에서 발생하는 '거짓 양성' 문제를 해결하고, HLS 최적화로 인한 실제 보안 결함까지 찾아낼 수 있는 새로운 검증 도구 (MaskedHLSVerif) 를 제안하여 암호 하드웨어 설계의 자동화와 보안을 동시에 달성하는 데 기여했습니다.