Helix Project Testbed - Towards the Self-Regenerative Incorruptible Enterprise

Information flow is an important security property that must be incorporated from the ground up, including at hardware design time, to provide a formal basis for a systems root of trust. We incorporate insights and techniques from designing information-flow secure programming languages to provide a new perspective on designing secure hardware. An important result of our DURIP is a new hardware description language, Caisson, that combines domain-specific abstractions common to hardware design with insights from type-based techniques used in secure programming languages. The proper combination of these elements allows for an expressive, provably-secure HDL that operates at a familiar level of abstraction to the target audience of the language, hardware architects. Additional work in this DURIP was to construct a minimal but configurable secure 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.