Types for Information Flow Control: Labeling Granularity and Semantic Models
Types for Information Flow Control: Labeling Granularity and Semantic Models
复制标题
信息流控制的类型：标记粒度和语义模型
DOI：
10.1109/csf.2018.00024
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Deepak Garg
中科院分区：
文献类型：
--
作者：
Vineet Rajani;Deepak Garg
基于秘密的信息流控制（IFC）使用敏感性标签跟踪程序内的依赖关系，并禁止公共输出依赖于秘密输入。特别是，文献已经提出了几种类型的系统来跟踪这些依赖关系。在一个极端，有细粒度的类型系统（如Flow Caml），它们单独标记所有值，并在单个值的级别上跟踪依赖性。另一个极端是粗粒度类型系统（如HLIO），它通过将单个标签与整个计算上下文相关联而不是单独标记所有值来粗略地跟踪依赖关系。在本文中，我们表明，尽管它们有明显的差异，这两种风格，事实上，同样的表现力。为此，我们展示了从粗粒度类型系统到细粒度类型系统的语义和类型保持翻译，反之亦然。正向转换并不奇怪，但反向转换是：它需要一个构造来任意限制粗粒度类型系统中上下文标签的范围（例如，HLIO的"toLabeled"结构）。作为一个单独的贡献，我们展示了如何扩展工作的IFC类型的逻辑关系模型，以高阶状态。我们为细粒度类型系统和粗粒度类型系统都建立了这样的逻辑关系。我们使用这些关系来证明这两个类型系统和我们的翻译之间的声音。
Language-based information flow control (IFC) tracks dependencies within a program using sensitivity labels and prohibits public outputs from depending on secret inputs. In particular, literature has proposed several type systems for tracking these dependencies. On one extreme, there are fine-grained type systems (like Flow Caml) that label all values individually and track dependence at the level of individual values. On the other extreme are coarse-grained type systems (like HLIO) that track dependence coarsely, by associating a single label with an entire computation context and not labeling all values individually. In this paper, we show that, despite their glaring differences, both these styles are, in fact, equally expressive. To do this, we show a semantics- and type-preserving translation from a coarse-grained type system to a fine-grained one and vice-versa. The forward translation isn't surprising, but the backward translation is: It requires a construct to arbitrarily limit the scope of a context label in the coarse-grained type system (e.g., HLIO's "toLabeled'' construct). As a separate contribution, we show how to extend work on logical relation models of IFC types to higher-order state. We build such logical relations for both the fine-grained type system and the coarse-grained type system. We use these relations to prove the two type systems and our translations between them sound.
登录
查看更多内容
随控制流变化而增加计算复杂性的类型理论
DOI：
--
发表时间：
2016
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Ezgi Çiçek;Zoe Paraskevopoulou;D. Garg
通讯作者：
D. Garg
DOI：
10.1145/1111037.1111045
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
Sebastian Hunt;David Sands
DOI：
--
发表时间：
2005
期刊：
影响因子：
--
作者：
J. Fiadeiro;U. Montanari;M. Wirsing
通讯作者：
M. Wirsing
许可式动态信息流分析
DOI：
--
发表时间：
2010
期刊：
ACM Workshop on Programming Languages and Analysis for Security
影响因子：
--
作者：
Thomas H. Austin;C. Flanagan
通讯作者：
C. Flanagan
DOI：
--
发表时间：
2017
期刊：
SIGL
影响因子：
--
作者：
Vineet Rajani;Iulia Bastys;Willard Rafnsson;D. Garg
通讯作者：
D. Garg