Securing concurrent programs with dynamic information-flow control

The work presented in this thesis focusses on dealing with timingcovert channels in dynamic information-flow control systems,particularly for the LIO library in Haskell.Timing channels are dangerous in the presence ofconcurrency. Therefore, 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. Wealso mitigate leaks that result from the precise measurement of thetiming of observable events (external timingcovert channel), e.g. by using a stopwatch.Timing channels can also be exploited through hardware-based sharedresources, such as the processor cache. This thesis presents acache-based attack on LIO that relies on timing perturbations to leaksensitive information through internal timing. To address thisproblem, we modify the Haskell runtime to support instruction-basedscheduling, a scheduling strategy that is indifferent to suchperturbations from underlying hardware components, such as the cache,TLB, and CPU buses. We show this scheduler is secure againstcache-based internal timing attacks for applications using a singleCPU. Additionally, we provide a purely language-based implementationof the instruction-based strategy for LIO, by means of a library. Weleverage the notion of resumptions, a restricted form ofcontinuations, to control the interleaving of threads, forcing eachthread to yield after every LIO operation. Due to the flexibility ofthis approach, we are able to support parallel computation in thelibrary, a novel feature in information-flow control tools.Finally, we present a new manifestation of internal timing in Haskell,by exploiting lazy evaluation to encode sensitive information astiming perturbations. We illustrate our claim with a concrete attackon LIO that relies on memoisation of shared thunks to leakinformation. We also propose a countermeasure based on restricting theimplicit sharing of values