Reactive noninterference

Many programs operate reactively, patiently waiting for user input, subsequently running for a while producing output, and eventually returning to a state where they are ready to accept another input (or perhaps diverging). When a reactive program communicates with multiple parties, we would like to be sure that it can be given secret information from one without leaking it to others. In this paper, we explore various definitions of noninterference for reactive programs and identify two of special interest—one corresponding to terminationinsensitive noninterference for a standard sequential language, the other to termination-sensitive noninterference. We focus on the former and develop a proof technique for showing that program behaviors are secure according to this definition. To demonstrate the viability of the approach, we define a simple reactive language with an information-flow type system and apply our proof technique to show that well-typed programs are secure.

• Type: Conference
• Year: 2009
• Where: CCS
• Authors: Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic
• Keywords: CCS 2009, Proof Technique, Reactive Programs, Security Privacy, Simple Reactive Language