Synthesizing JIT Compilers for In-Kernel DSLs

Abstract.Modern operating systems allow user-space applications tosubmit code for kernel execution through the use of in-kernel domain spe-cific languages (DSLs). Applications use these DSLs to customize systempolicies and add new functionality. For performance, the kernel executesthem via just-in-time (JIT) compilation. The correctness of these JITsis crucial for the security of the kernel: bugs in in-kernel JITs have ledto numerous critical issues and patches.

#todo