Model2Kernel: Model-Aware Symbolic Execution For Safe CUDA Kernels

이 논문은 LLM 추론에 사용되는 CUDA 커널의 메모리 안전성을 자동으로 검증하는 첫 번째 실용적 시스템인 Model2Kernel 을 제안하며, 모델 인식 동적 분석과 심볼릭 실행을 통해 353 개의 새로운 버그를 발견하고 낮은 오검출률을 입증했습니다.

핵심

🏛️ 배경: 거대한 AI 도서관과 정교한 기계

현대 사회에서 AI(예: 챗봇, 검색 엔진) 는 거대한 도서관처럼 작동합니다.

1. 도서관장 (LLM 모델): 책 (지식) 을 정리하고 답변을 준비하는 역할입니다.
2. 작업반 (CUDA 커널): 도서관장이 지시한 대로 실제로 책장을 넘기고, 책을 꺼내고, 내용을 계산하는 수천 명의 일꾼들이 모여 있는 작업반입니다. 이 일꾼들은 GPU(그래픽 카드) 라는 초고속 기계 위에서 동시에 일을 합니다.

문제점:
이 일꾼들은 매우 빠르지만, 매우 까다로운 규칙을 따릅니다.

• "책장 번호가 1000 번을 넘으면 안 돼."
• "동료의 책장을 건드리면 안 돼."
• "계산할 때 숫자가 너무 커지면 터져버려."

하지만 최근 AI 모델이 너무 커지고 복잡해지면서, 이 일꾼들이 **실수 (버그)**를 할 확률이 급격히 높아졌습니다. 한 명이라도 실수하면 전체 도서관이 멈추거나, 심지어 해커가 도서관의 비밀 문서를 훔쳐갈 수도 있습니다.

---

🕵️‍♂️ 해결사: Model2Kernel (모델을 아는 탐정)

기존의 보안 도구들은 두 가지 큰 문제가 있었습니다.

1. 너무 느리거나 비쌌음: 모든 일을 직접 눈으로 확인하려다 보니 시간이 너무 오래 걸렸습니다.
2. 상황을 몰랐음: 도서관장 (모델) 이 어떤 책을 언제 꺼내는지 모르고, 일꾼들에게 "가상"의 지시만 내렸기 때문에 실제 상황과 다른 오류를 많이 찾아냈습니다.

이때 등장한 Model2Kernel은 **"도서관장의 성격을 완벽히 이해하는 탐정"**입니다.

1. HFProbe: 도서관장의 행적 추적기 (가상 시뮬레이션)

이 도구의 첫 번째 구성 요소인 HFProbe는 실제 GPU(고성능 컴퓨터) 없이도 AI 모델을 '가상'으로 실행합니다.

• 비유: 도서관장이 "오늘은 1000 권의 책을 정리해"라고 하면, HFProbe 는 "아, 오늘 1000 권이구나. 그럼 일꾼들에게 1000 권에 맞는 지시를 내려야겠다"라고 미리 파악합니다.
• 핵심: AI 모델이 어떤 상황에서 어떤 지시를 내리는지, 그리고 그 지시가 일꾼들에게 어떻게 전달되는지 정확한 맥락을 파악합니다.

2. cuKLEE: 초능력을 가진 일꾼 감시관 (상징적 실행)

두 번째 구성 요소인 cuKLEE는 이 파악된 정보를 바탕으로 일꾼들의 작업을 가상 시뮬레이션으로 검증합니다.

• 비유: 보통은 "책장 1 번부터 100 번까지 확인해"라고 지시하지만, cuKLEE 는 **"만약 책장이 10000 번까지 있다면? 만약 책장 번호가 음수가 되면?"**처럼 **모든 가능한 상황 (상징적 입력)**을 한 번에 상상하며 검증합니다.
• 핵심: 실제 일을 시키지 않아도, "만약에 이런 일이 생기면?"이라는 시나리오를 수천 가지 만들어서, 어디서든 실수가 날 수 있는지 미리 찾아냅니다.

---

🚀 Model2Kernel 의 활약상

이 탐정 팀이 실제로 vLLM(인기 있는 AI 프레임워크) 과 Hugging Face(수백만 개의 AI 모델이 있는 곳) 에서 일어난 일을 분석한 결과 놀라운 성과를 거두었습니다.

• 353 개의 숨겨진 버그 발견: 기존에는 전혀 몰랐던 치명적인 오류 353 가지를 찾아냈습니다.
  • 정수 오버플로우: "1000 권을 정리해"라고 했는데, 숫자가 너무 커져서 컴퓨터가 "음수"로 잘못 계산하는 경우.
  • 배터리 오버플로우: "100 번 책장까지 가"라고 했는데, 101 번 책장까지 넘어가서 다른 사람의 책장을 건드리는 경우.
