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

Traces and systems

Hyperproperties are defined in terms of traces of a computational system. A trace is a sequence of states; a system is a set of traces. Intuitively, a program corresponds to the set of all of its possible execution traces, given any inputs. Formally, the set of traces over a set of states ${\displaystyle \Sigma }$ is ${\displaystyle \Phi \triangleq \Sigma ^{\omega }}$.

This representation is expressive enough to encompass several computational models, including labeled transition systems^[2] and state machines.^[3]

Hyperproperties

A trace property is a set of traces. Safety and liveness properties are trace properties. Formally, a trace property is an element of ${\displaystyle \mathbb {P} (\Phi )}$, where ${\displaystyle \mathbb {P} }$ is the powerset operator. A hyperproperty is a set of trace properties, that is, an element of ${\displaystyle \mathbb {P} (\mathbb {P} (\Phi ))}$.

Trace properties may be divided into safety properties (intuitively, properties that ensure "bad things don't happen") and liveness properties ("good things do happen"), and every trace property is the intersection of a safety property and a liveness property.^[4] Analogously, hyperproperties may be divided into hypersafety and hyperliveness hyperproperties, and every hyperproperty is an intersection of a safety hyperproperty and a liveness hyperproperty.^[5]

${\displaystyle k}$-safety properties are safety hyperproperties such that every violation of the property can be witnessed by a set of at most ${\displaystyle k}$ traces.^[6]

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

Notes