💻 computer science

Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs

이 논문은 하드웨어 설계를 위한 새로운 심볼릭 실행 기법인 piecewise composition을 소개하며, 이는 모듈형 구조를 활용하여 경로 탐색 작업을 SMT 솔버로 오프로드함으로써, 넷리스트 변환 없이 RTL Verilog를 직접 분석하면서도 실행 시간을 97% 단축하고 탐색된 경로 수를 10배가량 감소시킨다.

원저자: Kaki Ryan, Cynthia Sturton

게시일 2026-07-22

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Kaki Ryan, Cynthia Sturton

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

당신이 거대하고 미래적인 도시 내부의 미스터리를 풀려는 탐정이라고 상상해 보십시오. 이 도시는 당신의 휴대폰부터 지구 궤도를 도는 위성까지 모든 것을 제어하는 작은 실리콘 조각인 컴퓨터 칩입니다. 이 도시가 안전한지 확인하기 위해, 당신은 나쁜 놈들이 몰래 들어오거나 규칙을 어기지 못하도록 모든 거리, 골목, 그리고 숨겨진 문을 일일이 점검해야 합니다. 이 과학 분야를 '하드웨어 검증(hardware verification)'이라고 부르며, 이는 다리가 무너지기 전에 차가 지나갈 수 있는지 확인하는 안전 검사관의 디지털 버전과 같습니다.

탐정들이 이 업무에 사용하는 주요 도구는 '심볼릭 실행(symbolic execution)'이라고 불립니다. 특정 열쇠를 들고 한 번에 한 거리씩 걸어가는 대신, 심볼릭 실행은 마치 모든 가능한 거리를 동시에 걸을 수 있게 해주는 마법의 지도와 같습니다. 당신은 구체적인 숫자 대신 어떤 숫자든 나타낼 수 있는 '유령(ghosts)'을 배치하고, 그 유령 같은 가능성들에 대해 도시가 어떻게 반응하는지 관찰합니다. 문제는 도시가 커지고 복잡해질수록, 체크해야 할 거리의 수가 너무 빠르게 늘어나서 모든 곳을 확인하는 것이 불가능해진다는 점입니다. 이것을 '경로 폭발 문제(path explosion problem)'라고 합니다. 이는 마치 소방 호스에서 나오는 물을 마시려는 것과 같습니다. (물 혹은 이 경우에는 체크해야 할 경로의 수가) 너무 빠르게 쏟아져 나와서, 누출 지점을 찾기도 전에 압도당하게 됩니다. 만약 우리가 모든 경로를 확인할 수 없다면, 해커들이 비밀을 훔치거나 시스템을 마비시키기 위해 사용할 수 있는 숨겨진 함정을 놓칠 수도 있습니다.

여기서 "하드웨어 설계의 심볼릭 실행에서 발생하는 경로 폭발 문제 해결(Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs)"이라는 논문이 등장합니다. 저자인 카키 라이언(Kaki Ryan)과 신시아 스터튼(Cynthia Sturton)은 '피스와이즈 컴포지션(piecewise composition, 구간별 합성)'이라는 영리한 새로운 전략을 소개합니다. 도시 전체를 한꺼번에 가로지르려 하는 대신, 그들은 도시가 여러 '구역(neighborhoods/blocks)'으로 나누어 지어져 있다는 사실을 깨달았습니다. 각 구역을 별도로 탐색하여 해당 구역 내의 모든 가능한 경로를 지도화한 다음, 초지능형 계산기(SMT 솔버라고 불리는)를 사용하여 이 분리된 지도들이 어떻게 서로 맞물리는지 파악하는 방식입니다.

이것은 마치 거대한 직소 퍼즐을 푸는 것과 같습니다. 기존의 방식은 모든 조각을 하나씩 억지로 끼워 맞추며 그림이 나타나기를 바라는 것이었습니다. 만약 퍼즐 조각이 백만 개라면, 영원히 걸릴 것입니다. 새로운 '피스와이즈 컴포지션' 방식은 먼저 조각들을 관리 가능한 작은 더미로 분류하는 것과 같습니다. '하늘' 더미를 풀고, 그다음 '바다' 더미를 풀고, 그다음 '나무' 더미를 푸는 식입니다. 일단 이 작은 더미들에 대한 해답을 얻으면, 그것들이 어떻게 연결되는지 빠른 검사를 통해 확인합니다. 이 논문은 이 접근 방식이 단순히 조금 도움이 되는 수준이 아니라, 작업량을 획기적으로 줄여준다는 것을 보여줍니다. 복잡한 CPU와 시스템 온 칩(SoC)을 포함한 다섯 가지 서로 다른 오픈 소스 설계를 대상으로 한 테스트에서, 이 방식은 엔진이 탐색해야 하는 경로의 수를 약 92%에서 99%까지 줄였습니다.

