Performance evaluation of the Linux kernel eBPF verifier

Day 1 | 17:00 | 00:20 | K.4.201 | Julia Lawall, Maxime Derri

Note: I'm reworking this at the moment, some things won't work.

The stream isn't available yet! Check back at 17:00.
Get involved in the conversation!Join the chat

Integrated in the Linux kernel since 2014, eBPF has allowed the creation of a large variety of projects (observability, security, network, etc.). Unlike kernel modules, eBPF programs can be loaded by unprivileged users. The Linux kernel is protected by a static analyzer, called the eBPF verifier, which verifies that eBPF programs cannot harm the kernel and respect required security properties. Recently, several research works have shown that the eBPF verifier, which is a critical component, is not sound. This means that programs which should be rejected are accepted by the verifier, allowing unprivileged users to run malicious programs (e.g [1,2,3,4,5]). In this talk, we propose to evaluate the performance of the eBPF verifier through the measurement of three main aspects:

  • Performance evaluation: to understand the evolution of the eBPF verifier versions, we evaluated the verification time and consumed memory of six eBPF verifier versions (Linux kernel 5.0 to 6.8, both included). The results show that for some eBPF programs, the verifiers have nearly the same verification times (except for the conditional jumps, where the verification time has decreased since the introduction of the bounded loops in the Linux kernel 5.3). Consumed memory remains also stable.

  • Comparative evaluation with PREVAIL: as the eBPF verifier is not sound, we compared it to PREVAIL, which is another verifier proposed in 2019 at the PLDI conference. PREVAIL is a sound verifier that runs in user space and is used in the eBPF infrastructure of Windows. On the one hand, we were interested in the implementation differences between the two verification solutions and on the other hand, we observed the performance difference between the two verifiers. We observed that, although PREVAIL's performance has improved, it remains less efficient than the eBPF verifier. Nevertheless, PREVAIL showed that it can efficiently verify programs containing a lot of paths (implied by conditional jumps) thanks to the join operator and the fixpoint computation used for the bounded loops, where the eBPF verifier would have created a lot of paths, trying to reduce them with pruning.

  • Impact of compilers: beyond the verification mechanisms, there are external constraints such as the compilers: An eBPF program is first compiled into eBPF bytecode and then analyzed. However, we observed that for the eBPF verifier with a specific eBPF program, which varies only by its number of loop iterations, Clang-8 produced more programs accepted by the eBPF verifier and these programs are verified faster than those produced by Clang-14.