eBPF 是一种在内核中安全运行沙盒程序的技术，广泛应用于网络、可观测性和安全等领域。其安全性依赖于内核内部的编译管道：验证器检查每个程序，内核即时编译器（JIT）将验证后的字节码翻译为本地代码。为保持可信性，内核 JIT 设计得尽可能简单，采用单遍扫描逐条翻译字节码指令。但这种单遍设计严重限制了优化空间，导致 eBPF 程序的运行速度比原生编译代码慢最多 2 倍。传统的优化方案——直接修改内核 JIT——需要上游社区接受、经历漫长的发布周期，同时会扩大可信计算基（TCB）并增加每体系结构的代码量。为此，本文提出了 Kops，一种扩展接口，允许用户空间编译器和内核模块在不修改内核核心的前提下引入新操作，同时维持最小的 TCB。每个操作有两种形式：一段由普通 eBPF 指令组成的证明序列（由现有验证器检查），以及本地机器指令的 native emit（由 JIT 编译）。由于验证器已检查证明序列，native emit 是每个操作唯一新增的 TCB 部分。硬件惯用操作是此接口最直接的受益者。利用 Kops，作者构建了 EInsn，包含旋转、条件选择等七个单条 CPU 指令即可完成的操作。Lean 4 形式化验证表明每个 native emit 的计算结果与证明序列一致。在 x86-64 和 ARM64 上，EInsn 使 eBPF 微基准测试的性能提升最高 24%，生产应用提升最高 12%。同一接口还支持全程序原生替换，以增加 TCB 为代价可达到 2.358 倍加速。该论文适合操作系统、编译器、安全领域的工程师和研究者阅读。