Each language version is independently generated for its own context, not a direct translation.

这篇论文介绍了一个名为 Model2Kernel 的新系统，它的任务是自动检查大语言模型（LLM）在 GPU 上运行的“核心代码”是否安全。

为了让你更容易理解，我们可以把整个大模型推理过程想象成一家超级繁忙的“智能餐厅”。

1. 背景：餐厅里的“隐形危机”

大模型（LLM）：就像餐厅里那位才华横溢的主厨。他负责处理复杂的订单（比如写诗、写代码），但他自己不下厨，只负责指挥。
CUDA 内核（Kernels）：这是餐厅里真正切菜、炒菜、摆盘的“流水线工人”。主厨的指令最终都要变成这些工人的具体动作。这些工人是在 GPU（显卡）这个超级厨房里工作的。
问题所在：
- 现在的餐厅（大模型系统）越来越复杂，菜单（模型架构）千变万化，订单量（输入长度）也忽大忽小。
- 这些“流水线工人”（CUDA 代码）非常忙碌，成千上万个工人同时干活。
- 因为太忙太复杂，工人很容易犯错：
  - 越界访问：工人伸手去拿第 100 个盘子，但架子上只有 50 个，结果把架子弄坏了（内存越界）。
  - 数数溢出：工人手里拿着计数器，数到 20 亿时，计数器坏了，显示成 0，导致他以为还没开始干活，结果把菜倒进了错误的锅里（整数溢出）。
- 后果：轻则餐厅系统崩溃（服务中断），重则坏人可以偷偷修改主厨的秘方（篡改模型权重），甚至控制整个厨房（代码执行攻击）。

2. 现有的工具为什么不管用？

以前，人们检查这些工人有没有犯错，主要靠两种方法：

实时监控（动态检测）：派一个保安盯着每个工人。但这太慢了，餐厅会因此排队排到大街上（性能开销太大），而且保安需要特殊的装备（硬件支持），很多餐厅买不起。
静态代码审查（静态分析）：让一个专家在开工前看图纸。但问题是，餐厅的菜单（模型）和订单量（输入）是动态变化的，图纸上画的是“假设”，而实际干活时情况千变万化。专家看不懂这种“如果订单是 1 万单怎么办”的复杂情况，所以经常漏掉问题。

3. Model2Kernel 是怎么工作的？（核心创新）

Model2Kernel 就像是一个拥有“读心术”和“超级模拟能力”的 AI 质检员。它由两个聪明的助手组成：

助手 A：HFProbe（“餐厅观察员”）

任务：它不直接去厨房，而是先观察主厨（模型）是怎么指挥工人的。
做法：它会在没有真实 GPU 的情况下，“模拟”运行主厨的指令。它会搞清楚：
- 哪些参数是固定的？（比如：主厨规定切菜必须切 8 厘米，这是死规矩，不能变。）
- 哪些参数是用户控制的？（比如：今天来了多少客人，点了多少菜，这是可以变的。）
比喻：它就像是一个懂行的大堂经理，告诉质检员：“别瞎猜了，这个盘子的大小是固定的，但那个菜的数量可能是 1 个也可能是 100 万个，你重点检查那个。”

助手 B：cuKLEE（“超级模拟工”）

任务：拿着大堂经理提供的信息，在虚拟世界里让成千上万个“虚拟工人”同时干活，看看会不会出错。
做法：
- 符号化执行：它不把数字当成具体的"5"或"100"，而是当成一个变量（比如 $X$ ）。它会思考：“如果 $X$ 是 1000 万，工人会怎么做？如果 $X$ 是 20 亿，工人会怎么做？”
- 特殊抽象：它把每个食材（Tensor）想象成独立的、互不干扰的储物柜。这样它就能轻松判断工人是不是伸手去拿了别人的柜子（内存越界）。
- 多线程模拟：它能一次性模拟所有工人的动作，而不是一个个去试，效率极高。
比喻：它就像是一个能同时模拟一亿种可能性的“平行宇宙模拟器”。它能瞬间发现：“哦！如果客人点了 12 万道菜，工人的计数器就会爆炸，导致他把菜倒进垃圾桶里！”

