Leakage in Trustworthy Systems

Abstract

This dissertation presents a survey of the theoretical and practical techniques necessary to provably eliminate side-channel leakage through known mechanisms in component-based secure systems.

We cover the state of the art in leakage measures, including both Shannon and min entropy, concluding that Shannon entropy models the observed behaviour of our example systems closely, and can be used to give a safe bound on vulnerability in practical scenarios.

We comprehensively analyse several channel-mitigation strategies: cache colouring and instruction-based scheduling, showing that effectiveness and ease of implementation depend strongly on subtle hardware features. We also demonstrate that real-time scheduling can be employed to effectively mitigate remote chan nels at minimal cost.

Finally, we demonstrate that we can reason formally (and mechanically) about probabilistic non-functional properties, by formalising the probabilistic language pGCL in the Isabelle/HOL theorem prover, and using it to verify an implementation of lattice scheduling, a well-known cache-channel countermeasure. We prove that a correspondence exists between standard vulnerability bounds, in a channel-centric view, and the refinement lattice on programs in pGCL, used to model a guessing attack on a vulnerable system—a process-centric view.