결과는 놀라웠습니다. 새로운 엔진은 기존 방식보다 97% 더 빠르게 실행되었습니다. 또한, 이전에는 철저히 확인하기 너무 어려웠던 설계들에서 보안 버그와 규칙 위반을 성공적으로 찾아냈습니다. 예를 들어, OR1200이라는 특정 프로세서 코어를 테스트했을 때, 이 엔진은 알려진 30개의 버그 중 27개를 찾아냈는데, 이는 기존 도구들이 찾아낸 수보다 많았습니다. 저자들은 이것이 단순한 이론적 아이디어가 아님을 강조합니다. 그들은 칩을 만드는 데 사용되는 실제 코드(Verilog)를 읽고, 버그가 존재함을 증명하는 특정 명령 세트인 '카운터-예제(counter-example)'를 생성하는 작동하는 도구를 직접 만들었습니다.

하지만 이 논문은 이 방법이 모든 것을 즉시 해결해 주는 마법 지팡이는 아니라는 점을 주의 깊게 언급합니다. 이 방법은 하드웨어가 모듈식으로 설계되어, 각 블록이 혼란스럽게 겹치지 않고 명확히 구분되어 있다는 전제하에 작동합니다. 만약 설계에 특정 종류의 복잡한 연결(예: 두 부분이 동시에 동일한 메모리에 쓰려고 시도하는 '쓰기-쓰기' 의존성)이 있다면, 도구는 추측하는 대신 멈추고 에러를 보고합니다. 그러나 잘 구조화된 대다수의 하드웨어 설계에 있어서, 이 새로운 접근 방식은 가능성의 소방 호스를 길들이고, 우리의 디지털 도시를 더 안전하고 견고하며 미래를 향해 준비할 수 있게 만드는 길을 제시합니다.

기술 요약: 하드웨어 설계의 심볼릭 실행(Symbolic Execution)에서 발생하는 경로 폭발 문제 해결

문제 정의
심볼릭 실행은 구체적인 입력 값을 기호(symbol)로 대체하여 가능한 모든 실행 경로를 탐색함으로써 하드웨어 설계에 대한 검증을 일반화할 수 있는 강력한 도구입니다. 그러나 이는 "경로 폭발(path explosion)" 문제로 인해 심각한 어려움을 겪습니다. 전통적인 심볼릭 실행에서는 설계 내의 분기점(제어 흐름 문장) 수에 따라 탐색해야 할 경로의 수가 기하급급수적으로 증가합니다. 복잡한 하드웨어 설계의 경우, 이러한 지수적 성장은 전체 탐색을 계산적으로 불가능하게 만듭니다. 이를 완화하기 위한 기존의 시도들은 심볼릭 실행을 모델 체킹과 결합하거나, 구체적인 실행 트레이스를 활용하거나, 분석 범위를 작은 설계로 제한하는 방식이었으나, 이러한 접근법들은 대규모의 실제 레지스터 전송 레벨(RTL) 설계를 확장하는 데 한계가 있었습니다.

방법론: 조각별 합성 (Piecewise Composition)
저자들은 하드웨어 설계의 고유한 모듈 구조를 활용하여, 경로 탐색의 부담을 심볼릭 실행 엔진에서 만족 가능성 모듈로 이론(SMT) 솔버로 전환하는 기술인 **조각별 합성(piecewise composition)**을 소개합니다.

