Verification of Information Flow Properties under Rational Observation
This provides a unified framework for verifying information flow, applicable to problems like selective declassification and conditional anonymity, but is incremental as it builds on existing trace-based properties.
The paper tackles the verification of information flow properties in partially observable systems by defining rational information flow properties (RIFP) with observers modeled as finite transducers, leading to a general decidability criterion and PSPACE-completeness for regular languages.
Information flow properties express the capability for an agent to infer information about secret behaviours of a partially observable system. In a language-theoretic setting, where the system behaviour is described by a language, we define the class of rational information flow properties (RIFP), where observers are modeled by finite transducers, acting on languages in a given family $\mathcal{L}$. This leads to a general decidability criterion for the verification problem of RIFPs on $\mathcal{L}$, implying PSPACE-completeness for this problem on regular languages. We show that most trace-based information flow properties studied up to now are RIFPs, including those related to selective declassification and conditional anonymity. As a consequence, we retrieve several existing decidability results that were obtained by ad-hoc proofs.