Kernohan: A High-Integrity, High-Assurance Microkernel for Embedded Systems
📜 Abstract
The proposed presentation introduces Kernohan, a new microkernel designed for high-assurance embedded systems, as part of our work on trustworthy systems. Kernohan’s design builds on our existing high-assurance, formally-verified seL4 kernel. It is intended as a platform for secure, safety-critical software, with a particular focus on defence, automotive, and avionics applications. Kernohan embodies several innovations for supporting static resource management, security, and fault-tolerance. Additionally, the presentation discusses results from our evaluation which demonstrate the performance and integrity benefits of Kernohan in comparison to current state-of-the-art microkernels like L4-embedded and CAmkES.
✨ Summary
This paper introduces Kernohan, a microkernel aimed at providing high assurance for embedded systems, with an emphasis on secure, safety-critical applications such as those in defense, automotive, and avionics industries. Building upon the formally-verified seL4 microkernel, Kernohan incorporates innovations in static resource management, security, and fault-tolerance. The authors present performance evaluations showing advantages over existing microkernels like L4-embedded and CAmkES.
The paper appears not to have a wide citation presence, and there are no specific influences or direct references found in extensive web searches. It might be contributing to ongoing research and development within the field of secure embedded systems and formal verification processes. However, no specific papers or projects have been widely noted to cite or build upon Kernohan directly as of now.