By the same authors

Unifying theories of confidentiality

Research output: Contribution to conferencePaper



Publication details

DatePublished - 2010
Original languageEnglish


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.

    Research areas

  • MAKS, UTP, computer security, confidentiality properties, confidentiality-preserving refinement, information flow

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations