Information flow in systems with schedulers, Part I: Definitions

This paper studies information flow security in a synchronous state machine model, in which agents share a global clock and can make observations at all times, but in which an agent’s ability to perform actions is subject to a scheduler. A number of definitions of security for this setting are proposed, depending on whether the attacker is active or passive, whether the security should be robust to discovery of the schedule by the attacker, and on whether the definition is trace-based or bisimulation-based. In particular, the paper studies the dependence of these definitions of security on implementation details of the scheduler. Such independence is shown to hold for the trace-based definitions, but not for bisimulation-based definitions. Stronger versions of the bisimulation-based definitions are proposed that recover implementation-independence. A complete characterization of relationships between the definitions of security introduced in the paper is derived.