Typing noninterference for reactive programs

摘要

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.