Anale: Seria Informatică (Jan 2009)
On Deducible Information Flow in Synchronous Models
Abstract
We revisit the synchronous model of Wittbold and Johnson of information flow, by investigating the relationship between two notions of information flow: a notion based on counting differently-observable high-level strategies and a notion based on the deductions that the low-level user makes on high-level activity while observing system behavior. We then relate our results to some known models of information flow: we show that bisimulation-based equivalence checking is too strong, since it labels variations in the observation due to system nondeterminism as information flow.We also show that a synchronous, trace-based statement of Generalized Noninterference does not properly capture information flow either. Finally we give a decision procedure for detecting information flow for finitestate systems.