Analysis for Real-time Intransitive Information Flow Security Properties

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.