4. 成果如何？

战绩辉煌：研究人员用这个系统检查了 vLLM（一个流行的餐厅管理系统）、Hugging Face（最大的菜谱库）以及最新的科研论文中的代码。
发现漏洞：他们发现了 353 个以前没人知道的严重漏洞（主要是数数溢出和拿错盘子）。
误报很少：在这么多检查中，只有 9 次是“虚惊一场”（误报），准确率非常高。
对比优势：如果把 Model2Kernel 和以前的老工具比，老工具只能抓到 5-15 个漏洞，而 Model2Kernel 能抓到 15 个（在已知漏洞测试中），而且能发现大量新漏洞。

5. 总结

Model2Kernel 就像是给大模型餐厅配备了一套全自动的、懂行情的、能预知未来的安检系统。

它不需要昂贵的特殊硬件。
它能理解复杂的菜单变化。
它能提前发现那些只有在“超级大单”来临时才会爆发的隐患。

这项技术让大模型在大规模商用时更加安全、稳定，防止了因为代码小错误导致的系统崩溃或被黑客攻击的风险。对于普通用户来说，这意味着你以后用 AI 聊天、写代码时，背后的系统会更可靠，不容易“翻车”。

Each language version is independently generated for its own context, not a direct translation.

Model2Kernel：面向大语言模型推理的 CUDA 内核内存安全符号执行系统

1. 研究背景与问题定义

随着大语言模型（LLM）的广泛应用，GPU 加速的推理已成为现代计算基础设施的核心。生产级的推理系统（如 vLLM、Hugging Face Transformers）依赖 CUDA 内核 来实现 Transformer 架构中的核心张量操作。然而，这些内核极易受到内存安全漏洞（如缓冲区溢出、整数溢出、数据竞争）的威胁。

主要挑战包括：

模型依赖的张量布局：内核行为高度依赖于模型架构（如隐藏层大小、层数）和用户输入的序列长度，导致张量形状在运行时动态变化。
复杂的内存索引：细粒度的索引计算和数千个线程的并行执行增加了越界访问和数据竞争的风险。
现有技术的局限性：
- 动态检测工具（如 Compute Sanitizer）：运行开销大，或依赖尚未普及的硬件支持。
- 静态分析工具：难以处理运行时确定的缓冲区大小和可变的内核启动配置。
- 通用符号执行：难以处理动态数组和大规模线程并行，且无法自动推断模型架构对内核参数的约束。

目前缺乏一种能够自动、高效且准确地检测 LLM 推理系统中 CUDA 内存漏洞的实用化方案。

2. 方法论：Model2Kernel 系统架构

Model2Kernel 是一个全自动化的分析框架，旨在验证给定 LLM 模型在使用特定 CUDA 内核时是否存在内存安全问题。该系统由两个核心组件组成：HFProbe（动态模型分析器）和 cuKLEE（专用符号执行引擎）。

2.1 HFProbe：模型感知的动态分析器

HFProbe 的目标是理解模型如何调用 CUDA 内核，并区分哪些内核参数是由模型架构固定的，哪些是由用户控制的。

静态调用图构建：基于 Hugging Face 模型的 Python 代码（AST），构建静态调用图，识别所有可能被调用的 CUDA 内核。
无硬件动态剖析：修改 vLLM 和 Transformers 框架，使用“伪造（Fake）”的 CUDA 内核替代真实 GPU 计算。这使得系统无需 GPU 硬件即可运行模型，并记录内核调用时的张量形状、数据类型及参数值。
配置变异（Configuration Mutation）：利用 LLM（如 GPT-5）自动修改模型的 config.json 和框架启动参数，以触发更多未被默认配置覆盖的 CUDA 内核，确保分析的全面性。
上下文生成：收集运行数据，推断出张量维度与批大小（Batch Size）、序列长度（Sequence Length）之间的线性关系、不变量及边界约束，为符号执行提供精确的输入约束。

2.2 cuKLEE：面向 CUDA 的符号执行引擎

