Skip to main content
Reactive Noninterference
Departmental Papers (CIS)
  • Aaron Bohannon, University of Pennsylvania
  • Benjamin C Pierce, University of Pennsylvania
  • Vilhelm Sjoberg, University of Pennsylvania
  • Stephanie Weirich, University of Pennsylvania
  • Stephan A Zdancewic, University of Pennsylvania
Date of this Version
Document Type
Conference Paper

Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic. Reactive Noninterference. In ACM Computer and Communications Security Conference (CCS), 2009

© ACM, 2009. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Computer and Communications Security Conference , {(2009)}" Email


Many programs operate reactively-patiently waiting for user input, running for a while producing output, and eventually returning to a state where they are ready to accept another input (or occasionally diverging). When a reactive program communicates with multiple parties, we would like to be sure that it can be given secret information by one without leaking it to others. Motivated by web browsers and client-side web applications, we explore definitions of noninterference for reactive programs and identify two of special interest-one corresponding to termination-insensitive noninterference for a simple 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.
Citation Information
Aaron Bohannon, Benjamin C Pierce, Vilhelm Sjoberg, Stephanie Weirich, et al.. "Reactive Noninterference" (2009)
Available at: