Encoding information flow in Haskell
Encoding information flow in Haskell
复制标题
Haskell 中的信息流编码
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Steve Zdancewic
中科院分区：
文献类型：
--
作者：
Peng Li;Steve Zdancewic
本文提出了一种嵌入式安全子语言，用于在标准 Haskell 编程语言中实施信息流策略。该子语言提供了有用的信息流控制机制，包括动态安全网格、运行时代码特权和解密，而无需修改基本语言。这种设计避免了产生新语言的冗余工作，降低了采用安全类型语言的门槛，也为安全策略框架的使用提供了极大的灵活性和模块化性。嵌入式安全子语言是使用称为箭头的标准组合器接口设计的。用子语言构建的计算具有静态和显式的控制流组件，使得可以在运行时使用静态分析技术实现信息流控制，同时提供强大的安全保证。本文介绍了具体的 Haskell 实现和演示所提出技术的示例应用程序
This paper presents an embedded security sublanguage for enforcing information-flow policies in the standard Haskell programming language. The sublanguage provides useful information-flow control mechanisms including dynamic security lattices, run-time code privileges and declassification, without modifying the base language. This design avoids the redundant work of producing new languages, lowers the threshold for adopting security-typed languages, and also provides great flexibility and modularity for using security-policy frameworks. The embedded security sublanguage is designed using a standard combinator interface called arrows. Computations constructed in the sublanguage have static and explicit control-flow components, making it possible to implement information-flow control using static-analysis techniques at run time, while providing strong security guarantees. This paper presents a concrete Haskell implementation and an example application demonstrating the proposed techniques