Execution leases: a hardware-supported mechanism for enforcing strong non-interference

High assurance systems such as those found in aircraft controls and the financial industry are often required to handle a mix of tasks where some are niceties (such as the control of media for entertainment, or supporting a remote monitoring interface) while others are absolutely critical (such as the control of safety mechanisms, or maintaining the secrecy of a root key). While special purpose languages, careful code reviews, and automated theorem proving can be used to help mitigate the risk of combining these operations onto a single machine, it is difficult to say if any of these techniques are truly complete because they all assume a simplified model of computation far different from an actual processor implementation both in functionality and timing. In this paper we propose a new method for creating architectures that both a) makes the complete information-flow properties of the machine fully explicit and available to the programmer and b) allows those properties to be veri...

• Type: Conference
• Year: 2009
• Where: MICRO
• Authors: Mohit Tiwari, Xun Li, Hassan M. G. Wassel, Frederic T. Chong, Timothy Sherwood
• Keywords: Actual Processor Implementation, Automated Theorem Proving, Hardware, MICRO 2009, Remote Monitoring Interface