Verifcation of Hyperproperties (Apr-Jun '14) - July 2014

Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.

PI(s): Michael Clarkson (GW/Cornell), Mike Hicks (UMCP)
Researchers: Masoud Koleini (GW/Univ of Nottingham, UK), Kris Micinski (UMCP)

HARD PROBLEM(S) ADDRESSED

This refers to Hard Problems, released November 2012.

Compositional security---the construction of secure systems  from components with known security properties---is an important and unsolved problem.  We might, at first, think to employ the theory of trace properties, which characterizes correct behavior of programs in terms of properties of individual execution paths, to develop compositional security.  After all, that theory developed out of an interest in proving the correctness of programs, and compositionality is important in correctness, too.

Verification of security, unfortunately, isn't directly possible with that theory, because some important security policies require sets of execution paths to model. But there is reason to believe that similar verification methodologies could be developed for security: the theory of hyperproperties [Clarkson & Schneider 2010], invented by PI Clarkson, generalizes the theory of trace properties to security policies.

Hyperproperties are sets of trace properties, which themselves are sets of execution traces. Hyperproperties can express security policies, such as secure information flow and service level agreements, that trace properties cannot. PI Clarkson showed that

1. safety (nothing ``bad'' happens) and liveness (something ``good'' happens) can be generalized from trace properties to hyperproperties,
2. every hyperproperty is the intersection of a safety hyperproperty and a liveness hyperproperty,
3. k-safety hyperproperties, in which the ``bad thing'' is finitely bounded, can be verified by self-composition, and
4. refinement is applicable with safety hyperproperties.

We have recently [1] been working on an automated verification methodology for security. In this methodology, security policies are expressed as logical formulas, and a model checker verifies those formulas. The formulas are expressed in a new logic named HyperLTL, which generalizes linear-time temporal logic (LTL).
LTL implicitly quantifies over only a single execution path of a system, but HyperLTL allows explicit quantification over multiple execution paths simultaneously, as well as propositions that stipulate relationships among those paths.  For example, HyperLTL can express information-flow policies.  Neither LTL nor branching-time logics (e.g., CTL and CTL*) can directly express such policies, because they lack the capability to correlate multiple execution paths.  Providing that capability is the key idea of HyperLTL.

In collaboration with a UMD PhD student working with PI Hicks, we have also developed a prototype model checker for HyperLTL.  The prototype currently scales only to small systems.

Relationship to Science of Security.  Security science is concerned, in part, with the capability to construct systems whose security is predictable [Schneider 2012].   A verification methodology for hyperproperties will enable verification that software systems satisfy  security policies, thus providing predictable security and increasing the trustworthiness of software.  Security science is also concerned with the establishment of laws that relate policies, attacks, and defenses [op.cit.].   The research proposed here would establish a relationship between policies (hyperproperties) and a defense (verification of software).

[1] Temporal Logics for Hyperproperties. In Proc. Conference on Principles of Security and Trust, pages 265-284, April 2014. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez.

PUBLICATIONS
Report papers written as a results of this research. If accepted by or submitted to a journal, which journal. If presented at a conference, which conference.

None yet.

ACCOMPLISHMENT HIGHLIGHTS