Hyperproperties Project

Team:

External collaborators:

  • Michael Clarkson (George Washington University)

Problem

Hyperproperties, introduced in Michael Clarkson and Fred Schneider’s “Hyperproperties” paper, are predicates over sets of traces, as opposed to (trace) properties, which are predicates over single traces. Hyperproperties capture important security policies that cannot be expressed as properties.

The common notion of refinement as inclusion of sets of traces preserves properties but not always hyperproperties, because hyperproperties are not always closed under subsets. This means that a secure system (i.e. one satisfying certain hyperproperties) can be refined to an insecure system (i.e. one that no longer satisfies those hyperproperties).

The goal of this project is to investigate approaches to refinement that preserve hyperproperties.

Solution

We have developed ‘pop-refinement’, which is an approach to refinement in which specifications are predicates over programs and refinement is inclusion of predicates (‘pop’ stands for ‘predicates over programs’).

In pop-refinement, a specification (i.e. predicate over programs) can capture both functional and non-functional requirements, and refinement (i.e. inclusion of predicates over programs) always preserves all requirements. This applies to hyperproperties as well: every hyperproperty expressed or implied by the initial specification is preserved through all the refinements to the implementation.

Besides capturing and preserving hyperproperties, pop-refinement can also capture and preserve non-functional requirements that are notoriously difficult to express in common specification formalisms, e.g. constraints on memory footprint or absence of information leaks through low-level interfaces.

We have developed various simple examples of pop-refinement, some of which involve hyperproperties like generalized non-interference (i.e. a generalization of non-interference for non-deterministic systems; generalized non-interference is not closed under subsets). We plan to develop increasingly more complex examples.

Publications

Pop-Refinement
Alessandro Coglio
July 2014
Archive of Formal Proofs
{Description of pop-refinement, with two examples developed in Isabelle/HOL, one of which features hyperproperties.}