Hyperproperties [Clarkson and Schneider 2010] can express security policies, such as secure information flow and service level agreements, which the standard kinds of trace properties used in program verification cannot.
Our objective is to develop verification methodologies for hyperproperties.
We intend to apply those methodologies to the construction of secure systems from components with known security properties, thereby addressing the problem of compositional security.