• 거의 오보 없음: 353 개 중 9 개만 오보 (실수가 아닌 것을 실수라고 한 경우) 였습니다. 이는 매우 높은 정확도입니다.
• 기존 도구와의 비교: 다른 보안 도구들은 20 개의 알려진 버그 중 15 개만 찾았지만, Model2Kernel 은 15 개를 모두 찾아냈을 뿐만 아니라 훨씬 더 많은 새로운 버그를 찾아냈습니다.

---

💡 왜 이것이 중요한가요?

AI 가 우리 삶에 깊숙이 들어오면서, AI 시스템이 멈추거나 해킹당하는 것은 큰 재앙이 될 수 있습니다.

• Model2Kernel은 AI 시스템이 **실제 사용 환경 (긴 대화, 복잡한 질문)**에서도 안전하게 작동할 수 있도록 미리 예방 주사를 맞는 것과 같습니다.
• 이 도구는 AI 개발자들이 "우리가 만든 프로그램이 안전한가?"를 걱정하지 않고, 더 좋은 AI 를 만들 수 있게 도와줍니다.

📝 한 줄 요약

"Model2Kernel 은 AI 가 작동하는 복잡한 기계실 (GPU) 에서, 도서관장의 지시를 완벽히 이해한 채 모든 상황을 미리 시뮬레이션하여 치명적인 실수 (버그) 를 찾아내는 초강력 보안 시스템입니다."

기술 요약

1. 문제 정의 (Problem)

대형 언어 모델 (LLM) 의 광범위한 채택으로 인해 GPU 가속 추론은 현대 컴퓨팅 인프라의 핵심이 되었습니다. 그러나 이러한 추론 시스템은 CUDA 커널을 사용하여 핵심 트랜스포머 연산을 구현하는데, 이 커널들은 다음과 같은 이유로 메모리 안전성 버그에 매우 취약합니다.

• 모델 의존적 텐서 레이아웃: 모델 아키텍처에 따라 텐서의 모양 (shape) 이 달라지며, 이는 커널 입력의 크기를 결정합니다.
• 복잡한 메모리 인덱싱: 대규모 텐서와 수천 개의 병렬 스레드 간의 미세한 인덱스 계산은 경계 초과 (out-of-bounds) 접근 및 데이터 레이스를 유발하기 쉽습니다.
• 정수 오버플로우: 모델이 커지고 시퀀스 길이가 길어지면서 (예: 100 만 토큰), 인덱스 계산 시 32 비트 정수 오버플로우가 발생하기 쉽습니다.
• 심각한 결과: 이러한 버그는 모델 가중치 손상, 추론 서비스 중단, 그리고 악의적인 공격 (임의 메모리 쓰기, 코드 실행) 으로 이어질 수 있습니다.

기존 기술의 한계:

• 동적 분석 (Dynamic Analysis): GPU 메모리 버퍼의 메타데이터를 추적하지만, 높은 런타임 오버헤드가 발생하거나 아직 보편화되지 않은 특수 하드웨어에 의존합니다.
• 정적 분석 (Static Analysis): 런타임에 결정되는 버퍼 크기나 다양한 커널 실행 구성을 처리하지 못해 실제 LLM 추론 시스템의 커널에는 적용이 어렵습니다.

2. 방법론 (Methodology)

저자들은 Model2Kernel이라는 자동화된 분석 프레임워크를 제안했습니다. 이는 LLM 추론 시스템에서 사용되는 CUDA 커널의 메모리 안전성을 검증하는 최초의 실용적인 시스템입니다. Model2Kernel 은 두 가지 주요 구성 요소로 이루어져 있습니다.

A. HFProbe (모델 프로파일러)

• 역할: GPU 하드웨어 없이 모델을 "실행"하여 CUDA 커널이 어떻게 호출되는지 분석합니다.
• 기능:
  • 정적 분석: 모델의 Python 코드 (Hugging Face 포맷) 를 분석하여 호출 가능한 모든 CUDA 커널을 식별합니다.
  • 동적 프로파일링: 실제 구성을 사용하여 모델을 실행 (GPU 연산은 모킹) 하고, 커널 호출 시 텐서 모양과 인자 값을 기록합니다.
  • 구성 변형 (Mutation): LLM 에이전트를 활용하여 config.json 및 프레임워크 설정을 변형시켜 정적으로 식별되었으나 동적으로 트리거되지 않은 커널들을 추가로 실행합니다.
  • 출력: 커널 인자를 모델 아키텍처에 의해 고정된 값과 사용자가 제어하는 변수로 분류하여 cuKLEE 에 분석 컨텍스트를 제공합니다.

