A Temporal Logic of Security

TL;DR

This paper introduces HyperLTL, a novel temporal logic that extends LTL with quantification over multiple execution paths, enabling the expression and verification of complex security policies beyond traditional methods.

Contribution

The paper presents HyperLTL, a new logic for security policy verification, along with a model-checking algorithm and implementation, expanding the expressiveness of security policy specification.

Findings

HyperLTL can express information-flow security policies not possible with LTL.

A model-checking algorithm for a fragment of HyperLTL is developed and implemented.

HyperLTL's expressiveness is characterized by an arithmetic hierarchy of hyperproperties.

Abstract

A new logic for verification of security policies is proposed. The logic, HyperLTL, extends linear-time temporal logic (LTL) with connectives for explicit and simultaneous quantification over multiple execution paths, thereby enabling HyperLTL to express information-flow security policies that LTL cannot. A model-checking algorithm for a fragment of HyperLTL is given, and the algorithm is implemented in a prototype model checker. The class of security policies expressible in HyperLTL is characterized by an arithmetic hierarchy of hyperproperties.