Compositional Information-Flow Security for Interactive Systems
Compositional Information-Flow Security for Interactive Systems
复制标题
交互式系统的组合信息流安全
DOI：
10.1109/csf.2014.27
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
A. Sabelfeld
中科院分区：
文献类型：
--
作者：
Willard Rafnsson;A. Sabelfeld
为了在由零件构建的系统中实现端到端的安全性，重要的是要确保安全组件的组成本身是安全的。这项工作研究了两种流行的可能性非干预条件的组成性。第一个条件是不敏感的非干扰（PINI），是由JSFLOW，PARAGAR，顺序LIO，JIF，FLOW CAML和SPARK Execiner等实用工具强制执行的安全条件。我们表明，这种条件在公平的并行组成下没有保留：与另一个PINI系统合理组成PINI系统可以产生不安全的系统。我们探索允许恢复PINI组成的约束。此外，我们发展了组成推理的理论。与PIN相比，我们显示了PSNI在组成下的表现，没有公平性假设。我们的工作是在非确定交互式系统的一般框架内进行的。
To achieve end-to-end security in a system built from parts, it is important to ensure that the composition of secure components is itself secure. This work investigates the compositionality of two popular conditions of possibilistic noninterference. The first condition, progress-insensitive noninterference (PINI), is the security condition enforced by practical tools like JSFlow, Paragon, sequential LIO, Jif, Flow Caml, and SPARK Examiner. We show that this condition is not preserved under fair parallel composition: composing a PINI system fairly with another PINI system can yield an insecure system. We explore constraints that allow recovering compositionality for PINI. Further, we develop a theory of compositional reasoning. In contrast to PINI, we show what PSNI behaves well under composition, with and without fairness assumptions. Our work is performed within a general framework for nondeterministic interactive systems.