Flavours of Sequential Information Flow
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.
Cite
@article{arxiv.2105.02013,
title = {Flavours of Sequential Information Flow},
author = {Ezio Bartocci and Thomas Ferrère and Thomas A. Henzinger and Dejan Nickovic and Ana Oliveira da Costa},
journal= {arXiv preprint arXiv:2105.02013},
year = {2021}
}