Real Time Information Flow Analysis

In previous work, we have studied some non-interference properties
for information flow analysis in computer systems on classic
(possibilistic) labeled transition systems. In this paper, some of
these properties, notably BNDC, are reformulated in a
real-time setting. This is done by first enhancing the Security
Process Algebra 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.