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. 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 is . This representation is expressive enough to encompass several computational models, including labeled transition systems and state machines. Hyperproperties A trace property is a set of traces. Safety and liveness properties are trace properties. Formally, a trace property is an element of , where is the powerset operator. A hyperproperty is a set of trace properties, that is, an element of . 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. Analogously, hyperproperties may be divided into hypersafety and hyperliveness hyperproperties, and every hyperproperty is an intersection of a safety hyperproperty and a liveness hyperproperty. -safety properties are safety hyperproperties such that every violation of the property can be witnessed by a set of at most traces. Examples Every safety property can be lifted to a 1-safety hyperproperty that expresses the same condition. -safety hyperproperties: (lifts of safety properties): false, defined to be the set containing the empty set. Formally, . This hyperproperty is not satisfied by any system. true, defined to be the set of all traces. Formally, . This hyperproperty is satisfied by all systems. Access control : Monotonicity Injectivity Symmetry, anti-symmetry, and asymmetry Observational determinism Noninterference Transitivity Associativity Properties Since hyperproperties are exactly the elements of the power set , 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. Applications Several program logics (most notably, HyperLTL) and model checking algorithms have been developed for checking that a system conforms to a hyperproperty. References Notes Sources