기술 요약: 하드웨어 설계의 정보 흐름을 위한 증강 심볼릭 실행 (Augmented Symbolic Execution)

문제 정의

하드웨어 설계의 보안성을 검증하려면 소스 신호(입력)에서 싱크 신호(출력)로 정보가 어떻게 흐르는지 분석해야 합니다. 원치 않는 흐름은 액세스 권한 위반, 메모리 유출 또는 권한 상승으로 이어질 수 있습니다. 심볼릭 실행(Symbolic Execution, SE)은 계측 없이 이러한 흐름을 추적할 수 있는 정밀한 도구이지만, 분기점(branch points)에 따라 실행 경로의 수가 기하급수적으로 증가하는 "경로 폭발(path explosion)" 문제에 직면합니다. 또한, 하드웨어 설계는 멀티 클록 사이클 추론을 통해 복잡성을 더하며, 이로 인해 입력에서 출력까지의 완전한 흐름을 실현하는 것이 어려워집니다. 기존 솔루션들은 설계 공간을 제한하거나 작은 핵심 컴포넌트만을 분석하는 경우가 많습니다.

핵서 해결하고자 하는 핵심 과제는 제한된 시간 내에 실현 가능한 정보 흐름(데이터가 실제로 이동하는 실제 경로)과 실현 불가능한 경로(실행 시 발생할 수 없는 정적 분석의 결과물)를 효율적으로 구별하고, 이러한 흐름을 유도하기 위한 구체적인 입력 시퀀스를 제공하는 것입니다.

방법론: SEIF

저자들은 정적 분석을 심볼릭 실행과 결합하여 정보 흐름 경로를 검증하고 명시화하는 방법론인 SEIF(발음: "safe")를 제시합니다. SEIF는 Verilog RTL 설계 내의 신호 연결성을 과대 근사(over-approximate)하는 정적으로 구축된 정보 흐름(Information Flow, IF) 그래프를 기반으로 작동합니다.

이 방법론은 다음 세 가지 주요 단계로 진행됩니다.

1. 전역적으로 실현 불가능한 경로 제거 (Pruning Globally Unrealizable Paths)

심볼릭 실행을 호출하기 전에, SEIF는 IF 그래프를 분석하여 논리적으로 불가능한 경로를 제거합니다.

• 세그멘테이션(Segmentation): IF 경로는 클록 사이클 경계를 나타내는 논블로킹 할당(non-blocking assignments)을 기준으로 세그먼트로 나뉩니다.
• 제약 조건 확인(Constraint Checking): 각 세그먼트에 대해 흐름이 발생하기 위해 필요한 조건들을 수집합니다. SMT 솔버는 **공동 만족 가능성(co-satisfiability)**을 체크합니다. 만약 단일 클록 사이클 세그먼트 내의 제약 조건들이 서로 모순된다면(예: 신호가 동시에 high이면서 low이어야 하는 경우), 해당 경로는 전역적으로 실현 불가능한 것으로 간주하여 폐기합니다.

2. 가이드형 심볼릭 실행 (Guided Symbolic Execution)

남은 경로들에 대해, SEIF는 설계 상태를 통해 실현 가능한 실행 경로를 찾기 위해 IF 그래프에 의해 가이드되는 심볼릭 실행을 수행합니다.

• 가이드 탐색(Guided Search): 실행 엔진은 현재 IF 그래프 세그먼트를 실현하는 데 필요한 특정 코드 라인을 포함하는 설계 경로만을 따르도록 제한됩니다. 이는 탐색 공간을 크게 줄여줍니다.
• 클록 사이클 경계 프루닝(Clock Cycle Boundary Pruning): 각 클록 사이클에서 엔진은 현재의 심볼릭 상태가 다음 IF 세그먼트의 조건을 만족하는지 확인합니다. 만족하지 않는 경우, 해당 브랜치로 이어지는 경로를 프루닝합니다.
• 스톨링 전략(Stalling Strategy): 핵심적인 혁신은 IF 경로의 진행을 "스톨(stall, 지연)"시키는 능력입니다. 현재 상태가 다음 세그먼트의 조건을 만족할 수 없는 경우, SEIF는 IF 경로 포인터를 진전시키지 않고 머신 상태를 진전시키기 위해 설계를 한 클록 사이클 동안 심볼릭하게 실행합니다. 결정적으로, 스톨링 중에는 SEIF가 이전 세그먼트에서 축적된 정보(예: 레지스터가 초기화되는 것을 방지)를 덮어쓰는 경로를 탐색하지 못하도록 차단합니다.
• 탐색 휴리스틱(Search Heuristics): 본 논문은 네 가지 탐색 전략을 평가합니다:
  1. Baseline 1: 계속 진행 또는 스톨만 수행 (조합의 전수 탐색).
  2. Baseline 2: 백트래킹만 수행 (스톨링 없음).
  3. 스톨링과 백트래킹 병행: 하이브리드 접근 방식.
  4. UNSAT Core 휴리스틱을 사용한 스톨링: 제약 조건 충돌을 줄이는 스톨 경로를 우선시하기 위해 SMT 솔버의 UNSAT core를 사용하여, 유효한 다음 상태를 향해 탐색을 효과적으로 유도합니다.

