Hyperproperty

In computer science, hyperproperties are a formalism for describing properties of computational systems. Hyperproperties generalize safety and liveness properties, and can express properties such as non-interference and observational determinism.^[1]

Elaborating on the example of non-interference: Non-interference can't be represented as a "property" in the formal sense because there's no inclusion-test that could be applied to a single program trace; non-interference is an assertion about how neighboring traces are similar to each other and it does no good to look at one trace at a time. "Hyperproperties" are the extension from properties as predicates on traces to properties as relations between traces.

Definitions

Examples

• Every safety property can be lifted to a 1-safety hyperproperty that expresses the same condition.^[7]
• ${\displaystyle k}$-safety hyperproperties:
  • ${\displaystyle k=1}$ (lifts of safety properties):
    • false, defined to be the set containing the empty set. Formally, ${\displaystyle \mathbf {false} \triangleq \{\emptyset \}}$. This hyperproperty is not satisfied by any system.^[8]
    • true, defined to be the set of all traces. Formally, ${\displaystyle \mathbf {true} \triangleq \Phi }$. This hyperproperty is satisfied by all systems.^[9]
    • Access control^[10]
  • ${\displaystyle k=2}$:
    • Monotonicity^[11]
    • Injectivity^[11]
    • Symmetry, anti-symmetry, and asymmetry^[11]
    • Observational determinism^[12]
    • Noninterference
  • ${\displaystyle k=3}$
    • Transitivity^[11]
  • ${\displaystyle k=4}$
    • Associativity^[11]

Properties

Since hyperproperties are exactly the elements of the power set ${\displaystyle \mathbb {P} (\mathbb {P} (\Phi ))}$, they are closed under intersection and union.

The lower Vietoris topology of a standard topology on trace properties yields a topology on the set of hyperproperties.^[13]

Applications

Several program logics^[14][11][15] have been developed for checking that a program conforms to a hyperproperty.

HyperLTL^[14] and some model checking algorithms^[16][17] have been developed for checking that a finite state system conforms to a hyperproperty.

References