Proving execution platform contracts

Since the discovery of the Spectre vulnerability and its media coverage, micro-architectural side channel attacks have gained considerable interest, both in research and the general public. These side channels threaten many usage scenarios that have become central to everybody’s daily lives. Be it cloud services, where virtual machines share the same physical hardware, be it web applications on different tabs of one’s web browser, or be it applications on one’s smart phone. In all these cases, sensitive data might be processed by software running on a hardware platform along with potentially malicious other pieces of software. Due to the micro-architectural side channels the malicious software may observe how this sensitive data is processed and thus extract information on the data – effectively leaking sensitive information. New vulnerabilities and counter-measures are discovered and publicized at a frantic rate, calling for a sea change in the way micro-architecture designs and software process sensitive data. Hardware/software contracts were recently proposed to establish a formal framework, providing formal guarantees against information leakage and allowing a clear separation of concerns between hardware and software. However, these contracts only focus on the interactions between the micro-architecture and the application software, missing a crucial element that governs and mediates most of these interactions: system software – such as operating systems or hypervisors. The objective of this work is to fill this gap and extend the contracts to include the operating system (OS). For this we formalize thread and memory management policies provided by the OS on top of a hardware model in order to study information leakage on such a platform . We first show through an exploration of concrete examples that the OS plays a crucial role in providing security guarantees to software processing sensitive data. Finally, we apply an inductive proof strategy on these formal platform models in order to establish contracts between the software, the OS, and the hardware.