Qualitative and quantitative information flow with applications to security

Speaker: Annabelle McIver

Abstract

In this series of lectures I will describe how to use abstraction and refinement to reason about confidentiality properties in sequential programs. In the first two lectures a simple model based on Kripke structures is used to give a qualitative semantics to determine whether secret information is leaked inadvertently and in lectures 3&4 those ideas are generalised to enable the quantitative analysis of how much any leaked information can be used by an adversary.

Throughout the lectures the emphasis is on reasoning rules and the comparison of programs (and specifications) using a refinement order which maintains both functional consistency as well as information flow properties.

The approach is illustrated by a number of well-known case studies drawn from the security literature.