Today, automated reasoning about program behavior is a well-established discipline in computer science, with a wide array of tools and techniques.
In the most common scenario, the goal is to prove trace properties of programs, such as termination or functional correctness.
However, not all program properties can be expressed as properties of individual traces.
Hyperproperties are properties which relate different executions of the same program, and include non-interference, determinism, and injectivity, among others.
For example, proving determinism for a program requires showing that any two executions with identical initial states will produce identical final states.
Non-interference classifies a program’s inputs and outputs as either low (public) and high (secret). A program is said to fulfill non-interference if the low outputs are not influenced by the high inputs, i.e., if in several
runs of the program with identical low inputs (but possibly different high inputs), the resulting low outputs are identical.