基于政策的自主管理系统的形式化分析研究

摘要

计算机系统的复杂性不仅使其分析与开发困难,而且同样使其管理面临挑战。为解决复杂系统管理面临的问题,具有一定程度智能性的自主管理系统正成为研究的热点。在自主管理系统的实际开发之前,采用形式化方法对系统进行分析和验证不仅有助于构造正确可靠的计算机系统,还能够降低开发和维护的成本,并为系统的实际开发提供理论支持。
　　自主管理主要包括四个方面的内容:自配置、自恢复、自优化和自保护。本文采用形式化方法围绕自主管理中的自配置方面展开研究。在研究基于政策的自配置系统框架的基础上,提出采用着色 Petri网对此类系统进行建模、分析与验证,保证所开发自配置系统的正确性。为了描述系统配置过程中具备的性质,采用 CTL的扩展——ASK-CTL,并使用CPN Tools2.2.0进行仿真与验证。
　　在基于政策的自配置系统中,政策决策点(Policy Decision Point, PDP)和政策执行点(Policy Enforcement Point, PEP)是两个核心部件。COPS(Common Open Policy Service)协议是这两个部件间使用的信息交换协议,是基于政策的自主管理体系中不可缺少的一部分。此类系统中,政策消息的安全传输关系到整个系统的正确运行,这使其比一般的数据信息更为重要。鉴于COPS协议的重要性,在对其进行非形式化分析的基础上,针对协议的安全机制,构造该协议的着色Petri网模型并对其进行仿真,验证了该协议的安全性。最后通过模拟网络传输中出现的入侵行为,分析了入侵行为导致的结果,发现COPS协议存在的安全缺陷,为进一步完善该协议提供了根据。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1.1 课题研究的背景及意义

§1.2 国内外研究现状

§1.3 论文的工作

§1.4 论文的组织结构

第二章 基于政策的自配置系统的体系结构

§2.1 政策的概念

§2.2基于政策的自配置系统框架的设计

§2.3 COPS协议

§2.4 小结

第三章 形式化分析的基础理论

§3.1 Petri网的定义

§3.2 着色Petri网

§3.3 CPN Tools简介

§3.4 ASK-CTL逻辑

§3.5 小结

第四章 基于政策的自配置系统建模

§4.1 基于政策的自配置系统模型的层次结构

§4.2 系统模型的全局声明

§4.3 系统模型的顶层页

§4.4 PMT页

§4.5 PDP页

§4.6 PEP页

§4.7 Monitor页

§4.8 小结

第五章 基于政策的自配置系统模型的仿真与分析验证

§5.1 仿真实例

§5.2 仿真结果的分析与验证

§5.3 小结

第六章 COPS协议建模

§6.1 COPS协议模型的层次结构及声明

§6.2 COPS协议模型的顶层页

§6.3 PEP页

§6.4 Network页

§6.5 PDP页

§6.6 小结

第七章 COPS协议模型的仿真与分析验证

§7.1 仿真实例

§7.2 仿真结果与分析

§7.3 COPS协议的安全缺陷

§7.4 小结

第八章 结束语

致谢

参考文献

附录

攻读硕士学位期间的研究成果