Unifying Theories of Confidentiality

13 years 9 days ago
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.
Michael J. Banks, Jeremy L. Jacob
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where UTP
Authors Michael J. Banks, Jeremy L. Jacob
Comments (0)