A derivation framework for dependent security label inference
A derivation framework for dependent security label inference
复制标题
DOI：
10.1145/3276485
复制
发表时间：
2018-10
影响因子：
--
通讯作者：
Peixuan Li;Danfeng Zhang
中科院分区：
文献类型：
--
作者：
Peixuan Li;Danfeng Zhang
已经引入了各种形式的依赖安全标签（依赖程序状态的安全标签），以表达丰富的信息流策略。它们被证明是对现实世界软件和硬件系统的验证，例如会议管理系统，Android应用，MIPS处理器和类似Trustzone的体系结构。但是，大多数工作都假定所有（复杂）标签都是手动提供的，这既容易出错，又可能耗时。在本文中，我们解决了具有依赖安全标签的静态信息流量分析的自动标签推断问题。特别是，我们提出了第一个通用框架，以促进推理算法的设计和验证（就合理性和/或完整性而言）。框架模型将推理标记为解决方案，并为声音和/或完整约束解决方案提供指南。在框架下，我们提出了新的约束算法，这些算法既声音又完整。评估结果是由MIPS处理器的安全和不安全变体产生的一组约束，这表明新算法通过数量级来改善现有算法的性能，并提供更好的可伸缩性。
Dependent security labels (security labels that depend on program states) in various forms have been introduced to express rich information flow policies. They are shown to be essential in the verification of real-world software and hardware systems such as conference management systems, Android Apps, a MIPS processor and a TrustZone-like architecture. However, most work assumes that all (complex) labels are provided manually, which can both be error-prone and time-consuming. In this paper, we tackle the problem of automatic label inference for static information flow analyses with dependent security labels. In particular, we propose the first general framework to facilitate the design and validation (in terms of soundness and/or completeness) of inference algorithms. The framework models label inference as constraint solving and offers guidelines for sound and/or complete constraint solving. Under the framework, we propose novel constraint solving algorithms that are both sound and complete. Evaluation result on sets of constraints generated from secure and insecure variants of a MIPS processor suggests that the novel algorithms improve the performance of an existing algorithm by orders of magnitude and offers better scalability.