Real-Time Information Flow Analysis

In previous work, we studied some noninterference properties for information flow analysis in computer systems on classic (possibilistic) labeled transition systems. In this paper, some of these properties, notably bisimulation-based nondeducibility on compositions (BNDC), are reformulated in a real-time setting. This is done by first enhancing the security process algebra proposed by two of the authors with some extra constructs to model real-time systems (in a discrete time setting), and then by studying the natural extension of these properties in this enriched setting. We prove essentially the same results known for the untimed case: ordering relation among properties, compositionality aspects, partial model checking techniques. Finally, we illustrate the approach through two case studies, where in both cases the untimed specification is secure, while the timed specification may show up interesting timing covert channels.