owards a Formally Secure eBPF - Frédéric Besson

eBPF is a technology for running user-provided code with kernel
privileges.  Originally designed to perform in-kernel packet
filtering, eBPF has gained traction and eBPF scripts may be hooked in
various sub-systems of the Linux kernel. They provide a versatile way
to extend the kernel without sacrificing its integrity.

In this talk, I will present an overview of the eBPF ecosystem,
notably the verifier which is the sentry of the kernel.  I will
discuss current formalisation efforts regarding the semantics of eBPF, its verifier and its JIT compiler.