A Temporal Logic of Security
This work addresses the need for formal verification of security policies in systems, though it appears incremental as it builds on existing temporal logic frameworks.
The authors tackled the problem of verifying security policies by proposing HyperLTL, a new logic that extends linear-time temporal logic to express information-flow policies LTL cannot, and they implemented a model-checking algorithm in a prototype.
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.