动态策略的强静态实施
密码学与安全
2015-01-13 v1 编程语言
摘要
安全策略本质上是动态的。反映这一点，研究程序执行期间变化的信息流属性（包括如去分类、撤销和角色变更等概念）的兴趣日益增长。从语义角度看，动态信息流策略的静态验证只需关注两件事：1) 程序中数据之间的依赖关系，2) 这些依赖关系是否随时间变化与预期的流策略一致。本文为这一直觉提供了形式化基础。我们提出了对Hunt和Sands（POPL '06, ESOP '11）引入的主流感敏感类型系统的一个直接扩展，以推断程序中的端到端依赖关系以及中间点的依赖关系。这使得类型指派可应用于静态和动态策略的验证。我们的扩展保留了该主类型系统的显著特征，即类型推断独立于要实施的策略：单一的通用依赖分析（类型指派）可用于验证给定程序的许多不同动态策略，从而在(1)和(2)之间实现清晰分离。我们还对动态信息流的基础做出了贡献。可以说，文献中对动态安全条件最具说服力的语义定义是以所谓基于知识的风格表述的。我们提出了一种针对动态策略的基于知识的终止不敏感安全性的新定义。我们展示了新定义避免了先前定义的异常，并享有作为双运行风格属性的简单而有用的刻画。
引用
@article{arxiv.1501.02633,
title = {Very Static Enforcement of Dynamic Policies},
author = {Bart van Delft and Sebastian Hunt and David Sands},
journal= {arXiv preprint arXiv:1501.02633},
year = {2015}
}
备注
Technical Report of publication under the same name in Principles of Security and Trust (POST) 2015