Kops: Safely Extending the eBPF Compilation Pipeline with Native Operations

Kops is a secure extension interface that accelerates eBPF programs by allowing userspace compilers and kernel modules to introduce new native operations—verified via vanilla eBPF proof sequences—thereby achieving significant performance gains without expanding the kernel's trusted computing base.

The Gist

Imagine the operating system (the "brain" of your computer) has a very strict security guard. This guard, called the eBPF Verifier, checks every little program (like a traffic cop or a security scanner) before letting it run inside the kernel. The guard is incredibly careful: it only allows programs written in a very simple, safe language.

Once the guard says, "Okay, this is safe," a translator (the JIT Compiler) turns that simple language into the computer's native language so it can run fast.

The Problem: The "One-Word-at-a-Time" Translator

The paper explains that the current translator is designed to be super simple and trustworthy. It translates the safe program one instruction at a time, in a single pass. It doesn't look ahead or try to be clever.

Think of it like a translator who is forbidden from using idioms or shortcuts. If you want to say "rotate a number," the safe language doesn't have a single word for that. So, the translator has to write out a long, clunky sentence using ten different words to explain the same thing.

• Result: The computer has to read and execute a long, messy sentence instead of a single, powerful command. This makes eBPF programs run up to twice as slow as they could if they were written in the native language directly.

The Solution: Kops (The "Magic Passport")

The authors created a system called Kops. Think of Kops as a special "Magic Passport" system that lets the computer use powerful, native shortcuts without breaking the security guard's rules.

Here is how it works, using a simple analogy:

1. The Two-Part Passport: Every new "shortcut" (like a hardware rotation or a conditional selection) comes with two parts:

   • The Proof (The Safe Version): A long, boring, step-by-step explanation written in the safe language. The security guard checks this to make sure it's safe.
   • The Native Emit (The Magic Version): A single, powerful instruction that the computer's hardware actually executes.

2. The Process:

   • Before the program runs, a "Recognizer" (a smart tool outside the kernel) looks for patterns. If it sees a long, clunky sentence that matches a known shortcut, it swaps it out for the "Magic Passport."
   • The Security Guard still sees the long, boring "Proof" version. It checks that, says "Safe," and gives the green light.
   • The Translator then sees the "Magic Passport." Instead of translating the long sentence, it simply swaps it for the single, powerful native instruction.

3. The Safety Guarantee: The security guard never sees the "Magic" version. It only trusts the "Proof." The only new thing the system has to trust is the specific code that turns the "Proof" into the "Magic" instruction. The authors proved mathematically (using a tool called Lean 4) that the "Magic" instruction does exactly the same thing as the long "Proof" sentence.

What Did They Build? (EInsn)

Using Kops, they built a set of seven specific shortcuts called EInsn. These are things computers are really good at doing in one step (like rotating bits or picking between two values) but which the safe language usually forces to be done in many steps.

The Results

• Speed: By using these shortcuts, they made eBPF programs run 24% faster on some computers and 22% faster on others. In real-world applications (like network traffic management), they saw up to a 12% speed boost.
• Safety: They didn't have to change the security guard's rules or make the translator more complex. The "trusted" part of the system stayed tiny and safe.
• Flexibility: If a computer doesn't support a specific shortcut, the system just falls back to the long, safe version. It doesn't break.

The Big Picture

Imagine you are driving a car (the computer). The current rules say you must drive at 20 mph because the speedometer is broken and can only read in 5-mph increments. You can't go faster, even if the road is clear.

Kops is like a special license that says: "We know you are driving safely (the Proof), so we will let you use the car's actual speedometer (the Native Emit) to go faster, but only on specific, pre-approved roads."

They proved that this new way of driving is just as safe as the old way, but it gets you to your destination much quicker.

Technical Summary

Technical Summary: Kops – Safely Extending the eBPF Compilation Pipeline with Native Operations

1. Problem Statement

eBPF (Extended Berkeley Packet Filter) safely extends OS kernels for networking, observability, and security by employing a compilation pipeline where an in-kernel verifier checks programs for safety before a Just-In-Time (JIT) compiler translates them to native code. However, the kernel JIT is designed to be simple and trustworthy, translating bytecode instructions one at a time in a single pass. This "per-opcode" design prevents cross-instruction optimizations and fails to recognize hardware idioms (e.g., rotate, conditional select) that modern CPUs execute as single instructions.

