Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns---e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements---are subsumed by the beautiful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been very successful but limited to an impoverished notion of specification: trace properties. Some mathematically precise properties of programs---dubbed hyperproperties---refer to traces collectively. For example, confidentiality involves knowledge of possible traces. This article reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, especially in connection with loops, and suggests directions for further research. The main results are: the first compositional semantics of imperative programs with loops, at the hyper level, and a proof that this semantics is the same as the direct image of a standard semantics, for subset closed hyperproperties.
Fine grained information flow monitoring can in principle address a wide range of security and privacy goals, for example in web applications. But it is very difficult to achieve sound monitoring with acceptable runtime cost and sufficient precision to avoid impractical restrictions on programs and policies. We present a systematic technique for design of monitors that are correct by construction. It encompasses policies with downgrading. The technique is based on abstract interpretation which is a standard basis for static analysis of programs. This should enable integration of a wide range of analysis techniques, enabling more sophisticated engineering of monitors to address the challenges of precision and scaling to widely used programming languages. Stepwise refinement is a crucial conceptual tool for system development, encouraging program construction via a number of separate correctness-preserving stages which ideally can be understood in isolation. A crucial conceptual component of security is an adversary's ignorance of concealed information. We suggest a novel method of combining these two ideas. Our suggestion is based on a mathematical definition of ''ignorance-preserving'' refinement that extends classical refinement by limiting an adversary's access to concealed information: moving from specification to implementation should never increase that access. The novelty is the way we achieve this in the context of sequential programs. Specifically we give an operational model (and detailed justification for it), a basic sequential programming language and its operational semantics in that model, a ''logic of ignorance'' interpreted over the same model, then a program-logical semantics bringing those together - and finally we use the logic to establish, via refinement, the correctness of a real (though small) protocol: Rivest's Oblivious Transfer. A previous report^@? treated Chaum's Dining Cryptographers similarly. In passing we solve the Refinement Paradox for sequential programs. 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. 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.