技术摘要：Heimdall

问题陈述

扩展伯克利数据包过滤器（eBPF）程序对于 Linux 内核在网络、可观测性和安全领域的扩展至关重要。虽然内核内置的 eBPF 验证器强制执行底层内存安全和终止性，但它无法强制执行更高层级的源码级属性，如初始化纪律、模式一致性和错误处理。作者记录了六类源码级漏洞，这些漏洞能够编译并通过内核验证器，但可能导致静默数据损坏、敏感信息泄露或产生错误的执行结果。

已识别的关键漏洞包括：

• 未初始化状态：程序发出驻留在栈上的结构体而未进行零初始化，会泄露每 CPU 栈残留数据，包括足以恢复内核地址空间布局随机化（KASLR）偏移量的内核指针和返回地址。
• 未检查的辅助函数返回值：失败的辅助函数（例如 bpf_probe_read_user_str）常被忽略，导致发出陈旧的栈数据而非截断的字符串。
• 缓冲区/大小不匹配：开发者向输出辅助函数传递错误的大小，可能导致泄露包含内核指针的相邻私有字段。
• 钩子/上下文不匹配：在 XDP 钩子中使用错误的上下文结构体（例如 __sk_buff）会导致数据被错误解读。
• 映射类型/模式混淆：声明的映射值大小与实际数据不匹配，或将映射查找结果重新解释为无关类型。
• 有符号/无符号混淆：将有符号辅助函数返回值（指示错误）存储到无符号字段中，会生成虚假的大正数值，这些数值被用作映射键。

此外，eBPF 验证器本身存在已知漏洞（例如，不健全的剪枝、缺失的契约验证），这些漏洞可能被利用。迁移到像 Rust 这样的内存安全语言可以填补这些漏洞，但在大规模上进行手动重写是不切实际的，而现有的自动化工具缺乏确保语义等价性或 eBPF 上下文安全性的严谨性。

方法论：Heimdall 流水线

Heimdall 是一个自动化流水线，可将遗留的 libbpf C 程序翻译为惯用的、安全的 Aya Rust 程序。它采用结合大语言模型（LLM）、静态分析和形式化验证的五阶段迭代过程：

1. LLM 翻译：LLM 利用 Aya API 映射、钩子宏和可用示例，将 C 源代码翻译为 Rust。
2. 编译与内核验证：生成的 Rust 代码被编译为 eBPF 字节码。编译器 lint 防护（例如拒绝未使用的 unsafe 块）和内核验证器检查基本安全性和正确性。错误被反馈给 LLM 进行修复。
3. 安全检查（静态分析）：自定义静态分析引擎扫描 Rust 源代码，查找编译器和验证器可能遗漏的不安全逃逸机制。这包括禁止无类型的环形缓冲区预留、强制执行零初始化，并要求显式处理辅助函数返回值的 Result 类型。
4. 符号执行：原始 C 二进制文件和编译后的 Rust 二进制文件均被加载到自定义的 angr eBPF 后端中。该后端对 eBPF 辅助函数、映射、重定位和原子操作进行建模。它执行符号执行以探索所有可行路径，生成关于返回值和映射副作用的结构化公式。
5. 等价性检查：基于 Z3 的求解器检查 C 和 Rust 程序是否在语义上等价。作者引入了条件语义等价性，即仅要求在满足声明的安全条件（例如辅助函数调用成功）的输入上实现等价。这使得更安全的 Rust 翻译（在错误处理或内存零填充方面表现不同）在触发漏洞的路径上被视为与有缺陷的 C 源代码等价，同时仍能验证在有效路径上逻辑是否得以保留。如果找到反例，则将其反馈给 LLM 进行针对性修复。

为了支持这一过程，作者构建了完整的 angr eBPF 后端，包括 ELF 加载器、架构定义、VEX IR 提升器和辅助函数存根。他们还开发了自定义的ITE 链编码，以在符号键下建模映射副作用，捕捉“最后写入获胜”的语义。

主要贡献

• Heimdall 流水线：首个将生产级 eBPF 程序从 C 自动翻译为 Rust 的系统，并为每个程序提供可观察行为保留的形式化保证。
• 条件等价性：一种新颖的验证方法，通过将等价性检查限制在安全执行路径上，来验证在触发漏洞的路径上行为不同的安全性提升型翻译。
• eBPF 符号执行后端：一个完整的 angr eBPF 后端，对内核辅助函数、映射和 BPF 到 BPF 调用进行建模，支持在字节码级别进行形式化推理。
• Safe-Aya 静态分析器：一个策略引擎，拒绝通过内核验证器但属于不安全 Rust 模式的代码（例如无类型的环形缓冲区、被忽略的辅助函数错误）。
• 安全发现：在十个开源 eBPF 程序中发现了此前未报告的信息泄露，包括通过栈残留恢复 KASLR 以及环形缓冲区中的跨事件内容泄露。
• 基准测试与评估：包含 102 个 eBPF 程序的公开基准测试，以及对翻译流水线的全面评估。

结果

该系统在来自不同来源（libbpf-tools、libbpf-bootstrap、KEN、Suricata 等）的 102 个真实世界 eBPF 程序上进行了评估。

• 成功率：Heimdall 生成了 96 个经过形式化验证等价的翻译（94.1%）。其余六个要么部分验证（由于符号执行限制），要么超出了求解器的可扩展性限制。
• 漏洞修复：在 96 个经过验证的翻译中，Heimdall 修复了 100% 观察到的未初始化状态、未检查辅助函数返回值和有符号/无符号混淆实例。
• 与基线对比：与没有 Heimdall 流水线的基线 LLM 代理相比，Heimdall（智能体）实现了 98% 的三次通过率（编译、内核验证、安全检查、等价性），而基线仅为 4–12%。
• 运行时开销：对 10 个程序的运行时验证显示，Rust 翻译通常产生适度的开销（几何平均值相对于 C 从 0.44 倍到 3.60 倍不等），大多数落在 1.14 倍到 1.89 倍之间。
• 安全性：翻译消除了导致已识别漏洞的特定不安全模式（未初始化内存、未检查的错误）。

意义

该论文声称 Heimdall 是首个系统，能够自动化生产级 eBPF 程序向内存安全的迁移，并提供每个程序的形式化保证，确保迁移保留了可观察行为。它解决了内核验证器的底层保证与现代 eBPF 应用高层安全需求之间的差距。通过将 LLM 与形式化验证和静态分析相结合，Heimdall 证明了自动翻译可以生成不仅在语法上正确，而且在语义上等价且不存在内核验证器无法检测的特定类源码级安全漏洞的代码。这项工作为 eBPF 迁移确立了新的基准，并为构建更健壮、内存安全的内核扩展奠定了基础。