Model2Kernel: Model-Aware Symbolic Execution For Safe CUDA Kernels

TL;DR

Model2Kernel is a novel system that uses model-aware dynamic analysis and symbolic execution to automatically detect memory-safety bugs in CUDA kernels used for large language model inference, improving reliability and security.

Contribution

It introduces the first practical, model-aware symbolic execution framework tailored for CUDA kernels in LLM inference, addressing limitations of prior methods.

Findings

Discovered 353 previously unknown bugs in CUDA kernels.

Achieved only nine false positives in bug detection.

Effectively verified memory safety in real-world LLM inference systems.

Abstract

The widespread adoption of large language models (LLMs) has made GPU-accelerated inference a critical part of modern computing infrastructure. Production inference systems rely on CUDA kernels to implement core transformer operations, yet these kernels are highly susceptible to memory-safety bugs due to model-dependent tensor layouts, intricate memory indexing, and massive thread-level parallelism. Such bugs can corrupt model weights, crash inference services, or even enable adversarial attacks. Existing techniques either depend on unavailable hardware, incur high overhead, or fail to handle kernel inputs with variable lengths, and none can effectively detect CUDA memory bugs in LLM inference systems. This paper presents Model2Kernel, the first practical system for automatically verifying the memory safety of CUDA kernels used in LLM inference. Model2Kernel performs model-aware dynamic analysis to determine how each model invokes kernels and to classify kernel arguments as either fixed by the model architecture or controlled by model users. Using this information, Model2Kernel then applies CUDA-specialized symbolic execution, supported by new abstractions for dynamic tensor memory and thread identifiers, to accurately pinpoint memory bugs in kernels. In the evaluation on CUDA kernels and models from vLLM, Hugging Face, and recent LLM research papers, Model2Kernel discovers 353 previously unknown bugs while producing only nine false positives, demonstrating its effectiveness.