On Confidentiality and Formal Methods

Abstract

The contemporary challenge of engineering verifiably secure software has motivated various techniques for measuring and regulating the flow of confidential data from systems to their users. Unfortunately, these techniques suffer from a lack of integration with modern formal methods for software development, which inhibits their application in practice. This thesis proposes a novel approach for integrating information flow security concerns with formal methods. Working in the Unifying Theories of Programming (UTP), this thesis presents a generic framework for modelling interactions between users and systems. This framework can be applied to encode information flow about a system's activities to its users. It thereby allows confidentiality properties to be formalised in the UTP as upper bounds on information flow to users. The main contribution of this thesis is a unified platform for designing software that is not only functionally correct, but also secure by design. This platform specialises the information flow encoding to the Circus formal method, making it possible to specify confidentiality properties within Circus processes. In this setting, conflicts between functionality and confidentiality are represented as miracles, rendering insecure functionality infeasible. The platform provides techniques for verifying that functionality and confidentiality properties are mutually consistent. These techniques can be applied to develop a process through a series of feasibility-preserving refinement steps, to achieve a system implementation that does not leak secret information to untrusted users. These techniques are evaluated with a brief case study.