Reactive noninterference
Reactive noninterference
复制标题
反应式无干扰
DOI：
10.1145/1653662.1653673
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Steve Zdancewic
中科院分区：
文献类型：
--
作者：
A. Bohannon;B. Pierce;Vilhelm Sjöberg;Stephanie Weirich;Steve Zdancewic
许多程序都是反应性地运行——耐心等待用户输入，运行一段时间产生输出，最终返回到准备接受另一个输入的状态（或偶尔发散）。当反应式程序与多方通信时，我们希望确保一方可以向它提供秘密信息，而不会泄露给其他方。
在网络浏览器和客户端网络应用程序的推动下，我们探索了反应式程序的不干扰定义，并确定了两个特别感兴趣的定义——一个对应于简单顺序语言的终止不敏感不干扰，另一个对应于终止敏感不干扰。我们关注前者并开发一种证明技术来证明根据这个定义程序行为是安全的。为了证明该方法的可行性，我们定义了一种带有信息流类型系统的简单反应式语言，并应用我们的证明技术来证明类型良好的程序是安全的。
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.