Gradual Security Typing with References
Gradual Security Typing with References
复制标题
带参考的渐进安全打字
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Peter Thiemann
中科院分区：
文献类型：
--
作者：
L. Fennell;Peter Thiemann
用于信息流控制（IFC）的类型系统通常不灵活且过于保守。另一方面，信息流的动态运行时监视是灵活的和宽松的，但是很难保证程序的鲁棒行为。 IFC的逐渐键入使程序员可以在需要的情况下进行允许的动态检查与可预测的保守静态类型系统之间的选择。我们提出了ML-GS，这是一种单态ML核心语言，具有引用和高阶功能，可实现IFC的逐渐键入。该语言包含安全性铸件，使程序员能够在静态检查和动态检查之间来回过渡。特别是，ML-GS可以在参考类型上启用非平凡的演员阵容，以便可以在程序中在程序中到处安全地使用参考，无论它是在程序的动态还是静态检查的一部分中创建。该参考可以在动态和静态检查的零件之间共享。我们证明了逐渐安全类型系统的合理性以及终止不敏感的非干预。
Type systems for information-flow control (IFC) are often inflexible and too conservative. On the other hand, dynamic run-time monitoring of information flow is flexible and permissive but it is difficult to guarantee robust behavior of a program. Gradual typing for IFC enables the programmer to choose between permissive dynamic checking and a predictable, conservative static type system, where needed. We propose ML-GS, a monomorphic ML core language with references and higher-order functions that implements gradual typing for IFC. This language contains security casts, which enable the programmer to transition back and forth between static and dynamic checking. In particular, ML-GS enables non-trivial casts on reference types so that a reference can be safely used everywhere in a program regardless of whether it was created in a dynamically or statically checked part of the program. The reference can be shared between dynamically and statically checked parts. We prove the soundness of the gradual security type system along with termination insensitive non-interference.
DOI：
10.1145/1111037.1111045
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
Sebastian Hunt;David Sands