该论文聚焦于Linux内核扩展程序eBPF的安全迁移问题。eBPF程序被广泛用于网络、可观测性及安全策略执行，但其内核验证器仅检查低级内存安全和终止性，未强制许多高级源级属性，如初始化规则、schema一致性或错误处理。作者识别出六类源级bug，这些bug能够通过编译和内核验证，但会导致数据静默损坏、将先前跟踪的事件泄露至用户空间，或产生错误的执行结果。其中，作者发现了十款开源eBPF程序中此前未报道的信息泄露：这些程序中的环形缓冲区或栈驻留事件记录会将完全可解码的先前跟踪事件（包括用户标识路径和足以恢复每个事件KASLR偏移的内核返回地址）泄露到用户空间。为加固这些被验证器接受的缺陷程序并支持安全迁移，作者提出了Heimdall——一个自动化流水线，利用大语言模型（LLM）将遗留的libbpf C程序翻译为基于Aya Rust的eBPF程序。Heimdall迭代修复编译和内核验证失败，通过静态分析安全引擎拒绝Rust-Aya中不安全的逃逸机制，并借助符号执行和Z3等价性检查逐程序证明翻译后程序与原始程序行为等价。在102个eBPF程序上的实验表明，Heimdall成功生成了96个经形式化验证等价（94.1%）的翻译版本。Heimdall是首个能够自动化地将生产级eBPF程序迁移到内存安全语言，并为每个翻译程序提供形式化保证保持可观测行为的系统。

在基于格的密码学中，多项式乘法是核心运算。数论变换（NTT）能够实现快速乘法，但其系数域模数有严格限制。Hafiz等人（2025）通过引入不完全NTT（incomplete NTT）解决了这一局限，该方案将截断NTT与传统乘法方法结合。本文针对不完全NTT框架下的Toom-4乘法进行了深入研究。尽管Toom-4在渐近复杂度上优于Karatsuba乘法，但其精确成本尚未以与不完全NTT兼容的形式表达。为此，作者给出了Toom-4的具体实现，并推导了显式的运算计数，将系数域上的加法/减法与乘法分开统计。基于加法链的分析，提出了一个简洁的不完全NTT成本模型。利用该模型，分析了结合Toom-4、Karatsuba和不完全NTT的混合策略，确定了Toom-4具有优势的参数范围，并通过实验验证了预测行为的正确性。该工作为格密码实现中乘法方法的选择提供了理论依据，有助于优化性能。

本文介绍了 Zorya 符号执行框架的扩展，使其能够处理由 Go 标准 gc 编译器生成的多线程二进制文件。Zorya 框架最初仅支持单线程 TinyGo 二进制，通过将二进制提升到 Ghidra 的 P-Code 中间表示，并利用 Z3 SMT 求解器对具体值和符号值进行推理来检测漏洞。为了支持 gc 编译的二进制，作者解决了三个关键挑战：从 gdb 转储恢复操作系统线程状态以处理多线程；中和运行时抢占机制避免执行干扰；引入写时复制（copy-on-write）覆盖路径分析，用于检测未执行分支上的静默漏洞（如整数溢出）。研究在 11 个来自生产级 Go 项目（如 Kubernetes、Go-Ethereum 和 CoreDNS）的真实漏洞上进行了严格评估。结果表明，Zorya 成功检测出 7 个二进制级别漏洞，其中包括一个静默整数溢出——其他评估工具在没有手动编写预言（oracle）的情况下无法发现。该工作显著扩展了 concolic 测试在 Go 生态系统的实用性，为自动化安全分析提供了新手段。适合安全研究人员、Go 开发者和二进制分析工具开发者阅读。