Information Flow in Systems with Schedulers

The focus of work on information flow security has primarily been on definitions of security in asynchronous systems models. This paper considers systems with schedulers, which require synchronous variants of these definitions. In particular, it studies the dependence of these variant definitions of security on implementation details of the scheduler. Such independence is shown to hold for synchronous variants of trace-based definitions, but not for bisimulation-based definitions. Stronger versions of the bisimulation-based definitions are proposed that recover implementation-independence.