Fine-grained and coarse-grained reactive noninterference

Abstract

We study bisimilarity and the security property of noninterference in a core synchronous reactive language that we name. In the synchronous reactive paradigm, programs communicate by means of broadcast events, and their parallel execution is regulated by the notion of instant. Within each instant, programs may emit events and get suspended while waiting for events emitted by other programs. They may also explicitly return the control to the scheduler, thereby suspending themselves until the end of the instant. An instant is thus a period of time during which all programs compute until termination or suspension. In there is no memory, and the focus is on the control structure of programs. An asymmetric parallel operator is used to implement a deterministic scheduling. This scheduling is fair - in the sense that it gives its turn to each parallel component - if all components are cooperative, namely if they always return the control after a finite number of steps. We first prove that programs are indeed cooperative. This result is based on two features of the language: the semantics of loops, which requires them to yield the control at each iteration of their body; and a delayed reaction to the absence of events, which ensures the monotonicity of computations (viewed as I/O functions on event sets) during instants. Cooperativeness is crucial as it entails the reactivity of a program to its context, namely its capacity to input events from the context at the start of instants, and to output events to the context at the end of instants. We define two bisimulation equivalences on programs, formalising respectively a fine-grained observation of programs (the observer is viewed as a program) and a coarse-grained observation (the observer is viewed as part of the context). As expected, the latter equivalence is more abstract than the former, as it only compares the I/O behaviours of programs at each instant, while the former also compares their intermediate results. Based on these bisimulations, two properties of reactive noninterference (RNI) are proposed. Both properties are time-insensitive and termination-insensitive. Coarse-grained RNI is more abstract than fine-grained RNI, because it views the parallel operator as commutative and abstracts away from repeated emissions of the same event during an instant. Finally, a type system guaranteeing both security properties is presented. Thanks partly to a design choice of, which offers two separate constructs for loops and iteration, this type system allows for a precise treatment of termination leaks, which are an issue in parallel languages. © Springer International Publishing Switzerland 2014.