Automatic Inference of Hyperproperties

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.

Eilers et al. developed a methodology to verify general hyperproperties (and non-interference in particular)¹, and implemented it in the Viper framework. To achieve this, they build a modular product program, which simulates several executions of the original program. A hyperproperty can then be expressed as a trace property of the product program, and verified using standard verifiers. However, as is generally the case with deductive verification, Eilers’ methodology requires specifications to be added to the program in the form of pre- and postconditions, and loop invariants. This is cumbersome in general, and specifications for hyperproperties are especially verbose and difficult to find.

In this thesis (as part of the VerifiedSCION program), I developed a framework to automatically infer such specifications, in order to prove hyperproperties with less or even without programmer input. Concretely, I developed a static analysis to infer specifications on product programs, and implement it in the static analyzer Sample, which is part of the Viper framework. My work served as the foundation for another thesis² that applied this framework to GPU kernels.