Provable Protection of Confidential Data in Microkernel-Based Systems

Modern computer systems process increasing amounts of private, sensitive, and valuable information. Yet, despite significant academic and industrial efforts, most of today's operating systems (OSs) do not protect confidential data against unauthorized disclosure over covert channels. Large trusted computing bases and high covert-channel analysis costs are two factors contributing to this situation.

In my thesis Provable Protection of Confidential Data in Microkernel-Based Systems, I approach the visionary goal of a cost-efficient, provable, and perfect protection of confidential data against leakage over covert communication channels. To achieve this goal, I combine the complementary strength of microkernels and of security type systems. This webpage presents my thesis and links to its accompanying sources.

PVS Sources: