ISSN : 1796-217X
Volume : 4    Issue : 1    Date : February 2009

Analysis for Real-time Intransitive Information Flow Security Properties
Yong Huang, Lingdi Ping, Shanping Li, and Xuezeng Pan
Page(s): 90-97
Full Text:
PDF (196 KB)

Real-time information flow security properties such as timed noninterference provide assurances
that some time dependent information flows may not become possible. However, with transitive
noninterference formulation, it is difficult to deal with intransitive flow policies like channel control
and secure downgrading of information with time constraints. In this paper, we introduce the notion
of trust domain into Timed Secure Process Algebra (tSPA), extending intransitive noninterference to
real-time systems. Based on weak timed bisimulation equivalence, some security properties for
intransitive flow are reformulated in a realtime setting, in particular one property which is persistent,
meaning that if a system is secure then all of its reachable states are secure too. Furthermore, we
prove that such persistent intransitive timed property is compositional, which is thus possible to
alleviate the state space explosion problem caused by the interleaving of all the possible
executions of parallel processes. Finally, we provide one case study showing that it is possible to
model and analyze the real-time system through our approach.

Index Terms
real-time information flow, trust domain, intransitive noninterference, timed bisimulation
equivalence, timing covert channels