基于模型检测的Hyper-V虚拟机监控器的安全性分析
本文关键词：基于模型检测的Hyper-V虚拟机监控器的安全性分析 出处：《西安电子科技大学》2015年硕士论文 论文类型：学位论文
【摘要】：在不久的未来,云计算很快就会席卷IT领域,而虚拟机监控器是所有虚拟化技术活的核心。云计算本质的复杂性和动态性使得传统的、以及基于虚拟化的防御技术很难达到有效的防御效果。为了保证云计算的安全,分析虚拟机监控器自身的安全性、找出软件本身存在漏洞是解决其安全问题的根本办法。为了尽量多的找出虚拟机监控器存在的安全漏洞,对系统脆弱性的分析应在各个抽象层次上进行。所以,我们可以使用形式化分析方法中的模型检测理论进行漏洞挖掘。利用现有的形式化代码分析技术来分析虚拟机监控器的脆弱性时主要存在以下问题：1.只证明了代码的正确性,而不能证明安全性,如在已知Hyper-V源码的基础上利用模型检测方法验证其正确性的工具VCC。一些针对代码层的可信静态分析工具可以检验数据结构行为和同步问题等,但是在进行检测时没有考虑软件的安全性。2.只针对开源的虚拟机监控器。一些研究方法试图形式化的捕获代码意图,并将安全性考虑在内,但是这种方法对于不开源的软件比如微软的虚拟机监控器Hyper-V是不可行的。本文使用模型检测的方法来进行基于Hyper-V的虚拟机监控器的漏洞分析。本研究遵循的流程是：抽象-建模-描述-验证。主要工作如下：1.分析了Hyper-V的基本架构。本文详细研究了微软的虚拟化技术及其架构,分析了Hyper-V的安全特性。将敏感指令、特权指令、CPU的状态及状态转移进行了分级和分类,定义不同主体的可执行指令,构建了CPU简单的三个状态的状态转移图。2.构建Hyper-V CPU的安全参考模型。形式化的定义了Hyper-V的各个主体,使用Promela和SPIN得到了CPU状态的有限状态模型,有限状态模型包括的主体有VMM, VMPP以及两个VMCP等。在有限状态模型的基础上,结合用LTL所定义的安全断言,构建了Hyper-V CPU的安全参考模型。3.构建Hyper-V内存的安全参考模型。描述了虚拟内存到物理内存的映射及其关系,将物理内存划分为三个不同的等级,并为不同的主体定义不同的内存访问权限。根据主体的形式化定义以及有限状态模型,从主体中抽象出相关内存的属性。形式化的描述主体,并建造内存的有限状态模型。最终根据内存的转移规则以及内存状态的有限状态模型,利用SPIN得到内存访问的安全参考模型。4. 构建多任务的CPU安全参考模型。对于DoS攻击,根据Hyper-V的架构以及调度机制的特点构建针对多任务的CPU安全参考模型。该模型可以用来抽象超级调用的相关代码,减少代码分析的工作量。针对CPU的安全参考模型、内存的安全参考模型以及多任务的CPU的安全参考模型为进一步检测Hyper-V代码的安全性奠定了基础。
【学位授予单位】：西安电子科技大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP302;TP309
【相似文献】
相关期刊论文 前10条
1 曹晓刚;;Java虚拟机的10年[J];程序员;2005年07期
2 宋韬;盘细平;罗元柯;倪国军;;Java虚拟机在嵌入式DSP系统上的实现[J];计算机应用与软件;2007年04期
3 刘黎波;;Java虚拟机拦截原理研究[J];科技风;2008年21期
4 刘治波;;Java虚拟机简析[J];济南职业学院学报;2008年01期
5 郝帅;;Java虚拟机中相关技术的探讨[J];成功(教育);2008年08期
6 李霞;;系统虚拟机关键技术研究[J];微型电脑应用;2010年03期
7 郑晓珑;孔挺;;虚拟机的安全风险与管理[J];硅谷;2010年16期
8 李学昌;平淡;;为速度而战,虚拟机内外兼修[J];电脑爱好者;2010年18期
9 王惠萍;张海龙;冯帆;王建华;;Java虚拟机使用及优化[J];计算机与网络;2010年21期
10 郑婷婷;武延军;贺也平;;云计算环境下的虚拟机快速克隆技术[J];计算机工程与应用;2011年13期
相关会议论文 前10条
1 孟广平;;虚拟机漂移网络连接方法探讨[A];中国计量协会冶金分会2011年会论文集[C];2011年
2 段翼真;王晓程;;可信安全虚拟机平台的研究[A];第26次全国计算机安全学术交流会论文集[C];2011年
3 李明宇;张倩;吕品;;网络流量感知的虚拟机高可用动态部署研究[A];2014第二届中国指挥控制大会论文集（上）[C];2014年
4 林红;;Java虚拟机面向数字媒体的应用研究[A];计算机技术与应用进展——全国第17届计算机科学与技术应用（CACIS）学术会议论文集（上册）[C];2006年
5 杨旭;彭一明;刑承杰;李若淼;;基于VMware vSphere 5虚拟机的备份系统实现[A];中国高等教育学会教育信息化分会第十二次学术年会论文集[C];2014年
6 沈敏虎;查德平;刘百祥;赵泽宇;;虚拟机网络部署与管理研究[A];中国高等教育学会教育信息化分会第十次学术年会论文集[C];2010年
7 李英壮;廖培腾;孙梦;李先毅;;基于云计算的数据中心虚拟机管理平台的设计[A];中国高等教育学会教育信息化分会第十次学术年会论文集[C];2010年
8 朱欣焰;苏科华;毛继国;龚健雅;;GIS符号虚拟机及实现方法研究[A];《测绘通报》测绘科学前沿技术论坛摘要集[C];2008年
9 于洋;陈晓东;俞承芳;李旦;;基于FPGA平台的虚拟机建模与仿真[A];2007'仪表，，自动化及先进集成技术大会论文集（一）[C];2007年
10 丁涛;郝沁汾;张冰;;内核虚拟机调度策略的研究与分析[A];'2010系统仿真技术及其应用学术会议论文集[C];2010年
相关重要报纸文章 前10条
1 ;虚拟机的生与死[N];网络世界;2008年
2 本报记者 卜娜;高性能Java虚拟机将在中国云市场释能[N];中国计算机报;2012年
3 本报记者 邱燕娜;如何告别虚拟机管理烦恼[N];中国计算机报;2012年
4 ;首批通过云计算产品虚拟机管理测评名单[N];中国电子报;2014年
5 申琳;虚拟机泛滥 系统安全怎么办[N];中国计算机报;2008年
6 Tom Henderson邋沈建苗 编译;虚拟机管理的五大问题[N];计算机世界;2008年
7 盆盆;真实的虚拟机[N];中国电脑教育报;2004年
8 本版编辑 综合 编译整理 田梦;管理好虚拟机的全生命周期[N];计算机世界;2008年
9 李婷;中国研制出全球最快反病毒虚拟机[N];人民邮电;2009年
10 张弛;虚拟机迁移走向真正自由[N];网络世界;2010年
相关博士学位论文 前10条
1 宋翔;多核虚拟环境的性能及可伸缩性研究[D];复旦大学;2014年
2 王桂平;云环境下面向可信的虚拟机异常检测关键技术研究[D];重庆大学;2015年
3 周真;云平台下运行环境感知的虚拟机异常检测策略及算法研究[D];重庆大学;2015年
4 郭芬;面向虚拟机的云平台资源部署与调度研究[D];华南理工大学;2015年
5 周傲;高可靠云服务供应关键技术研究[D];北京邮电大学;2015年
6 陈彬;分布环境下虚拟机按需部署关键技术研究[D];国防科学技术大学;2010年
7 刘海坤;虚拟机在线迁移性能优化关键技术研究[D];华中科技大学;2012年
8 刘谦;面向云计算的虚拟机系统安全研究[D];上海交通大学;2012年
9 赵佳;虚拟机动态迁移的关键问题研究[D];吉林大学;2013年
10 邓莉;基于虚拟机迁移的动态资源配置研究[D];华中科技大学;2013年
相关硕士学位论文 前10条
1 潘飞;负载相关的虚拟机放置策略研究[D];杭州电子科技大学;2011年
2 王建一;混合型桌面云高可用性研究与实现[D];华南理工大学;2015年
3 周衡;云计算环境下虚拟机优化调度策略研究[D];河北大学;2015年
4 罗仲皓;基于OpenStack的私有云计算平台的设计与实现[D];华南理工大学;2015年
5 李子堂;面向负载均衡的虚拟机动态迁移优化研究[D];辽宁大学;2015年
6 张煜;基于OpenStack的“实验云”平台的研究与开发[D];西南交通大学;2015年
7 曾文琦;面向应用服务的云规模虚似机性能监控与负载分析技术研究[D];复旦大学;2013年
8 施继成;面向多核处理器的虚拟机性能优化[D];复旦大学;2014年
9 游井辉;基于虚拟机动态迁移的资源调度策略研究[D];华南理工大学;2015年
10 方良英;云平台的资源优化管理研究与实现[D];南京师范大学;2015年
本文编号：1324185
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/1324185.html