B. cuKLEE (CUDA 전용 심볼릭 실행 엔진)

• 역할: HFProbe 로부터 얻은 정보를 바탕으로 CUDA 커널의 메모리 버그를 탐지합니다.
• 핵심 기술:
  • 동적 텐서 메모리 추상화: 런타임에 결정되는 텐서 모양을 처리하기 위해, 각 텐서를 별도의 분리된 메모리 영역으로 모델링합니다. 텐서의 기저 주소, 요소 수, 차원 등을 심볼릭 변수로 표현하여 경계 검사 (bounds checking) 를 용이하게 합니다.
  • 스레드 식별자 심볼릭화: 수천 개의 병렬 스레드를 개별적으로 실행하는 대신, threadIdx, blockIdx 등을 심볼릭 변수로 처리하여 단일 실행 경로로 모든 스레드의 행동을 포착합니다. 이를 통해 데이터 레이스를 효율적으로 탐지합니다.
  • 텐서 메서드 요약: PyTorch 의 복잡한 텐서 메서드 (예: sum, view) 를 심볼릭 제약 조건으로 요약하여 분석 효율성을 높입니다.
  • 버그 탐지 유형: 버퍼 오버플로우, 정수 오버플로우, 데이터 레이스, NULL 포인터 역참조.

3. 주요 기여 (Key Contributions)

1. cuKLEE 개발: 동적 모양을 가진 텐서를 지원하고 수천 개의 CUDA 스레드를 확장 가능한 방식으로 처리하는 CUDA 특화 심볼릭 실행 엔진을 설계했습니다.
2. HFProbe 개발: 모델이 CUDA 커널을 호출하는 방식을 분석하고 모델 의존적 커널 인자를 추론하는 동적 모델 프로파일러를 개발했습니다.
3. Model2Kernel 통합 및 검증: 위 두 구성 요소를 통합하여 LLM 추론 시스템의 CUDA 메모리 버그를 자동으로 탐지하는 프레임워크를 구축하고, 광범위한 실험을 통해 그 유효성을 입증했습니다.

4. 실험 결과 (Results)

저자들은 vLLM, Hugging Face, 그리고 최근 연구 논문 (4 개) 에서 제공된 120 개의 모델과 173 개의 커널을 대상으로 실험을 수행했습니다.

• 버그 탐지: 총 353 개의 새로운 메모리 버그를 발견했습니다.
  • 정수 오버플로우 (Integer Overflows): 328 개
  • 경계 초과 접근 (Out-of-bounds Accesses): 25 개
  • (데이터 레이스와 NULL 포인터는 발견되지 않음)
• 정확도: 9 개의 거짓 양성 (False Positives) 만 발생하여 오검출률은 약 2.49% 로 매우 낮았습니다.
• 기존 기술 대비 성능: 알려진 20 개의 vLLM 버그를 대상으로 Honeycomb, GKLEE, ESBMC-GPU 와 비교한 결과, Model2Kernel 은 15 개를 성공적으로 탐지하여 기존 도구들보다 훨씬 높은 커버리지를 보였습니다.
• 성능: 분석에는 총 약 986 시간이 소요되었으나, 병렬 처리를 통해 효율적으로 수행되었습니다.

5. 의의 및 결론 (Significance)

• 실용성: Model2Kernel 은 실제 LLM 추론 시스템 (vLLM, Transformers 등) 에서 발생하는 메모리 안전성 문제를 자동으로 탐지할 수 있는 최초의 실용적인 도구입니다.
• 보안 강화: LLM 추론 시스템의 취약점을 사전에 발견하여 모델 가중치 조작이나 서비스 중단과 같은 심각한 보안 위협을 방지할 수 있습니다.
• 기술적 혁신: 심볼릭 실행의 한계였던 동적 배열 처리와 대규모 병렬 스레드 분석 문제를 해결하여, 복잡한 GPU 커널 분석의 새로운 기준을 제시했습니다.
• 향후 방향: Triton 커널이나 NPU 지원으로 확장 가능하며, 경로 탐색 전략을 CUDA 에 최적화하여 효율성을 더 높일 수 있는 잠재력을 가지고 있습니다.

이 논문은 LLM 생태계의 급속한 성장 속에서 GPU 기반 추론 시스템의 신뢰성과 보안을 확보하기 위한 필수적인 도구로서 Model2Kernel 의 가치를 입증했습니다.