Hyperproperties
∗
Michael R. Clarkson Fred B. Schneider
{clarkson,fbs}@cs.cornell.edu
Department of Computer Science
Cornell University
October 16, 2009
Abstract
Trace properties, which have long been used for reasoning about systems, are
sets of execution traces. Hyperproperties, introduced here, are sets of trace prop-
erties. Hyperproperties can express security policies, such as secure information
flow and service level agreements, that trace properties cannot. Safety and liveness
are generalized to hyperproperties, and every hyperproperty is shown to be the in-
tersection of a safety hyperproperty and a liveness hyperproperty. A verification
technique for safety hyperproperties is given and is shown to generalize prior tech-
niques for verifying secure information flow. Refinement is shown to be applicable
with safety hyperproperties. A topological characterization of hyperproperties is
given.
1 Introduction
Important security policies cannot be expressed as properties of individual execution
traces of a system [2,22,42, 52, 60,62, 64]. For example, noninterference [23] is a con-
fidentiality policy that stipulates commands executed on behalf of users holding high
clearances have no effect on system behavior observed by users holding low clearances.
It is not a property of individual traces, because whether a trace is allowed by the policy
depends on whether another trace (obtained by deleting command executions by high
users) is also allowed. For another example, stipulating a bound on mean response time
over all executions is an availability policy that cannot be specified as a property of in-
dividual traces, because the acceptability of delays in a trace depends on the magnitude
of delays in all other traces. However, both example policies are properties of systems,
because a system (viewed as a whole, not as individual executions) either does or does
not satisfy each policy.
∗
Supported in part by AFOSR grant F9550-06-0019, National Science Foundation Grants 0430161 and
CCF-0424422 (TRUST), an Intel Foundation Ph.D. Fellowship, and a gift from Microsoft Corporation.
