存在异常时的灵活动态信息流控制
密码学与安全
2015-03-20 v1 编程语言
摘要
我们描述了一种新的、动态的、浮动标签的语言级信息流控制方法。一个带标签的IO单子LIO跟踪当前标签并限制对IO功能的访问。当前标签浮动以超过所有观察到的数据的标签，并限制可以修改的内容。与其他基于语言的工作不同，LIO还用一个当前许可来限制当前标签，提供了一种形式的自主访问控制。计算可以封装并传递具有不同标签的计算结果。此外，LIO单子提供了简单形式的带标签可变引用和异常处理。我们给出了精确的语义，并证明了按名调用λ演算的机密性和完整性属性，并在Haskell中提供了实现。
引用
@article{arxiv.1207.1457,
title = {Flexible Dynamic Information Flow Control in the Presence of Exceptions},
author = {Deian Stefan and Alejandro Russo and John C. Mitchell and David Mazières},
journal= {arXiv preprint arXiv:1207.1457},
year = {2015}
}