Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 963-992 |
| Number of pages | 30 |
| Journal | Formal Aspects of Computing |
| Volume | 26 |
| Issue number | 5 |
| Early online date | 27 Sept 2013 |
| DOIs | |
| Publication status | Published - 2014 |
Keywords
- Information flow security
- Confidentiality properties
- Circus
- Unifying theories of programming
- Miracles
- Confidentiality-preserving refinement
