Securing functional programs with floating-label information-flow control

The work presented in this thesis focuses on information-flow control systems for functional programs, particularly on the LIO library in Haskell. The thesis considers threemain aspects in this area: timing covert channels, dynamic policies andenforcement mechanisms that improve precision of the analysis.Timing channels are dangerous in the presence ofconcurrency. We start with the design, formalisation andimplementation of a concurrent version of LIO which is secure againstthem. More specifically, we remove leaks due to non-terminatingbehaviour of programs (termination covert channel) and leaks producedby forcing certain interleavings of threads, as a result of affectingtheir timing behaviour (internal timing covert channel). The keyinsight is to decouple computations so that threads observing thetiming or termination behaviour of other threads are required to be atthe same confidentiality level. This work only deals with internaltiming that can be exploited through language-level operations.We also mitigate leaks that result from the precise measurement of thetiming of observable events (external timing covert channel), e.g. byusing a stopwatch. In further work, we tackle leaks that result fromhardware-based shared resources, such as the processor cache. Thisthesis presents a cache-based attack on LIO and proposes two solutionsthat rely on time-agnostic scheduling: the first one consists in amodification to the Haskell runtime and the other one is a purelylanguage-based implementation. We also present a new manifestation ofinternal timing in Haskell, by exploiting lazy evaluation to encodesensitive information as timing perturbations.Dynamic policies arise when the set of allowed flows of information ispermitted to change as the program runs. Declassification can beviewed as a special case of dynamic policies. This thesis introducesan extension to LIO which supports dynamic policies and can encodewell-known label formats such as the DLM and DC labels. Moreover, wealso present the notion of restricted privileges, giving principalsthe ability to restrict the ways in which their authority can be usedin the system, and supporting robust declassification.We also add flow-sensitivity to LIO, whichconsists in the ability for the security labels of references tomutate, depending on the sensitivity of what is stored in them.Finally, we introduce a hybrid enforcement which mixes staticand dynamic analyses. In particular, we leverage advanced type systemfeatures in Haskell to give the programmer control over which parts ofthe program are dynamically checked and which parts are staticallychecked. The core of this library is a general technique for deferringchecking of type-class constraints to runtime which is applicable toother domains beyond language-based security