Jitk: A Trustworthy In-Kernel Interpreter Infrastructure

Modern operating systems run multiple interpreters in the kernel, which enable user-space applications to add new functionality or specialize system policies. Jitk is a new infrastructure for building in-kernel interpreters that guarantee functional correctness as they compile user-space policies down to native instructions for execution in the kernel. To demonstrate Jitk, we implement two interpreters in the Linux kernel, BPF and INET-DIAG, which are used for network and system call filtering and socket monitoring, respectively.

Source: css.csail.mit.edu