Flow Locks: Towards a Core Calculus for Dynamic Flow Policies
Flow Locks: Towards a Core Calculus for Dynamic Flow Policies
复制标题
流锁：走向动态流策略的核心演算
DOI：
10.1007/11693024_13
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
David Sands
中科院分区：
文献类型：
--
作者：
Niklas Broberg;David Sands
安全很少是静态概念。被认为是机密或不受信任的数据随时间而变化的，根据不断变化的事件和状态。安全信息流的静态验证在最近的编程语言研究中一直是一个流行的主题，但是所考虑的信息流策略是基于多级安全性的，该安全性呈现了安全级别的静态视图。在本文中，我们引入了一种非常简单的机制，用于指定动态信息流策略，流量锁，该机制指定了某个参与者可以读取数据的条件。策略和代码之间的接口是通过打开和关闭流量锁的说明。我们提供了类型和效果系统的类型和类似于ML的语言，其引用允许完全静态的流锁策略验证，并证明该系统满足语义安全性属性的概括性。我们表明，这种简单的机制可以代表许多最近提出的信息流范式进行解密。
Security is rarely a static notion. What is considered to be confidential or untrusted data varies over time according to changing events and states. The static verification of secure information flow has been a popular theme in recent programming language research, but information flow policies considered are based on multilevel security which presents a static view of security levels. In this paper we introduce a very simple mechanism for specifying dynamic information flow policies, flow locks, which specify conditions under which data may be read by a certain actor. The interface between the policy and the code is via instructions which open and close flow locks. We present a type and effect system for an ML-like language with references which permits the completely static verification of flow lock policies, and prove that the system satisfies a semantic security property generalising noninterference. We show that this simple mechanism can represent a number of recently proposed information flow paradigms for declassification.