Reactive noninterference

12 years 16 hour ago
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.
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sj&oum
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where CCS
Authors Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic
Comments (0)