Provable Protection of Confidential Data in Microkernel-Based Systems

Although modern computer systems process increasing amounts of sensitive, private, and valuable information, most of today’s operating systems (OSs) fail to protect confidential data against unauthorized disclosure over covert channels. Securing the large code bases of these OSs and checking the secured code for the absence of covert channels would come at enormous costs. Microkernels significantly reduce the necessarily trusted code. However, cost-efficient, provable confidential-data protection in microkernel-based systems is still challenging. This thesis makes two central contributions to the provable protection of confidential data against disclosure over covert channels: • A budget-enforcing, fixed-priority scheduler that provably eliminates covert timing channels in open microkernel-based systems; and • A sound control-flow-sensitive security type system for low-level operating-system code. To prevent scheduling-related timing channels, the proposed scheduler treats possibly leaking, blocked threads as if they were runnable. When it selects such a thread, it runs a higher classified budget consumer. A characterization of budget-consumer time as a blocking term makes it possible to reuse a large class of existing admission tests to determine whether the proposed scheduler can meet the real-time guarantees of all threads we envisage to run. Compared to contemporary information-flow-secure schedulers, significantly more real-time threads can be admitted for the proposed scheduler. The role of the proposed security type system is to prove those system components free of security policy violating information flows that simultaneously operate on behalf of differently classified clients. In an open microkernel-based system, these are the microkernel and the necessarily trusted multilevel servers. To reduce the complexity of the security type system, C++ operating-system code is translated into a corresponding Toy program, which in turn is complemented with calls to Toy procedures describing the side effects of interactions with the underlying hardware. Toy is a non-deterministic intermediate programming language, which I have designed specifically for this purpose. A universal lattice for shared-memory programs enables the type system to check the resulting Toy code for potentially harmful information flows, even if the security policy of the system is not known at the time of the analysis. I demonstrate the feasibility of the proposed analysis in three case studies: a virtual-memory access, L4 inter-process communication and a secure buffer cache. In addition, I prove Osvik’s countermeasure effective against AES cache side-channel attacks. To my best knowledge, this is the first security-type-system-based proof of such a countermeasure. The ability of a security type system to tolerate temporary breaches of confidentiality in lock-protected shared-memory regions turned out to be fundamental for this proof