Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
Xi Wang, David Lazar, Nickolai Zeldovich, Adam J. Chlipala, Zachary Tatlock · 2015
Modern operating systems run multiple interpreters in the kernel, which enable user-space applications to add new functionality or specialize system policies. The correct-ness of such interpreters is critical to the overall system security: bugs in interpreters could allow adversaries to compromise user-space applications and even the kernel. Jitk is a new infrastructure for building in-kernel in-terpreters that guarantee functional correctness as they compile user-space policies down to native instructions for execution in the kernel. To demonstrate Jitk, we im-plement two interpreters in the Linux kernel, BPF and INET-DIAG, which are used for network and system call filtering and socket monitoring, respectively. To help ap-plication developers write correct filters, we introduce a high-level rule language, along with a proof that Jitk correctly translates high-level rules all the way to native machine code, and demonstrate that this language can be integrated into OpenSSH with tens of lines of code. We built a prototype of Jitk on top of the CompCert verified compiler and integrated it into the Linux kernel. Ex-perimental results show that Jitk is practical, fast, and trustworthy. 1