On integrating confidentiality and functionality in a formal method
Michael J. Banks, Jeremy L. Jacob · Formal Aspects of Computing · 2013
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.