Verification of Information Flow Properties under Rational Observation

TL;DR

This paper introduces rational information flow properties (RIFP) to analyze what an observer can infer about secret behaviors in systems, providing a general framework with decidability results for regular languages.

Contribution

It defines RIFPs using finite transducers, establishes a general decidability criterion, and unifies existing trace-based properties under this framework.

Findings

Decidability of RIFPs on regular languages is PSPACE-complete.

Most trace-based information flow properties are RIFPs.

The framework recovers several existing decidability results.

Abstract

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.