By the same authors

From the same journal

From the same journal

On integrating confidentiality and functionality in a formal method

Research output: Contribution to journalArticle

Published copy (DOI)



Publication details

JournalFormal Aspects of Computing
DateE-pub ahead of print - 27 Sep 2013
DatePublished (current) - 2014
Issue number5
Number of pages30
Pages (from-to)963-992
Early online date27/09/13
Original languageEnglish


This paper proposes a formal method, based on Circus, for developing software systems that respect a joint specification of functionality and confidentiality attributes. We extend the semantics of Circus to capture the information that users can infer about a system’s behaviour, enabling confidentiality and functionality attributes of a system to be specified together. We represent inconsistencies between functionality and confidentiality properties as miracles, rendering insecure functionality infeasible. We present techniques for verifying that a system design’s functionality and confidentiality attributes are mutually consistent, and for ensuring that consistency is maintained by refinement steps.

    Research areas

  • Information flow security, Confidentiality properties, Circus, Unifying theories of programming, Miracles, Confidentiality-preserving refinement

Discover related content

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

View graph of relations