ACRN之InterruptWindow功能正确性形式化验证.doc
《ACRN之InterruptWindow功能正确性形式化验证.doc》由会员分享,可在线阅读,更多相关《ACRN之InterruptWindow功能正确性形式化验证.doc(9页珍藏版)》请在三一文库上搜索。
1、ACRN之InterruptWindow功能正确性形式化验证1.ACRN背景简介ACRN是Linux基金会今年发布的一款新的嵌入式hypervisor参考软件,项目的官方名称为ACRN,这是一个专为物联网和嵌入式设备设计的管理程序。该项目得益于英特尔代码和工程的贡献,其目标是创建一个灵活小巧的虚拟机管理系统。通过基于Linux 的服务操作系统,ACRN 可以同时运行多个客户操作系统,如 Android、其他Linux发行版,或者RTOS,使其成为许多场景的理想选择。ACRN架构如图所示:图1 ACRN架构我们下面需要验证的功能就是ACRN的InterruptWindow功能模型,在验证该模型之
2、前我们需要先进行一下基础知识的培训。2.x86_64架构的InterruptWindow原理介绍Intel InterruptWindow功能是专门为运行在x86_64平台上的虚拟机处理虚拟中断设计的硬件功能,那么为什么要有InterruptWindow功能我们还要从虚拟中断的处理流程开始说起,一般来讲基于x86_64平台物理机中断处理简化流程如下所示:图2 x86_64平台物理机中断处理流程那么现在我们回过头来再看看如果是虚拟机该如何模拟物理机的中断过程,我们说做设计之前一般做法是首先要做几个核心问题的抽象,然后再根据这些问题找到相应的解决方案,最后当问题迎刃而解的时候设计方案也自然水到渠成
3、,相应的我们做虚拟机中断模型分析之前也需要先抛出几个核心问题:运行中的虚拟机如何处理外部中断?外部中断如何注入到虚拟机的中断控制器中?虚拟机的中断控制器何时进行中断的计算与分发?回答一:Intel目前的处理方式分为两种情况考虑:1)外部中断分发到虚拟机正在运行的CPU核,此时硬件会产生一个vm_exit事件让虚拟机暂停运行退出到Hypervisor层进行中断处理;2)外部中断分发到非虚拟机运行的CPU核,此时由Hypervisor层对该中断进行处理。回答二:Intel提供了inject_event方式注入中断,简单说是将需要马上处理的虚拟中断写入到硬件提供VMX内存页的VMX_ENTRY_IN
4、T_INFO_FIELD字段,当系统执行vm_entry指令返回虚拟机运行模式时这个字段会被硬件检测触发中断动作跳转到虚拟机的IDT表执行中断处理。回答三:通过对上述inject_event工作原理的描述,我们可以得出结论虚拟中断的计算与分发需要在Hypervisor层由软件来完成。这样我们就遇到一个问题,假如当前虚拟机处于vm_exit状态,那么可以由软件完成虚拟中断的计算与分发,但是我们考虑一种特殊情况,如果当前vm_exit的虚拟机本身处于关中断状态,那么此时注入虚拟中断返回虚拟机时硬件必然会响应当前的中断,这显然是错误的,因此此时我们只能暂时放弃注入虚拟中断,等到虚拟机打开中断使能状态
5、才能让硬件响应中断,那么这该如何做到呢?Intel提供了一种InterruptWindow机制来解决这个问题,该机制的原理是:配置了InterrruptWindow使能的虚拟机运行阶段当执行STI指令打开中断使能会触发一个vm_exit事件退出到Hypervisor,这个退出原因硬件会标记为InterruptWindow,Hypervisor层会根据这个事件将虚拟中断控制器计算准备分发的虚拟中断注入到虚拟机VMX页VMX_ENTRY_INT_INFO_FIELD字段最终返回虚拟机执行中断处理。通过上面的分析我们对Intel处理器的虚拟中断处理原理及InterruptWindow机制也有了一个大
6、概的了解,下面我们准备就基于InterruptWindow机制进行一次安全性形式化验证。我们的目标是通过对开源这个功能模型的形式化模型检测来验证这部分设计是否安全可靠,在做验证之前我们先来简单了解一下形式化验证的两个基本概念。3.形式化验证概念介绍我们说软件安全性主要取决于设计阶段的模型是否安全、正确,传统的软件设计主要是基于标准的瀑布模型即:需求分析、系统设计、详细设计、编码、测试几个基本环节组成。实际上整个开发过程并没有针对需求和设计的模型推导和验证阶段,所谓需求分析、系统设计只是针对功能实现而言的,这时的系统设计还比较粗糙实际上主要依赖于以往的经验和简单的逻辑分析并没有做完备的模型正确性
7、推演和验证,因为此时也没有工具和手段在这个阶段进行概念级的验证,真正的软件正确性主要还是依靠设计评审和功能测试两个阶段来保证。但这两个阶段还是存在较大程度人为经验的因素,包括评审组人员的构成、背景、经验,测试组人员对需求的理解程度、是否有相关领域的测试背景经验都会最终影响设计正确性的保证,因此传统的软件工程方法是无法从根本上保证软件设计的安全性、正确性,必须有一种客观性的理论方法来保证在需求分析、概念建模阶段就存在一个可量化、能够验证的模型才能从根本上解决上述问题。这种方法在目前业界叫做形式化方法,形式化方法的核心就是形式化语言,以及基于形式化语言构建出来的形式化模型。对于一些高可靠性系统如:
8、航天器、车载发动机、工业自动化控制器等来说其系统的行为必须是可以预测的,即某些非法或不可预测的错误行为都是不允许的,而传统依靠测试和同行评审为主的软件工程方法无法保证这些系统属性行为的正确性,所以需要将这些高可靠性系统用语义明确的形式化语言进行建模,采用模型检测、定理证明的方法对系统目标属性进行正确性推演和验证。4.LTL(线性时态逻辑)简介线性时态逻辑是由命题时态逻辑(PTL)和一阶时态逻辑(FOTL)组成,其中PTL、FOTL本质上是在命题逻辑、一阶逻辑基础上扩展了模态词或时态算子的模态逻辑。线性时态逻辑所用到的时态算子如下: always算子,F表示F总是为真或者F永远为真。 somet
9、imes算子,F表示F最终为真或者F有时为真。 next算子,F表示F在下一时刻为真。 until算子,F1F2表示F1一直为真直到F2为真。命题时态逻辑公式:简称PTL公式,定义如下:公理1:原子命题(命题常元或者命题变元)是PTL公式。公理2:如果F1、F2是PTL公式,那么F1(非)、F1F2(合取)、F1F2(析取)、F1 F2(蕴含)、F1F2(等价)是PTL公式。公理3:如果F是PTL公式,那么F、F、F是PTL公式。公理4:如果F1、F2是PTL公式,那么F1F2是PTL公式。公理5:当且仅当有限次地使用公理1-4所组成的公式是PTL合法公式。命题时态逻辑公式的BNF表示为::=
10、 P|一阶时态逻辑公式:简称FOTL公式,定义如下:公理1:原子谓词公式是FOTL公式。公理2:如果F1、F2是FOTL公式,那么F1(非)、F1F2(合取)、F1F2(析取)、F1 F2(蕴含)、F1F2(等价)是FOTL公式。公理3:如果F是FOTL公式,x是F中出现的变量即个体变元,则x.F、x.F是FOTL公式。公理4:如果F1、F2是FOTL公式,那么F1、F1、F1、F1F2是FOTL公式。公理5:当且仅当有限次地使用公理1-4所组成的公式是FOTL合法公式。一阶时态逻辑公式的BNF表示为::= P|x.|x.|PTL公式和FOTL公式统称为LTL公式。了解了上述基本概念后下面我们
11、就可以开始进行形式化验证模型的设计工作。5.基于LTL的形式化验证模型设计目前我们做InterruptWindow这部分的形式化验证主要是采用经典的LTL即线性时态逻辑来进行,采用线性时态逻辑主要有两方面的考虑:一是线性时态逻辑比较适合进行算法的过程描述,可以快速由底层代码的分析抽象生成上层的数学验证模型;二是时态逻辑属性比较适合做模型检测。下面我们开始通过对ACRN的InterruptWindow代码分析进行LTL形式化模型抽象,InterruptWindow的处理模型由以下几个部分组成:1)虚拟机运行状态2)VM_Exit事件处理3)外部中断处理4)虚拟中断计算与分发5)Interrupt
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- ACRN InterruptWindow 功能 正确性 形式化 验证
链接地址:https://www.31doc.com/p-3245611.html