Hyperproperties

TLDR

Trace properties are sets of execution traces used for reasoning about systems, while hyperproperties extend this by expressing security policies such as secure information flow and service level agreements that trace properties cannot capture. The paper introduces hyperproperties as sets of trace properties. The authors present a verification technique for safety hyperproperties that generalizes prior secure information flow methods, show that refinement applies to safety hyperproperties, and provide a topological characterization of hyperproperties. The study demonstrates that safety and liveness generalize to hyperproperties, every hyperproperty is the intersection of a safety and a liveness hyperproperty, and introduces a verification technique, refinement applicability, and a topological characterization.

Abstract

Trace properties, which have long been used for reasoning about systems, are sets of execution traces. Hyperproperties, introduced here, are sets of trace properties. Hyperproperties can express security policies, such as secure information flow and service level agreements, that trace properties c annot. Safety and liveness are generalized to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. A verification technique for safety hyperproperties is given and is shown to generalize prior techniques for verifying secure information flow. Refinement is shown to be applicable with safety hyperproperties. A topological characterization of hyperproperties is given.