面向PaaS云的信息流控制模型及关键技术研究

摘要

PaaS云作为一种重要的云计算模式，通常以可编程容器的形式交付一组软件和基础设施供云租户开发、托管及部署应用程序或服务。PaaS平台自身负责维护资源的动态扩展，可极大降低应用程序的开发成本和开发负担，近年来在谷歌、亚马逊和微软等云巨头的大力推动下迅猛发展，其商业价值也日益凸显。然而，PaaS云在快速发展的同时也面临着无法回避的数据安全和隐私保护问题。首先，用户将数据存储在云端，不再拥有对自己数据的完全控制能力，只能信任云服务商和平台自身的安全机制来提供数据安全保护，而云服务商和PaaS平台的可信性不易评估。同时，为提高应用开发效率，PaaS云应用通常集成了大量第三方组件，但是组件代码本身不可避免地会存在一些缺陷，组件间交互也可能会存在错误配置，进一步增加了应用的脆弱性。此外，PaaS云整合了多种分布式异构资源，为提高资源综合利用率，多租户多用户之间通常共享计算与存储资源，加剧了用户数据被恶意用户非法访问的风险。这些都可能会威胁到整个平台和用户数据的安全，造成隐私数据泄露、平台完整性破坏等严重安全后果。因此，需要对PaaS平台实施以数据为中心的端到端的安全防护，确保即使平台本身或组件存在安全漏洞也不会导致用户隐私信息泄露和完整性破坏。
　　本研究主要内容包括：⑴提出了一个面向PaaS云的分布式信息流控制模型PIFC，实现了以数据为中心的、灵活的、细粒度信息流控制，有效增强了PaaS平台和用户数据的机密性和完整性。现有的云安全模型主要针对IaaS和SaaS的安全需求，不能很好地满足PaaS云环境的分布式、语言级细粒度信息流控制需求。对此，提出了一个面向PaaS的信息流控制模型(Information Flow Control Model for PaaS，PIFC)。该模型将实施IFC的实体与对象关联，实施细粒度的信息流控制；定义了授权实体及其偏序关系，支持实体间特权传递以满足最小权限原则；引入了能力概念，允许授权实体表达并实施独立的安全需求，以实现分布式特权；引入了标签授权约束集，以防止用户利益冲突并支持职责分离。⑵基于SPA语言描述了PIFC模型的形式化规范，提出一种基于SPA进程等价关系的可降级无干扰属性，实现了对PIFC模型的无干扰性质的形式化证明和自动化验证。基于安全进程代数SPA的语法和语义形式化描述了PIFC模型，分析比较并证明了经典无干扰属性的偏序关系，基于进程等价关系提出了可降级的组合不可推断性NDCD，分析并定义了PIFC系统的高级、低级和降级动作集，通过定理归纳证明及工具自动化验证表明了PIFC模型是无干扰安全的。⑶设计了一种基于安全断言的高层策略描述语言，提出了基于遗传算法的PIFC安全标记自动化配置方法，可有效挖掘出满足PaaS云应用系统安全需求的近似最优解方案。PIFC模型可以细粒度地控制信息的访问和传播，但其灵活性也增加了PaaS云策略管理的复杂性。设计了一种基于安全断言的策略描述语言以表达 PaaS平台的安全需求；形式化定义了信息流安全标记挖掘问题，分析并证明了该问题是 NP完全问题；提出了基于遗传算法的标记挖掘近似最优化算法。分析评估了影响算法效率的主要因素，实验结果表明，算法可自动挖掘出满足PaaS云应用系统安全需求的策略配置近似最优解方案。⑷形式化定义了基于计算树时序逻辑CTL的PIFC信息流策略安全性分析问题，提出了基于分支限界和模型检测的两种策略验证方法，可有效验证 PaaS云信息流策略是否一致完备地满足特定安全需求。PaaS云中安全策略的错误配置会造成权限泄露等影响系统安全运行的严重后果。策略的安全性分析判定系统的所有可达状态是否都能保持特定的安全属性，可以验证策略是否一致完备的满足安全需求。形式化定义了基于Kripke结构和计算树时序逻辑的信息流策略安全性分析问题，验证信息流允许、禁止和授权管理三类信息流安全目标。提出了基于分支限界和模型检测的策略验证方法，有效增强了PaaS云中信息流策略的安全性和可靠性。⑸提出了一个面向 PaaS云的信息流控制框架 GIFC，结合了对象级、消息级和SQL级三种控制粒度，实现了PaaS云中用户数据整个生命周期的端到端的信息流跟踪和控制。现有的信息流控制机制存在控制粒度单一、需要修改语言运行时环境等问题。基于PIFC模型，结合最典型的PaaS云平台GAE，提出了一个信息流控制框架GIFC，结合了对象级、消息级和SQL级三种控制粒度。组件内利用Python的装饰器和动态分发机制等高级特性，设计并实现了一个轻量、易用、简洁的Python库LPIFC，可以控制对象的方法调用所涉及实体间的信息交互，避免了传统方式中修改解释器的缺陷；组件间消息代理根据消息安全标记来过滤消息，以此限制组件可以接收的消息集；组件与GAE datastore数据库之间扩展数据模式以支持标记信息的持久化存储。实验表明，多种IFC粒度相结合有效实现了信息流控制精度和运行性能的平衡。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景

1.2 相关研究现状

1.3 研究内容和主要贡献

1.4 本文的结构安排

第二章 面向PaaS云的分布式信息流模型

2.1 PaaS云的信息流及实体分析

2.2 模型要素

2.3 模型规则

2.4 示例及安全性分析

2.5 本章小结

第三章 基于SPA的PIFC无干扰分析与证明

3.1 SPA基础知识

3.2 基于SPA的PIFC系统形式化规范

3.3 PIFC无干扰分析及证明

3.4 本章小结

第四章 基于遗传算法的PIFC安全标记自动化挖掘

4.1 PIFC安全策略语言

4.2 安全标记挖掘问题及复杂度分析

4.3 基于遗传算法的安全标记挖掘问题求解

4.4 实验评估

4.5 本章小结

第五章 PIFC信息流策略安全性分析与形式化验证

5.1 PIFC策略安全性分析问题定义

5.2 PIFC策略安全性分析问题求解

5.3 实验评估

5.4 本章小结

第六章 面向PaaS云的信息流控制框架设计与实现

6.1 GIFC框架设计

6.2 GIFC实现关键技术

6.3 示例分析及性能测试

6.4 本章小结

第七章 结束语

7.1 主要工作总结

7.2 下一步研究方向

致谢

参考文献

作者简历 攻读博士学位期间完成的主要工作