A formal framework for real-time information flow analysis

We view Multi-Level Secure (MLS) real-time systems as systems in which MLS real-time tasks are scheduled and execute, according to a scheduling algorithm employed by the system. From this perspective, we develop a general trace-based framework that can carry out a covert-timing channel analysis of a real-time system. In addition, we propose a set of covert-timing channel free policies: If a system satisfies one of our proposed security policies, we demonstrated that the system can achieve a certain level of real-time information flow security. Finally, we compare the relative strength of the proposed covert-timing channel free security policies and analyze whether each security policy can be regarded as a property (a set of execution sequences).