Team for Research in
Ubiquitous Secure Technology

Citation
Fred Schneider, Michael R. Clarkson. "Hyperproperties". Technical report, Journal of Computer Security, December, 2008.

Abstract
Properties, which have long been used for reasoning about systems, are sets of traces. Hyperproperties, introduced here, are sets of properties. Hyperproperties can express security policies, such as secure information flow and service level agreements, that properties cannot. 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.

Electronic downloads

• http://hdl.handle.net/1813/11660

• HTML

  Fred Schneider, Michael R. Clarkson. <a
  href="http://www.truststc.org/pubs/558.html"
  ><i>Hyperproperties</i></a>, Technical
  report,  Journal of Computer Security, December, 2008.

• Plain text

  Fred Schneider, Michael R. Clarkson.
  "Hyperproperties". Technical report,  Journal of
  Computer Security, December, 2008.

• BibTeX

  @techreport{SchneiderClarkson08_Hyperproperties,
      author = {Fred Schneider and Michael R. Clarkson},
      title = {Hyperproperties},
      institution = {Journal of Computer Security},
      month = {December},
      year = {2008},
      abstract = {Properties, which have long been used for
                reasoning about systems, are sets of traces.
                Hyperproperties, introduced here, are sets of
                properties. Hyperproperties can express security
                policies, such as secure information flow and
                service level agreements, that properties cannot.
                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.},
      URL = {http://www.truststc.org/pubs/558.html}
  }
  

Posted by Jessica Gamble on 20 Feb 2009.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.