Characterization in the paper reveals that eBPF programs run up to 1.98× slower on ARM64 and 1.57× slower on x86-64 compared to natively compiled code. The performance gap is primarily driven by the kernel JIT's inability to optimize multi-instruction sequences into efficient native patterns. Existing solutions are limited: adding optimizations directly to the kernel JIT is difficult due to long release cycles, the need for upstream acceptance, and the expansion of the Trusted Computing Base (TCB). Userspace optimizers (e.g., Merlin, K2) can rewrite bytecode but cannot emit native instructions outside the standard eBPF instruction set.

2. Methodology: The Kops Mechanism

The authors present Kops, an extension interface that allows userspace compilers and kernel modules to introduce new operations without modifying the kernel core. Kops operates on the principle of dual representation for each new operation:

1. Proof Sequence: A sequence of vanilla eBPF instructions that the existing in-kernel verifier checks. This ensures that safety guarantees (memory safety, termination) remain intact.
2. Native Emit: A direct emission of machine instructions by the JIT compiler.

Workflow:

• Recognition: A compile-time recognizer (in userspace) identifies patterns corresponding to supported operations (e.g., a specific sequence of shifts and ORs for a rotate) and rewrites them into "extended instructions."
• Verification: Upon loading, the verifier lowers the extended instruction back into its proof sequence (vanilla eBPF) and performs its standard safety analysis.
• Restoration & Execution: If verification passes, the JIT restores the extended instruction and dispatches it to a descriptor that supplies the native machine code for the specific architecture.

Constraints & Safety:

• The kernel core changes are minimal and generic.
• The verifier remains architecture-independent; it only sees the proof sequence.
• The Trusted Computing Base (TCB) is expanded only by the specific native emit code for each operation. The recognizer and proof sequences are not part of the TCB; if a recognizer bug produces an unsafe rewrite, the verifier will reject it.
• Formal Verification: The authors use Lean 4 to prove that for every operation, the native emit produces the same eBPF-visible architectural state as the proof sequence.

3. Key Contributions

• Kops Mechanism: A framework to extend the eBPF compilation pipeline with new operations while reusing the existing verifier for safety. It separates the safety proof (vanilla eBPF) from the performance optimization (native emit).
• EInsn Implementation: A concrete instantiation of Kops providing seven hardware-idiom operations (Rotate, Conditional Select, Bit Extract, Byte Swap, Prefetch, Bulk Copy, and LEA). These operations map to single native instructions on x86-64 and ARM64 where the standard eBPF set requires multiple instructions.
• Formal Proofs: Lean 4 proofs verifying the semantic equivalence between the proof sequences and the native emits for each EInsn operation, ensuring the verifier's guarantees carry over to the optimized code.
• Kernel Implementation: A 929-line addition to the Linux kernel core (covering verifier lowering/restoration, JIT dispatch, and registration) and a userspace compile-time recognizer.

4. Results

The evaluation was conducted on x86-64 and ARM64 using 27 pure-bytecode microbenchmarks and production applications (Cilium and Katran).

• Microbenchmark Performance:
  • x86-64: EInsn achieved up to 24% speedup (1.242×) over the unmodified kernel JIT, recovering 42% of the performance gap to native code.
  • ARM64: EInsn achieved up to 22% speedup (1.222×).
  • Code Size: Native code size decreased by 12–23%.
• Production Applications:
  • Cilium (x86-64): Throughput improved by 7.4% (1.074×).
  • Katran (ARM64): Throughput improved by 7.3% (1.073×).
• Overhead: Load-time overhead was negligible (geometric mean ratio of 0.99× relative to stock kernel).
• Policy Sensitivity: The study highlighted that blindly enabling all matched sites does not always yield optimal performance; a "profitability" policy (selecting families based on workload-specific gains) is more effective than maximizing coverage.
• Upper Bound Comparison: The authors compared EInsn against a "native-in-kernel" approach (trusting the entire application's native code). While the native approach achieved 2.358× speedup on Cilium, it required trusting the application's native code, significantly enlarging the TCB. EInsn occupies a middle ground, offering controlled speedups without trusting the full application binary.

5. Significance and Claims

The paper claims that Kops successfully addresses the performance limitations of the eBPF JIT without compromising its safety model or significantly enlarging the TCB. By decoupling the safety proof (vanilla eBPF) from the performance optimization (native emit), Kops allows for the introduction of hardware-specific idioms that were previously impossible to utilize safely within the kernel.

The authors emphasize that this approach avoids the need for upstream kernel JIT modifications or instruction set revisions. Instead, new operations are shipped as loadable kernel modules. The work demonstrates that a small, bounded set of hardware idioms can recover a significant portion of the eBPF-native performance gap, making eBPF a more viable option for high-performance, low-latency kernel tasks while maintaining the rigorous safety guarantees required for kernel execution.