Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
source link: https://www.tuicool.com/articles/uYZNvqi
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Overview
Modern operating systems run multiple interpreters in the kernel, which enable user-space applications to add new functionality or specialize system policies. The correctness 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 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. To help application 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. Experimental results show that Jitk is practical, fast, and trustworthy.
Publications
-
Jitk: A trustworthy in-kernel interpreter infrastructure.
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock.
Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI '14) , Broomfield, CO, October 2013. -
Security bugs in embedded interpreters.
Haogang Chen, Cody Cutler, Taesoo Kim, Yandong Mao, Xi Wang, Nickolai Zeldovich, and M. Frans Kaashoek.
Proceedings of the 4th ACM SIGOPS Asia-Pacific Workshop on Systems (APSys '13) , Singapore, July 2013.
Software
You can get a copy of Jitk from our git repository:
git clone git://g.csail.mit.edu/jitk
A modified version of Linux with changes necessary to invoke Jitk for Seccomp is here:
git clone git://g.csail.mit.edu/jitk-linux
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK