Language Support for Controlling Timing-Based Covert Channels

The problem of controlling information flow in multithreaded programs remains an important open challenge.A major difficulty for tracking information flow in concurrent programs is due to the internal timing covert channel. Information is leaked via this channel when secrets affect the timing behavior of a thread, which, via the scheduler, affects the interleaving of public events. This channel is particularly dangerous because, in contrast to external timing, the attacker does not need to observe the actual execution time of programs. This thesis introduces a novel treatment of the interaction between threads and the scheduler. As a result, a permissive security specification and a compositional security type system are obtained. The type system guarantees security for a wide class of schedulers and provides a flexible treatment of dynamic thread creation and synchronization. The approach relies on the modification of the scheduler in the run-time environment. In some scenarios, the modification of the run-time environment might not be an acceptable requirement. For such scenarios, the thesis presents two transformations that eliminate the need for modifying the scheduler while avoiding internal timing leaks. The first transformation is given for programs running under cooperative schedulers. It states that threads must not yield control inside of computations that branch on secrets. The second transformation closes internal timing channel when the scheduler is preemptive and behaves as round-robin. It spawns dedicated threads, whenever computation may affect secrets, and carefully synchronizes them. This dissertation also presents two libraries for information-flowsecurity in Haskell. The first proposed library supports multithreaded code and evaluates the implementations of some of the ideas described above to avoid internal timing leaks. This implementation includes an online-shopping case study. The case study reveals that exploiting concurrency to leak secrets is feasible and dangerous in practice and shows how the library can help avoiding internal timing leaks. Up to the publication date, this is the first tool that provides information-flow security in multithreaded programs and the first implementation of a case study that involves concurrency and information-flow policies. The second library, in constrast, is designed for sequential programs and includes a novel treatment for inteded release of information (declassification)