핵심 개념: 설계를 하나의 거대한 단일 제어 흐름 그래프로 탐색하는 대신, 이 접근법은 설계를 독립적인 블록(구체적으로 Verilog always 블록)으로 분해합니다. 엔진은 각 클록 사이클마다 각 독립적인 블록을 정확히 한 번씩 심볼릭하게 탐색하여, 각 블록에 대한 경로 파편(fragment) 집합(트리)을 생성합니다.
SMT를 통한 합성: 전체 루트-리프(root-to-leaf) 경로를 재구성하거나 어설션(assertion)을 검증하기 위해, 엔진은 SMT 솔버를 사용하여 이러한 독립적인 경로 파편들을 합성합니다. 솔버는 각 블록의 경로 조건 및 심볼릭 스토어(symbolic store)를 기반으로 특정 파편들을 결합하는 것이 가능한지 여부를 확인합니다.
복잡도 감소: $N$ 개의 독립적인 always 블록이 있고 각 블록이 최대 $b$ 개의 이진 분기점을 포함하는 설계의 경우, 전통적인 심볼릭 실행은 $O(2^{bN})$ 개의 경로를 탐색해야 합니다. 조각별 합성은 이를 $O(2^b \cdot N)$ 개의 경로 탐색으로 줄여줍니다. 복잡도는 단일 블록 내의 분기점에 대해서만 지수적으로 증가하며, 블록의 수에 대해서는 선형적으로 증가합니다.
의존성 처리: 본 방법론은 블록 간의 다양한 데이터 의존성을 고려합니다.
- Read-Read: 블록들을 별도로 탐색할 수 있습니다. SMT 솔버는 공유 변수가 충돌하는 불가능한 조합을 필터링합니다.
- Read-Write: 비차단 할당(non-blocking assignments)을 통해 한 블록에서의 업데이트가 동일 사이클 내의 다른 블록에서의 읽기에 충돌을 일으키지 않도록 보장합니다.
- Write-Write: 도구는 Verilog 권장 사항을 위반하는 쓰기-쓰기(write-write) 의존성을 감지하고 에러를 발생시킵니다.
구현 세부 사항: 엔진은 C나 네트리스트(netlist)로의 변환 없이 Verilog RTL 상에서 직접 작동합니다. 순차 블록(sequential blocks)을 탐색한 후 "더티(dirty)" 신호를 기반으로 할당을 재평가함으로써 조합 논리(combinational logic)를 처리합니다. 또한 사이클 경계에서 상태를 병합하여 여러 클록 사이클을 지원하며, 반복되는 서브모듈 처리(SMT를 통한 결과 병합) 및 무관한 블록을 제거하기 위한 영향 범위(Cone of Influence, COI) 분석과 같은 최적화를 포함합니다.

주요 기여

조각별 합성의 정의: 경로 폭발에 대응하기 위해 경로 결합 로직을 SMT 솔버로 전이함으로써 하드웨어 모듈성을 활용하는 공식적인 기법을 정의했습니다.
심볼릭 실행 엔진: 조각별 합성을 활용하여 Ver source code 상에서 직접 작동하는 Verilog RTL용 사이클 정밀(cycle-accurate) 엔진을 설계 및 구현했습니다.
실증적 평가: OR1200, PULPissimo, openMSP430 등을 포함한 5개의 오픈 소스 설계와 84개의 보안 핵심 어설션을 사용하여 종합적인 평가를 수행했습니다.

결과
평가는 성능의 유의미한 향상과 어설션 위반 발견 능력을 입증합니다:

경로 감소: 조각별 합성은 기존 심볼릭 실행과 비교했을 때 방문하는 코드 라인 수를 92%~~99%, 분기점 방문 횟수를 64%~~99% 감소시킵니다.
실행 시간: 이 기술은 전체 실행 시간을 평균 97% 단축합니다. MC68HC11 SPI의 전체 탐색에서, 엔진은 베이스라인이 요구하는 코드 라인의 약 7%, 분기점의 약 4%만을 탐색했습니다.
솔버 효율성: 합성이 SMT 쿼리 복잡도를 폭발시킬 수 있다는 우려와 달리, 탐색된 경로의 감소는 SMT 쿼리 수의 평균 18% 감소와 솔버 시간의 21% 감소를 이끌어냈습니다.
버그 탐지: 엔진는 5개의 설계 모두에서 어설션 위반을 성공적으로 찾아냈습니다. 구체적으로 Hack@DAC SoC에서 31개 중 24개의 버그를, OR1200 프로세서에서 30개 중 27개의 버그를 식별했습니다.
비교: 본 도구는 유사한 설계에서 취약점을 찾는 데 2분 미만이 소요된 반면, 기존의 최첨단 도구들(예: Coppelia, RTLConTest)은 유사한 취약점을 찾는 데 수 시간이 걸렸습니다.

의의 및 주장
본 논문은 조각별 합성이 RTL 수준 분석의 세밀함을 희생하지 않으면서 대규모 하드웨어 설계를 위한 심볼릭 실행의 규모를 확장할 수 있는 실행 가능한 경로를 제공한다고 주장합니다. 독립적인 하드웨어 모듈의 탐색을 분리하고 현대적인 SMT 솔버를 사용하여 이를 재결합함으로써, 이 접근법은 개별 경로 정보를 유지하면서도 탐색 공간의 지수적 증가를 완화합니다. 저자들은 이 방법이 이전에 심볼릭 실행이 불가능했던 복잡한 SoC 및 CPU의 검증을 가능하게 하며, 원래의 RTL 설계로 직접 추적 가능한 정밀한 반례(counter-example)를 제공한다고 주장합니다. 이 연구는 실세계 설계에서 어설션 위반 및 잠재적 취약점을 탐지할 수 있게 함으로써 하드웨어 보안 검증의 진보를 보여줍니다.

유사한 논문