cuKLEE 基于 KLEE 构建，针对 CUDA 内核的特性进行了深度定制，专门用于检测缓冲区溢出、整数溢出、数据竞争和空指针解引用。

动态张量内存模型：
- 将每个张量建模为离散且分离的内存区域，而非连续内存。
- 为每个张量引入符号约束变量（如基地址 $B_t$ 、元素数量 $N_t$ 、维度 $d_i$ 等）。
- 通过抽象张量方法（如 numel(), size()），将张量操作转化为对符号变量的约束，从而高效处理动态形状的张量。
线程感知的符号执行：
- 将 CUDA 线程标识符（blockIdx, threadIdx）建模为符号变量，而非枚举具体值。
- 通过单遍符号执行捕获所有线程的行为，利用约束求解器检查线程间的数据竞争（通过引入第二组线程 ID 变量并检查冲突写操作）。
约束求解与漏洞检测：
- 结合 HFProbe 提供的模型架构约束（如隐藏层大小固定）和用户输入约束（如序列长度可变）。
- 检测整数运算溢出、指针越界访问以及空指针解引用。

3. 关键贡献

cuKLEE 引擎：首个支持动态形状张量和大规模线程并行的 CUDA 专用符号执行引擎。它通过离散内存建模和线程 ID 符号化，解决了传统符号执行在处理 LLM 推理场景时的扩展性难题。
HFProbe 分析器：一种无需 GPU 硬件即可分析模型调用行为并推断内核参数约束的动态剖析工具。它通过配置变异技术，显著提高了内核覆盖率和分析深度。
Model2Kernel 框架：将上述两者结合，实现了 LLM 推理系统中 CUDA 内存漏洞的自动化检测。
实证研究：在 vLLM、Hugging Face 及最新研究论文中的模型和内核上进行了大规模评估，发现了大量未知漏洞。

4. 实验结果

研究团队在三个来源的 120 个模型和 173 个 CUDA 内核上进行了评估（包括 vLLM 0.9.0、Hugging Face 自定义内核模型及 4 篇顶会论文代码）。

漏洞发现：
- 共发现 353 个以前未知的内存安全漏洞。
- 其中包括 328 个整数溢出（Integer Overflows）和 25 个越界访问（Out-of-Bounds Accesses）。
- 未发现数据竞争或空指针解引用（受限于测试集特性）。
准确性：
- 误报率极低，仅 9 个误报（False Positives），误报率约为 2.49%。
- 误报主要源于 HFProbe 无法跨内核追踪张量值、未加载真实权重导致的索引推断偏差，以及 vLLM 内部约束未被完全建模。
对比基线：
- 在 20 个已知的 vLLM 漏洞上，Model2Kernel 成功检测出 15 个。
- 相比之下，现有工具（Honeycomb, GKLEE, ESBMC-GPU）仅能检测出 0-5 个，主要受限于对动态内存、现代 C++ 特性及大规模线程并行的支持不足。
成本：
- 总分析耗时约 986 小时（并行执行），LLM 调用成本约 442 美元。考虑到代码库规模（Python 和 CUDA 代码超 10 万行），该成本被认为是可接受的。

5. 意义与影响

安全性提升：LLM 推理系统中的内存漏洞可能导致模型权重被篡改、服务崩溃，甚至被攻击者利用进行任意代码执行。Model2Kernel 为构建更安全的推理基础设施提供了关键工具。
开发范式转变：证明了将模型架构感知（Model-Aware）与符号执行相结合是解决复杂 GPU 程序验证问题的有效途径。
社区贡献：发现的数百个漏洞已被提交给相关项目（如 vLLM），有助于修复现有系统并防止未来类似问题的发生。
未来方向：该框架的核心思想（如配置变异、离散内存建模）可推广至 NPU 内核及其他类型的 GPU 漏洞检测。

总结：Model2Kernel 填补了 LLM 推理系统内存安全检测的空白，通过创新的“模型 - 内核”联合分析策略，实现了对大规模、动态 CUDA 内核的高效、精准漏洞挖掘，对保障 AI 基础设施的安全性具有重要意义。

Model2Kernel: Model-Aware Symbolic Execution For Safe CUDA Kernels