Abstract:
We study the security property of noninterference for a class of
synchronous programs called reactive programs. We consider a
core reactive language, obtained by extending the imperative language
of Volpano, Smith and Irvine with a form of scheduled parallelism and
with reactive primitives that manipulate broadcast signals. The
definition of noninterference has to be tuned to the particular nature
of reactive computations, which are regulated by a notion of instant.
Moreover, a new form of covert channel may arise in reactive
computations, called suspension leak. We give a formulation of
noninterference based on bisimulation, as is now usual for concurrent
languages. We then propose a type system to enforce this property in
our language. Our type system is inspired by that introduced by
Boudol and Castellani, and independently by Smith, for a parallel
language with scheduling. We establish the soundness of our type
system with respect to our new notion of noninterference. We finally
show that this notion of noninterference refines in several aspects
the standard one for imperative languages.