Reconciling noninterference and gradual typing
Reconciling noninterference and gradual typing
复制标题
协调无干扰和渐进打字
DOI：
10.1145/3373718.3394778
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Jia, Limin
中科院分区：
文献类型：
--
作者：
de Amorim, Arthur Azevedo;Fredrikson, Matt;Jia, Limin
渐进类型的标准正确性标准之一是动态渐进保证，它确保程序中的类型注释松动不会以任意方式影响其行为。虽然自然，以前的工作已经指出，保证不持有任何渐进式系统的信息流控制。Toro等人的GSLRef语言，例如，不得不放弃它来验证noninterference.We表明，我们可以解决这个冲突，通过避免以前的建议的一个功能：类型引导分类，或使用类型归属分类数据。渐进式语言需要运行时保密标签来动态地实施安全性;如果类型归属仅仅检查这些标签而不修改它们（即不对数据进行分类），则它不会违反动态渐进式保证。我们用GLIO来证明这一想法，GLIO是一个基于LIO库的渐进类型系统，它强制执行渐进保证和不干扰，具有高阶函数、通用引用、粗粒度信息流控制、安全子类型和一流标签。我们给语言的域理论语义，使用皮茨的关系结构的框架来证明不干涉和动态渐进的保证。
One of the standard correctness criteria for gradual typing is the dynamic gradual guarantee, which ensures that loosening type annotations in a program does not affect its behavior in arbitrary ways. Though natural, prior work has pointed out that the guarantee does not hold of any gradual type system for information-flow control. Toro et al.'s GSLRef language, for example, had to abandon it to validate noninterference.We show that we can solve this conflict by avoiding a feature of prior proposals: type-guided classification, or the use of type ascription to classify data. Gradual languages require run-time secrecy labels to enforce security dynamically; if type ascription merely checks these labels without modifying them (that is, without classifying data), it cannot violate the dynamic gradual guarantee. We demonstrate this idea with GLIO, a gradual type system based on the LIO library that enforces both the gradual guarantee and noninterference, featuring higher-order functions, general references, coarsegrained information-flow control, security subtyping and first-class labels. We give the language a domain-theoretic semantics, using Pitts' framework of relational structures to prove noninterference and the dynamic gradual guarantee.
登录
查看更多内容
带参考的渐进安全打字
DOI：
--
发表时间：
2013
期刊：
IEEE Computer Security Foundations Symposium
影响因子：
--
作者：
L. Fennell;Peter Thiemann
通讯作者：
Peter Thiemann
信息流控制的类型：标记粒度和语义模型
DOI：
10.1109/csf.2018.00024
发表时间：
2018
期刊：
2018 IEEE 31st Computer Security Foundations Symposium (CSF)
影响因子：
--
作者：
Vineet Rajani;Deepak Garg
通讯作者：
Deepak Garg
DOI：
10.1007/978-3-540-73589-2_2
发表时间：
2007-07
期刊：
--
影响因子：
--
作者：
Jeremy G. Siek;Walid Taha
通讯作者：
Jeremy G. Siek;Walid Taha
经过验证的信息流架构
DOI：
10.1145/2535838.2535839
发表时间：
2014
期刊：
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Arthur Azevedo de Amorim;Nathan Collins;A. DeHon;Delphine Demange;Cătălin Hriţcu;David Pichardie;B. Pierce;R. Pollack;A. Tolmach
通讯作者：
A. Tolmach
抽象渐进式打字
DOI：
--
发表时间：
2016
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Ronald Garcia;Alison M. Clark;É. Tanter
通讯作者：
É. Tanter