On Confidentiality and Formal Methods
Michael J. Banks · White Rose eTheses Online (University of Leeds, The University of Sheffield, University of York) · 2012
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