ACRN之InterruptWindow功能正确性形式化验证

1. ACRN背景简介

ACRN是Linux基金会今年发布的一款新的嵌入式hypervisor参考软件，项目的官方名称为ACRN，这是一个专为物联网和嵌入式设备设计的管理程序。该项目得益于英特尔代码和工程的贡献，其目标是创建一个灵活小巧的虚拟机管理系统。通过基于 Linux 的服务操作系统，ACRN 可以同时运行多个客户操作系统，如 Android、其他Linux发行版，或者RTOS，使其成为许多场景的理想选择。ACRN架构如图所示：

图1  ACRN架构

我们下面需要验证的功能就是ACRN的InterruptWindow功能模型，在验证该模型之前我们需要先进行一下基础知识的培训。

2. x86_64架构的InterruptWindow原理介绍

Intel InterruptWindow功能是专门为运行在x86_64平台上的虚拟机处理虚拟中断设计的硬件功能，那么为什么要有InterruptWindow功能我们还要从虚拟中断的处理流程开始说起，一般来讲基于x86_64平台物理机中断处理简化流程如下所示：

图2  x86_64平台物理机中断处理流程

那么现在我们回过头来再看看如果是虚拟机该如何模拟物理机的中断过程，我们说做设计之前一般做法是首先要做几个核心问题的抽象，然后再根据这些问题找到相应的解决方案，最后当问题迎刃而解的时候设计方案也自然水到渠成，相应的我们做虚拟机中断模型分析之前也需要先抛出几个核心问题：

运行中的虚拟机如何处理外部中断？

外部中断如何注入到虚拟机的中断控制器中？

虚拟机的中断控制器何时进行中断的计算与分发？

回答一：Intel目前的处理方式分为两种情况考虑：

1）外部中断分发到虚拟机正在运行的CPU核，此时硬件会产生一个vm_exit事件让虚拟机暂停运行退出到Hypervisor层进行中断处理；

2）外部中断分发到非虚拟机运行的CPU核，此时由Hypervisor层对该中断进行处理。

回答二：Intel提供了inject_event方式注入中断，简单说是将需要马上处理的虚拟中断写入到硬件提供VMX内存页的VMX_ENTRY_INT_INFO_FIELD字段，当系统执行vm_entry指令返回虚拟机运行模式时这个字段会被硬件检测触发中断动作跳转到虚拟机的IDT表执行中断处理。

回答三：通过对上述inject_event工作原理的描述，我们可以得出结论虚拟中断的计算与分发需要在Hypervisor层由软件来完成。

这样我们就遇到一个问题，假如当前虚拟机处于vm_exit状态，那么可以由软件完成虚拟中断的计算与分发，但是我们考虑一种特殊情况，如果当前vm_exit的虚拟机本身处于关中断状态，那么此时注入虚拟中断返回虚拟机时硬件必然会响应当前的中断，这显然是错误的，因此此时我们只能暂时放弃注入虚拟中断，等到虚拟机打开中断使能状态才能让硬件响应中断，那么这该如何做到呢？

Intel提供了一种InterruptWindow机制来解决这个问题，该机制的原理是：配置了InterrruptWindow使能的虚拟机运行阶段当执行STI指令打开中断使能会触发一个vm_exit事件退出到Hypervisor，这个退出原因硬件会标记为InterruptWindow，Hypervisor层会根据这个事件将虚拟中断控制器计算准备分发的虚拟中断注入到虚拟机VMX页VMX_ENTRY_INT_INFO_FIELD字段最终返回虚拟机执行中断处理。

通过上面的分析我们对Intel处理器的虚拟中断处理原理及InterruptWindow机制也有了一个大概的了解，下面我们准备就基于InterruptWindow机制进行一次安全性形式化验证。

我们的目标是通过对开源这个功能模型的形式化模型检测来验证这部分设计是否安全可靠，在做验证之前我们先来简单了解一下形式化验证的两个基本概念。

3. 形式化验证概念介绍

我们说软件安全性主要取决于设计阶段的模型是否安全、正确，传统的软件设计主要是基于标准的瀑布模型即：需求分析、系统设计、详细设计、编码、测试几个基本环节组成。

