Securing Interactive Programs
Securing Interactive Programs
复制标题
确保交互式程序的安全
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
A. Sabelfeld
中科院分区：
文献类型：
--
作者：
Willard Rafnsson;Daniel Hedin;A. Sabelfeld
本文研究了交互式程序信息流安全的基础。先前的研究假设环境是整体的，也就是说，它必须随时准备向程序提供新的输入。然而，在这种假设下安全的程序可能会泄漏输入的存在。在并发设置中，这种泄漏可以被放大为完全保密的泄漏。我们提出了一个框架，它从两个方面概括了以前的研究：首先，该框架脱离了环境的整体，其次，该框架具有通信通道的细粒度安全类型，其中我们区分了消息存在和消息内容的安全级别。我们证明了广义框架具有吸引人的组合性特性：安全程序的并行组合导致安全线程池。我们还表明，将环境建模为策略会导致强大的组合性：各种类型的组合（有或没有作用域）遵循我们的一般组合性结果。此外，我们提出了一种类型系统，该系统支持通过细粒度安全类型实施安全性。
This paper studies the foundations of information-flow security for interactive programs. Previous research assumes that the environment is total, that is, it must always be ready to feed new inputs into programs. However, programs secure under this assumption can leak the presence of input. Such leaks can be magnified to whole-secret leaks in the concurrent setting. We propose a framework that generalizes previous research along two dimensions: first, the framework breaks away from the totality of the environment and, second, the framework features fine-grained security types for communication channels, where we distinguish between the security level of message presence and message content. We show that the generalized framework features appealing compositionality properties: parallel composition of secure program results in a secure thread pool. We also show that modeling environments as strategies leads to strong compositionality: various types of composition (with and without scoping) follow from our general compositionality result. Further, we propose a type system that supports enforcement of security via fine-grained security types.