Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

High assurance systems used in avionics, medical implants, and cryptographic devices often rely on a small trusted base of hardware and software to manage the rest of the system. Crafting the core of such a system in a way that achieves flexibility, security, and performance requires a careful balancing act. Simple static primitives with hard partitions of space and time are easier to analyze formally, but strict approaches to the problem at the hardware level have been extremely restrictive, failing to allow even the simplest of dynamic behaviors to be expressed. Our approach to this problem is to construct a minimal but configurable architectural skeleton. This skeleton couples a critical slice of the low level hardware implementation with a microkernel in a way that allows information flow properties of the entire construction to be statically verified all the way down to its gate-level implementation. This strict structure is then made usable by a runtime system that delivers ...

• Type: Journal
• Year: 2011
• Where: ISCA
• Authors: Mohit Tiwari, Jason Oberg, Xun Li 0001, Jonathan Valamehr, Timothy E. Levin, Ben Hardekopf, Ryan Kastner, Frederic T. Chong, Timothy Sherwood
• Keywords: Computer Systems Organization, Hardware, Inter Process Communication, ISCA 2011, Medical Implants