实际上整个开发过程并没有针对需求和设计的模型推导和验证阶段，所谓需求分析、系统设计只是针对功能实现而言的，这时的系统设计还比较粗糙实际上主要依赖于以往的经验和简单的逻辑分析并没有做完备的模型正确性推演和验证，因为此时也没有工具和手段在这个阶段进行概念级的验证，真正的软件正确性主要还是依靠设计评审和功能测试两个阶段来保证。

但这两个阶段还是存在较大程度人为经验的因素，包括评审组人员的构成、背景、经验，测试组人员对需求的理解程度、是否有相关领域的测试背景经验都会最终影响设计正确性的保证，因此传统的软件工程方法是无法从根本上保证软件设计的安全性、正确性，必须有一种客观性的理论方法来保证在需求分析、概念建模阶段就存在一个可量化、能够验证的模型才能从根本上解决上述问题。

这种方法在目前业界叫做形式化方法，形式化方法的核心就是形式化语言，以及基于形式化语言构建出来的形式化模型。

对于一些高可靠性系统如：航天器、车载发动机、工业自动化控制器等来说其系统的行为必须是可以预测的，即某些非法或不可预测的错误行为都是不允许的，而传统依靠测试和同行评审为主的软件工程方法无法保证这些系统属性行为的正确性，所以需要将这些高可靠性系统用语义明确的形式化语言进行建模，采用模型检测、定理证明的方法对系统目标属性进行正确性推演和验证。

4. LTL（线性时态逻辑）简介

线性时态逻辑是由命题时态逻辑（PTL）和一阶时态逻辑（FOTL）组成，其中PTL、FOTL本质上是在命题逻辑、一阶逻辑基础上扩展了模态词或时态算子的模态逻辑。

线性时态逻辑所用到的时态算子如下：

□ always算子，□F表示F总是为真或者F永远为真。

◇ sometimes算子，◇F表示F最终为真或者F有时为真。

○ next算子，○F表示F在下一时刻为真。

▷ until算子，F1▷F2表示F1一直为真直到F2为真。

命题时态逻辑公式：简称PTL公式，定义如下：

公理1：原子命题（命题常元或者命题变元）是PTL公式。

