Apr 6, 2014
Ilaria Castellani: Secure information flow for synchronous reactive programs
We consider the security property of noninterference in a core synchronous reactive language that we call CRL. In the synchronous reactive paradigm, threads communicate by means of broadcast events, and their parallel execution is regulated by a notion of instant. Threads get suspended while waiting for an absent event or when deliberately releasing the control for the current instant. An instant is a period of time during which all threads compute up to termination or suspension. A program interacts with its environment only at the start and the end of instants.
?
We define two bisimulation equivalences on CRL programs, corresponding respectively to a fine-grained and to a coarse-grained observation of programs. Based on these bisimulations, two properties of Reactive Noninterference (RNI) are introduced, formalising secure information flow. Both RNI properties are clock-sensitive (events are observed with their clock-stamp, i.e. the instant in which they are produced) and termination-insensitive.?Coarse-grained RNI is more abstract than fine-grained RNI in that it ignores the order of generation of events and repeated emissions of the same event within an instant.
?
We present a type system guaranteeing both security properties. Thanks to some design choices of CRL and to specific typing rules for conditionals, this type system allows for a precise treatment of termination leaks, which are an issue in parallel languages.
?
Finally, we try to draw some analogies between the behaviour of synchronous programs within instants and that of pi-calculus processes within sessions.