ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification

1. 문제 정의 (Problem Statement)

현대 시스템 온 칩 (SoC) 은 복잡한 IP 블록으로 구성되며, 공급망의 불신과 악성 제 3 자 IP 사용으로 인해 보안 취약점에 노출되어 있습니다. 기존 보안 검증 방법론은 다음과 같은 한계를 가집니다.

• 수동 의존성 및 확장성 부족: 기존 위협 모델링 (Threat Modeling) 은 수동으로 수행되어 오류가 발생하기 쉽고, 설계 복잡도와 공격 벡터의 증가를 따라가지 못합니다.
• 지식 활용의 부재: CWE(Common Weakness Enumeration), CVE, CAPEC 등 방대한 취약점 데이터베이스가 존재하지만, 이를 SoC 설계에 체계적으로 적용하여 자동화된 검증으로 연결하는 방법이 부족합니다.
• 검증 도구의 한계: 정형 검증 (Formal Verification) 은 강력한 도구이지만, 이를 위해서는 설계 의도를 반영한 정확한 '속성 (Assertion)'을 수동으로 작성해야 하며, 이는 전문 지식과 막대한 노력이 요구됩니다.
• LLM 의 일반화 부족: 최근 LLM 을 활용한 속성 생성 연구들은 특정 취약점에만 국한되거나, 전체 CWE 공간에 걸쳐 일반화되지 못하는 '임의적 (Ad-hoc)' 접근법을 취하고 있습니다.

2. 방법론 (Methodology)

논문에서 제안하는 ATLAS는 LLM(대형 언어 모델) 을 활용하여 표준화된 위협 모델링과 속성 기반 정형 검증을 연결하는 통합 프레임워크입니다. 주요 흐름은 다음과 같습니다.

A. 자산 중심 위협 모델링 (Asset-Centric Threat Modeling)

1. 표준화된 템플릿: 공격자 (Adversary), 자산 (Assets), 공격 표면 (Attack Surfaces), 취약점 (Vulnerabilities), 위협 (Threats) 을 정의하는 표준 템플릿을 도입하여 일관된 위협 모델 생성을 보장합니다.
2. 위협 모델 데이터베이스 (TMDB) 구축:
   • MITRE 의 CWE, CVE, CAPEC 데이터를 기반으로 LLM(GPT-5) 을 활용하여 각 하드웨어 취약점 (CWE) 마다 표준 템플릿에 맞는 위협 모델을 자동 생성합니다.
   • 인간 전문가의 피드백을 통해 검증된 고품질 예시 데이터를 기반으로 LLM 을 학습시켜, 모든 알려진 하드웨어 CWE 에 대한 포괄적인 TMDB 를 구성합니다.
3. SoC 특화 자산 탐지:
   • SoC 의 RTL(Register Transfer Level) 코드를 분석하여 보호해야 할 민감한 자산 (예: 상태 머신, 키, 인증 데이터 등) 을 식별합니다.
   • 식별된 자산과 TMDB 를 매핑하여 해당 설계에 적용 가능한 구체적인 위협 모델과 CWE 를 도출합니다.

B. 컨텍스트 기반 정형 검증 (Context-Aware Formal Verification)

식별된 위협 모델을 정형 검증용 속성 (SystemVerilog Assertions, SVA) 으로 변환하는 과정에서 LLM 의 정확도를 높이기 위해 3 가지 핵심 컨텍스트를 제공합니다.

1. 설계 문서 (Design Documents, DD): 명세서, 레지스터 맵, 권한 규칙 등 RTL 에 명시되지 않은 설계 의도와 공격 표면을 파악합니다.
2. 추상 구문 트리 (Abstract Syntax Tree, AST): RTL 코드의 구조적, 위상적 정보 (신호 연결, 상태 전이, 제어 흐름) 를 제공하여 LLM 이 논리적 흐름을 정확히 이해하도록 돕습니다.
3. RTL 요약 (RTL Summary): LLM 이 생성한 보안 중심의 코드 요약으로, 설계 문서에 명시되지 않은 민감한 레지스터나 코드 수준의 뉘앙스를 파악합니다.