3. 시맨틱 분석 및 후처리 (Semantic Analysis and Post-Processing)

• 진정한 흐름 검증(True Flow Verification): 텍스트 상의 흐름은 존재하지만 실제 정보 전달은 일어나지 않는 "거짓 양성(false positives)" 사례(예: y = x XOR x)를 제거하기 위해 시맨틱 체크를 수행합니다.
• 리셋 상태 검증(Reset State Verification): 도구는 발견된 실행 경로가 설계의 리셋 상태로부터 도달 가능한지 확인합니다. 도달 불가능하다면, 해당 경로가 중간 상태에서 시작된 것으로 식별합니다.

주요 기여

1. SEIF의 정의: 하드웨어의 정보 흐름을 분석하기 위해 정적 분석(IF 그래프)과 가이드형 심볼릭 실행을 결합한 새로운 방법론을 정의했습니다.
2. 구현: Z3 솔버를 활용하여 Sylvia 심볼릭 실행 엔진과 Hyperflow 그래프 툴체인 위에 구축된 도구 구현을 제시했습니다.
3. 탐색 휴리스틱: 멀티 클록 사이클 경로 탐색의 복잡성을 관리하기 위해, 특히 스톨링을 가이드하는 UNSAT core 사용을 포함한 특정 탐색 전략을 개발하고 평가했습니다.
4. 평가: 네 가지 오픈 소스 설계(OR1200, openMSP430, AKER Access Control, AES 코어)에 대한 종합적인 테스트를 수행했습니다.

결과

평가는 12 코어와 62GB RAM을 갖춘 듀얼 소켓 서버에서 수행되었습니다.

• 경로 계수(Path Accounting): SEIF는 정적으로 구축된 IF 그래프의 경로 중 **86~90%**를 성공적으로 계수했습니다. 이는 실현 가능한 설계 경로를 찾아내거나 해당 경로가 불가능함을 증명함으로써 달성되었습니다.
• 진정한 흐름(True Flows): 계수된 경로 중 **58~77%**가 진정한 정보 흐름으로 식별되었으며, 이는 정적 IF 그래프가 강력한 근사치임을 나타냅니다.
• 성능: SEIF는 평균 4~6초 내에 10~12 클록 사이클 깊이까지 경로를 전수 탐색할 수 있습니다.
• 탐색 전략 효용성: UNSAT Core 휴리스틱은 다른 전략들보다 성능이 우수하여, 베이스라인보다 실현 가능한 설계 경로를 26% 더 자주 찾아냈으며, 경로당 평균 탐색 시간을 3~6초로 단축했습니다. 또한 비휴리스틱 접근 방식에 비해 백트래킹 빈도를 크게 줄였습니다.
• 확장성(Scalability): MSP430 프로그램 카운터에 대한 케이스 스터디에서, SEIF는 16 클록 사이클 탐색 범위 내에서 19,060개의 IF 경로 중 **89.93%**에 대한 설계 경로를 찾아냈습니다.

의의 및 주장

본 논문은 SEIF가 정적 분석의 결과물과 실제 보안 위반을 구분하는 과정을 자동화함으로써 보안 검증의 새로운 관점을 제공한다고 주장합니다.

• 정밀도: 엔지니어가 복잡한 멀티 사이클 흐름을 수동으로 추적하거나 입력 시퀀스를 추측할 필요를 없애줍니다.
• 실행 가능성(Actionability): 위반이 발견되면, SEIF는 리셋 또는 중간 상태로부터 설계를 위반 경로로 유도하기 위한 구체적인 입력 값 시퀀스를 제공합니다.
• 효율성: 정적 IF 그래프를 사용하여 심볼릭 실행을 가이드함으로써, 순수 심볼릭 실행의 고질적인 문제인 경로 폭발 문제를 피하고, 순수 SE보다 더 깊은 클록 사이클과 더 큰 설계를 분석할 수 있게 합니다.
• 한계: 저자들은 SEIF가 명세 및 설계상의 무해한 인적 오류로 인한 결함을 타겟으로 한다는 점을 인정합니다. 이 도구는 검증 이후에 삽입된 악의적인 합성 도구, 제조 또는 공급망 공격(예: 아날로그 트로잔)으로 인한 결함은 탐지할 수 없습니다. 또한, 재수렴 팬아웃(reconvergent fan-out) 시나리오의 경우, 모든 설계 경로를 전수 조사하지 못하면 잘못된 결과를 보고할 수 있습니다.