Hyperproperties

Abstract

Trace properties, which have long been used for reasoning about systems, aresets 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 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 14, 2016
Accession Number
AD1000345

Entities

People

  • Fred B. Schneider
  • Michael R. Clarkson

Organizations

  • Cornell University

Tags

Communities of Interest

  • Biomedical

DTIC Thesaurus Topics

  • Channel Capacity
  • Coding
  • Computer Access Control
  • Computer Science
  • Computers
  • Construction
  • Cryptography
  • Cybersecurity
  • Notation
  • Observation
  • Observers
  • Probability
  • Set Theory
  • Specifications
  • Standards
  • Statistics
  • Theorems

Readers

  • Computational Modeling and Simulation
  • Cybersecurity.