Unifying Theories of Confidentiality

Abstract. This paper presents a framework for reasoning about the security of confidential data within software systems. A novelty is that we use Hoare and He's Unifying Theories of Programming (UTP) to do so and derive advantage from this choice. We identify how information flow between users can be modelled in the UTP and devise conditions for verifying that system designs may not leak secret information to untrusted users. We also investigate how these conditions can be combined with existing notions of refinement to produce refinement relations suitable for deriving secure implementations of systems.

• Type: Journal
• Year: 2010
• Where: UTP
• Authors: Michael J. Banks, Jeremy L. Jacob
• Keywords: Confidential Data, Programming Languages, Refinement Relations, Secure Implementations, UTP 2010