公理2：如果F1、F2是PTL公式，那么﹁F1(非）、F1∧F2（合取）、F1∨F2（析取）、F1⟶ F2（蕴含）、F1↔F2（等价）是PTL公式。

公理3：如果F是PTL公式，那么□F、◇F、○F是PTL公式。

公理4：如果F1、F2是PTL公式，那么F1▷F2是PTL公式。

公理5：当且仅当有限次地使用公理1-4所组成的公式是PTL合法公式。

命题时态逻辑公式的BNF表示为：

Φ::= P|¬Φ|Φ∧Φ|Φ∨Φ|Φ⟶Φ|Φ↔Φ|□Φ|◇Φ|○Φ|Φ▷Φ

一阶时态逻辑公式：简称FOTL公式，定义如下：

公理1：原子谓词公式是FOTL公式。

公理2：如果F1、F2是FOTL公式，那么﹁F1（非）、F1∧F2（合取）、F1∨F2（析取）、F1⟶ F2（蕴含）、F1↔F2（等价）是FOTL公式。

公理3：如果F是FOTL公式，x是F中出现的变量即个体变元，则∀x.F、∃x.F是FOTL公式。

公理4：如果F1、F2是FOTL公式，那么□F1、◇F1、○F1、F1▷F2是FOTL公式。

公理5：当且仅当有限次地使用公理1-4所组成的公式是FOTL合法公式。

一阶时态逻辑公式的BNF表示为：

Φ::= P|¬Φ|Φ∧Φ|Φ∨Φ|Φ⟶Φ|Φ↔Φ|∀x.Φ|∃x.Φ|□Φ|◇Φ|○Φ|Φ▷Φ

PTL公式和FOTL公式统称为LTL公式。

了解了上述基本概念后下面我们就可以开始进行形式化验证模型的设计工作。

5. 基于LTL的形式化验证模型设计

目前我们做InterruptWindow这部分的形式化验证主要是采用经典的LTL即线性时态逻辑来进行，采用线性时态逻辑主要有两方面的考虑：一是线性时态逻辑比较适合进行算法的过程描述，可以快速由底层代码的分析抽象生成上层的数学验证模型；二是时态逻辑属性比较适合做模型检测。

下面我们开始通过对ACRN的InterruptWindow代码分析进行LTL形式化模型抽象，InterruptWindow的处理模型由以下几个部分组成：

1）虚拟机运行状态

2）VM_Exit事件处理

3）外部中断处理

4）虚拟中断计算与分发

5）InterruptWindow计算

我们说形式化方法并不是简单地去模拟一个CPU软件运行环境对被测目标代码进行运行时检查，那是软件测试的思路，形式化验证是指用数学方法对被验证的目标系统包括软硬件运行环境、代码功能进行抽象建模，通过数学层面的定理推导或模型计算完成预期目标正确性、可靠性的验证，因此形式化方法是无所不能的，只要你能够把被验证的目标系统用数学模型表达出来，那么剩下的事情都可以利用数学领域的知识来加以解决。

好了，通过上面的分析我们进一步了解了形式化方法的基本思想，现在我们使用形式化思想对上述InterruptWindow机制涉及到几个关键部件进行建模：

构建虚拟机运行状态模型

这个模型的抽象我们需要抓住核心要素剖析虚拟机运行状态下哪些是对模型验证起到核心作用的元素，实际上虚拟机在运行阶段无非就是完成三个关键动作，一是响应外部中断；二是虚拟中断执行；三是InterruptWindow检测与处理，因此我们只需要在模型里面表达出这三个核心要素即可完成目标，在LTL逻辑里面我们使用一个外部中断集合来表达外部中断在虚拟机运行阶段的响应动作，使用虚拟中断集合来表达虚拟中断控制器，那么虚拟机运行状态数学模型表示如下：

解释一下，这个模型每次执行vm_run状态都会触发external_interrupts的一次中断，在数学上我们表示为如果external_interrupts集合不为空则表明有外部中断过来，则虚拟机执行vm_exit跳转到下一个状态l2执行，当external_interrupts集合为空时表明当前没有外部中断需要处理，这时虚拟机要处理自身的虚拟中断，如果当前vapic集合不为空则从vapic集合里面选取一个最高优先级中断代表中断注入执行，执行完毕后检测irq_window_enabled时态变量是否为TRUE，如果为TRUE则表明InterruptWindow被使能，则需要模拟一个vm_exit事件跳转到下一个状态l2执行，如果当前vapic集合为空则表明目前没有需要处理的虚拟中断，此时需要查看pending_intr集合，这个集合是用来模拟IRR中断请求寄存器，如果此时IRR也为空则代表确实无中断需要处理则直接跳转到pc=“done”状态结束，如果IRR不为空而vapic集合为空那么说明模型处理一定有问题则跳转回原状态死循环，别担心这个死循环不是真的程序死循环而是状态循环，目的是让模型检查器能够及时捕捉到BUG所在。

VM_Exit事件处理

这部分功能的代码逻辑是：如果IRR为空表明没有虚拟中断需要注入则irq_window_enabled需要关闭使能，然后跳转到下一个状态l3继续处理，模型如下所示：

外部中断处理

ACRN针对外部中断的处理主要是放在softirq软中断处理过程执行，这部分我们只完成一个操作那就是从external_interrupts集合里面取出一个中断放入pending_intr集合，模拟实际硬件的动作，执行完成后跳转到下一个状态l4，实现如下：

虚拟中断计算与分发

这部分处理按照代码设计是放在acrn_do_intr_process过程中实现，我们的数学抽象是从pending_intr集合中取出一个中断然后加入到vapic集合中，完成虚拟中断的计算与分发注入动作，处理完成后继续跳转到下一个状态l5，实现如下：

InterruptWindow计算

这部分直接按照ACRN的代码逻辑照抄即可，逻辑本身并不复杂就不做过多的解释了直接看公式模型可以很容易搞懂，这部分逻辑执行完毕则跳转到l1即vm_run状态模拟vm_entry指令动作进入虚拟机运行态，模型如下：        

6. LTL并发处理模型构建

ACRN的InterruptWindow代码是可被多个VCPU线程重入的并发处理模型，因此需要针对该代码模型进行死锁或异常运行检查，这是确保安全性的关键要素之一，那么需要我们首先基于上述处理模型的推导进一步构造出并发处理模型的数学描述，LTL是将并发模型表示为时序状态的不确定性组合，因此我们可以使用时态逻辑状态机模型来表达这种不确定性组合，这也是上述不同时序状态对应的逻辑公式为什么都有一个self的原因，这个self是代表着并发执行的不同VCPU线程，为了达到独立并发执行目的我们需要将每个VCPU线程的vapic、pending_intr、interruptwindow、external_interrupts设计成独立的时态逻辑变量，因此我们可以采取Function+Record的方式，实现如下所示：

现在我们可以设计一个时序状态机让这些时序状态并发运行起来，为了达到这个目的我们需要给每个状态赋一个PC状态指针作为状态迁移的使能标识，由于每个VCPU线程拥有一个独立的PC状态指针，因此PC状态指针的设计可以采取Function方式，如下：

：

我们的时序状态机可以如下设计：

解释一下这个时序状态机分为四部分：

Init是时序状态初始化

vm是并发计算的语义描述

Next是下一个时序状态计算，语义是：当前VCPU线程集合必定存在一个VCPU线程可以满足vm的状态，并把这个状态作为下一个时序状态

Spec就是上述时序状态机运行语义模型的规格化描述

7. 安全性验证之程序终止性检查

InterruptWindow机制的安全性检查包括两部分：第一部分是程序能够正常终止，这部分检查是为后续正确性检查做准备工作，因为不能终止的程序是不能做正确性验证的，本质上InterruptWindow机制是一个循环的处理流程无法正常终止，但是我们可以通过数学抽象的手段将我们需要验证的状态属性模拟完毕后让时序状态机处于stuttering状态即处于终止状态，这样外部我们可以通过pc状态指针pc=“done”来设计一个时态属性进行检查；另一部分是并发程序终止性检查可以验证并发程序是否存在死锁或异常运行状态，程序终止性检查时态属性设计如下：

现在我们根据上述的时态属性设计开始使用数学模型验证工具来进行安全性检查，我们选取TLA+工具来做检查工作，至于TLA+工具如何使用由于网络上介绍性的文章比较多，使用方法本身也非常简单，不是本文讲解的重点就不做过多说明了，大家可以自行上网进行学习，书归正传我们现在开始用TLA+的TLC工具进行模型验证，配置检查属性后的验证结果表明：1.程序可以正常结束；2.并发VCPU线程不存在死锁和异常运行状态，TLC检测截图如下：

8. 安全性验证之程序正确性检查

我们已经完成了程序可终止性验证，但是能够正常终止不发生死锁的程序并不代表一定是正确的，即我们需要有一种模型来检查程序的设计是否符合我们的预期目标，那么如何做到这一点呢？我们说一般程序设计是否符合预期需要验证两个目标：一是结果正确性，二是过程正确性。对于InterruptWindow算法模型我们的时序状态最终需要满足的结果是：

即任意一个VCPU的pending_intr和vapic集合都为空。

那么过程正确性是什么呢？我们可以抽象为一个可归纳性不变式来表达：

即任意一个VCPU，如果pending_intr集合不为空，当前pc状态指针为l1，那么InterruptWindow一定使能，说的更通俗些就是如果当前VCPU除了当前中断还有其他中断要处理并且VCPU处于运行态，那么必须使能InterruptWindow机制。这条可归纳性不变式即是InterruptWindow功能的核心模型，你的软件设计正确性与否在于是否满足这条不变式性质，根据上面的设计我们使用TLC对正确性属性和不变式进行验证，验证结果如下图：  

可以看到验证结果正确，证明了ACRN的InterruptWindow软件模型设计是符合预期的。

9. 推广建议

这部分代码是Intel从KVM模块中继承过来的，经过了千锤百炼可以看到还是比较稳定可靠的，实际上欧美的软件公司在设计阶段一般都会有不同程度的模型验证，而不是简单地上来就开始做设计直接写代码，这样做的目的是为了保证后期的设计具有扎实的理论依据和可靠性基础，Intel的Hypervisor设计据了解也是做了局部模型验证的，没有形式化建模分析单纯依靠业务和编码经验是很难设计出真正可靠的软件产品的，而且基于形式化模型的设计开发效率要比普通软件开发方法效率高出不止一个数量级，因此形式化方法对我司的软件产品质量提升具有非常重要的意义，在物联网操作系统、车载操作系统、高可靠性通信设备软件包括光传输、路由器、交换机核心业务模型、协议模型、5G通讯协议安全性验证领域比较适合采取形式化验证方法来保证软件模型的正确性、可靠性。