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:
-
Noninterference of a Budget-Enforcing Fixed-Priority Scheduler
Soundness of the Control-Flow-Sensitive Security Type System for Low-Level Operating-System Code