Flavours of Sequential Information Flow

TL;DR

This paper formalizes various types of sequential information-flow policies in reactive systems using Hypertrace Logic, revealing limitations of HyperLTL in expressing most of these variants and introducing new methods for inexpressiveness proofs.

Contribution

It introduces Hypertrace Logic for specifying sequential information-flow and demonstrates HyperLTL's inability to express many variants, advancing understanding of logical expressiveness in security policies.

Findings

Hypertrace Logic effectively formalizes sequential information-flow variants.

HyperLTL cannot specify most two-state independence variants.

Introduces a new approach for proving inexpressiveness of logics like HyperLTL.

Abstract

Information-flow policies prescribe which information is available to a given user or subsystem. We study the problem of specifying such properties in reactive systems, which may require dynamic changes in information-flow restrictions between their states. We formalize several flavours of sequential information-flow, which cover different assumptions about the semantic relation between multiple observations of a system. Information-flow specification falls into the category of hyperproperties. We define different variants of sequential information-flow specification using a first-order logic with both trace quantifiers and temporal quantifiers called Hypertrace Logic. We prove that HyperLTL, equivalent to a subset of Hypertrace Logic with restricted quantifier prefixes, cannot specify the majority of the studied two-state independence variants. For our results, we introduce a notion of equivalence between sets of traces that cannot be distinguished by certain classes of formulas in Hypertrace Logic. This presents a new approach to proving inexpressiveness results for logics such as HyperLTL.