Improving the Isolation in Unikernels by Leveraging Microkernel Design

Abstract

Abstract Modern systems demand strong isolation guarantees to protect against software vulnerabilities and maintain robust security boundaries. Traditional operating systems often fall short due to their large trusted computing bases and reliance on discretionary access control mechanisms. The seL4 microkernel, with its formally verified design and capability-based access control, presents a compelling foundation for building highly secure, isolated systems. This study explores the feasibility of running unikernel applications such as Rumprun, on top of seL4, aiming to combine the minimalism and efficiency of unikernels with the strong isolation guarantees of seL4. Two different integration approaches were attempted by directly running a Rumprun binary in a minimal seL4 environment and embedding a Rumprun application within a CAmkES component. Both efforts encountered technical obstacles. Despite these practical limitations, the theoretical underpinnings of seL4’s capability system suggest that high isolation levels are achievable if integration complexity can be addressed. Initial experiments highlight that a hybrid architecture, combining minimal seL4 or CAmkES components with standalone unikernels might strike a balance between performance and isolation. Future directions include debugging existing integration challenges, evaluating the performance implications of different architectural decisions, and exploring alternative unikernel frameworks for better alignment with seL4’s static and modular design principles. The findings support that seL4 is well-suited for hosting unikernels in security-critical environments, provided that toolchain and architectural hurdles are resolved.