이러한 컨텍스트를 바탕으로 LLM 은 각 CWE 에 대응하는 구체적인 SVA 속성과 JasperGold 실행 스크립트를 자동 생성하며, 이를 통해 설계의 결함을 증명하거나 반례 (Counterexample) 를 찾습니다.

3. 주요 기여 (Key Contributions)

• 최초의 표준화된 위협 모델 템플릿: SoC 보안 검증을 위한 체계적이고 일관된 위협 모델링 템플릿을 제안하고, 이를 기반으로 자동화된 TMDB 를 구축했습니다.
• 지식 기반 자동화 프레임워크: CWE, CVE, CAPEC 등 방대한 취약점 지식을 SoC 설계에 자동 매핑하여, 수동 위협 모델링에서 정형 검증까지의 전 과정을 자동화했습니다.
• 다중 컨텍스트 통합 접근법: 설계 문서, AST, RTL 요약이라는 세 가지 소스를 결합하여 LLM 이 설계 의도를 정확히 이해하고 오류 없는 보안 속성을 생성하도록 유도했습니다.
• End-to-End 자동화: 자산 식별 $\rightarrow$ 위협 매핑 $\rightarrow$ 속성 생성 $\rightarrow$ 정형 증명까지의 전체 파이프라인을 구현했습니다.

4. 실험 결과 (Results)

ATLAS 는 HACK@DAC 벤치마크 (2018, 2019, 2021 년 버전 포함) 에 있는 3 개의 산업 규모 RISC-V 기반 SoC 설계 (OpenTitan 등) 에 대해 평가되었습니다.

• 취약점 탐지율: 총 48 개의 알려진 취약점 (CWE) 중 39 개 (81.25%) 를 성공적으로 탐지했습니다.
• 정확한 속성 생성: 탐지된 39 개 중 33 개 (82% 이상) 에서 올바른 보안 속성 (Property) 을 생성하여 JasperGold 를 통해 취약점을 정형적으로 증명하거나 반례를 도출했습니다.
• Ablation Study (성분 제거 실험):
  • TMDB(위협 모델 데이터베이스) 를 제거할 경우 LLM 만으로는 취약점 탐지율이 30% 미만으로 급감했습니다.
  • 3 가지 컨텍스트 (DD, AST, RTL Summ) 를 모두 사용할 때 가장 높은 정확도를 보였으며, 단일 컨텍스트만 사용할 때보다 약 2.3 배 ~3 배 더 많은 정확한 속성을 생성했습니다.
• 성공 사례: 잘 문서화된 블록 (예: aes_192, rsa_wrapper) 에서 높은 성공률을 보였으며, 설계 의도가 명확하지 않은 경우에도 유용한 경고 신호를 생성했습니다.

5. 의의 및 결론 (Significance)

• Secure-by-Design 패러다임 실현: 사후 수정이 아닌 설계 단계에서 자동화된 위협 모델링과 정형 검증을 통해 SoC 보안을 강화하는 'Secure-by-Design' 접근법을 실현 가능한 수준으로 끌어올렸습니다.
• 전문성 장벽 해소: 깊은 도메인 지식이 없어도 표준화된 템플릿과 LLM 을 통해 체계적인 보안 검증이 가능해졌습니다.
• 확장성: 새로운 취약점이나 SoC 설계가 등장할 때마다 TMDB 를 업데이트하고 컨텍스트를 적용함으로써, 진화하는 위협 환경에 유연하게 대응할 수 있는 확장 가능한 프레임워크를 제시했습니다.

결론적으로 ATLAS 는 SoC 보안 검증의 자동화 수준을 획기적으로 높였으며, 인공지능과 정형 검증을 결합하여 하드웨어 보안의 새로운 표준을 제시하는 중요한 연구로 평가됩니다.