1.ACRN背景簡(jiǎn)介

ACRN是Linux基金會(huì)今年發(fā)布的一款新的嵌入式hypervisor參考軟件，項(xiàng)目的官方名稱為ACRN，這是一個(gè)專(zhuān)為物聯(lián)網(wǎng)和嵌入式設(shè)備設(shè)計(jì)的管理程序。該項(xiàng)目得益于英特爾代碼和工程的貢獻(xiàn)，其目標(biāo)是創(chuàng)建一個(gè)靈活小巧的虛擬機(jī)管理系統(tǒng)。通過(guò)基于Linux 的服務(wù)操作系統(tǒng)，ACRN 可以同時(shí)運(yùn)行多個(gè)客戶操作系統(tǒng)，如 Android、其他Linux發(fā)行版，或者RTOS，使其成為許多場(chǎng)景的理想選擇。ACRN架構(gòu)如圖所示：

圖1 ACRN架構(gòu)

我們下面需要驗(yàn)證的功能就是ACRN的InterruptWindow功能模型，在驗(yàn)證該模型之前我們需要先進(jìn)行一下基礎(chǔ)知識(shí)的培訓(xùn)。

2.x86_64架構(gòu)的InterruptWindow原理介紹

Intel InterruptWindow功能是專(zhuān)門(mén)為運(yùn)行在x86_64平臺(tái)上的虛擬機(jī)處理虛擬中斷設(shè)計(jì)的硬件功能，那么為什么要有InterruptWindow功能我們還要從虛擬中斷的處理流程開(kāi)始說(shuō)起，一般來(lái)講基于x86_64平臺(tái)物理機(jī)中斷處理簡(jiǎn)化流程如下所示：

圖2 x86_64平臺(tái)物理機(jī)中斷處理流程

那么現(xiàn)在我們回過(guò)頭來(lái)再看看如果是虛擬機(jī)該如何模擬物理機(jī)的中斷過(guò)程，我們說(shuō)做設(shè)計(jì)之前一般做法是首先要做幾個(gè)核心問(wèn)題的抽象，然后再根據(jù)這些問(wèn)題找到相應(yīng)的解決方案，最后當(dāng)問(wèn)題迎刃而解的時(shí)候設(shè)計(jì)方案也自然水到渠成，相應(yīng)的我們做虛擬機(jī)中斷模型分析之前也需要先拋出幾個(gè)核心問(wèn)題：

運(yùn)行中的虛擬機(jī)如何處理外部中斷？

外部中斷如何注入到虛擬機(jī)的中斷控制器中？

虛擬機(jī)的中斷控制器何時(shí)進(jìn)行中斷的計(jì)算與分發(fā)？

回答一：Intel目前的處理方式分為兩種情況考慮：

1）外部中斷分發(fā)到虛擬機(jī)正在運(yùn)行的CPU核，此時(shí)硬件會(huì)產(chǎn)生一個(gè)vm_exit事件讓虛擬機(jī)暫停運(yùn)行退出到Hypervisor層進(jìn)行中斷處理；

2）外部中斷分發(fā)到非虛擬機(jī)運(yùn)行的CPU核，此時(shí)由Hypervisor層對(duì)該中斷進(jìn)行處理。

回答二：Intel提供了inject_event方式注入中斷，簡(jiǎn)單說(shuō)是將需要馬上處理的虛擬中斷寫(xiě)入到硬件提供VMX內(nèi)存頁(yè)的VMX_ENTRY_INT_INFO_FIELD字段，當(dāng)系統(tǒng)執(zhí)行vm_entry指令返回虛擬機(jī)運(yùn)行模式時(shí)這個(gè)字段會(huì)被硬件檢測(cè)觸發(fā)中斷動(dòng)作跳轉(zhuǎn)到虛擬機(jī)的IDT表執(zhí)行中斷處理。

回答三：通過(guò)對(duì)上述inject_event工作原理的描述，我們可以得出結(jié)論虛擬中斷的計(jì)算與分發(fā)需要在Hypervisor層由軟件來(lái)完成。

這樣我們就遇到一個(gè)問(wèn)題，假如當(dāng)前虛擬機(jī)處于vm_exit狀態(tài)，那么可以由軟件完成虛擬中斷的計(jì)算與分發(fā)，但是我們考慮一種特殊情況，如果當(dāng)前vm_exit的虛擬機(jī)本身處于關(guān)中斷狀態(tài)，那么此時(shí)注入虛擬中斷返回虛擬機(jī)時(shí)硬件必然會(huì)響應(yīng)當(dāng)前的中斷，這顯然是錯(cuò)誤的，因此此時(shí)我們只能暫時(shí)放棄注入虛擬中斷，等到虛擬機(jī)打開(kāi)中斷使能狀態(tài)才能讓硬件響應(yīng)中斷，那么這該如何做到呢？

Intel提供了一種InterruptWindow機(jī)制來(lái)解決這個(gè)問(wèn)題，該機(jī)制的原理是：配置了InterrruptWindow使能的虛擬機(jī)運(yùn)行階段當(dāng)執(zhí)行STI指令打開(kāi)中斷使能會(huì)觸發(fā)一個(gè)vm_exit事件退出到Hypervisor，這個(gè)退出原因硬件會(huì)標(biāo)記為InterruptWindow，Hypervisor層會(huì)根據(jù)這個(gè)事件將虛擬中斷控制器計(jì)算準(zhǔn)備分發(fā)的虛擬中斷注入到虛擬機(jī)VMX頁(yè)VMX_ENTRY_INT_INFO_FIELD字段最終返回虛擬機(jī)執(zhí)行中斷處理。

通過(guò)上面的分析我們對(duì)Intel處理器的虛擬中斷處理原理及InterruptWindow機(jī)制也有了一個(gè)大概的了解，下面我們準(zhǔn)備就基于InterruptWindow機(jī)制進(jìn)行一次安全性形式化驗(yàn)證。

我們的目標(biāo)是通過(guò)對(duì)開(kāi)源這個(gè)功能模型的形式化模型檢測(cè)來(lái)驗(yàn)證這部分設(shè)計(jì)是否安全可靠，在做驗(yàn)證之前我們先來(lái)簡(jiǎn)單了解一下形式化驗(yàn)證的兩個(gè)基本概念。

3.形式化驗(yàn)證概念介紹

我們說(shuō)軟件安全性主要取決于設(shè)計(jì)階段的模型是否安全、正確，傳統(tǒng)的軟件設(shè)計(jì)主要是基于標(biāo)準(zhǔn)的瀑布模型即：需求分析、系統(tǒng)設(shè)計(jì)、詳細(xì)設(shè)計(jì)、編碼、測(cè)試幾個(gè)基本環(huán)節(jié)組成。

實(shí)際上整個(gè)開(kāi)發(fā)過(guò)程并沒(méi)有針對(duì)需求和設(shè)計(jì)的模型推導(dǎo)和驗(yàn)證階段，所謂需求分析、系統(tǒng)設(shè)計(jì)只是針對(duì)功能實(shí)現(xiàn)而言的，這時(shí)的系統(tǒng)設(shè)計(jì)還比較粗糙實(shí)際上主要依賴于以往的經(jīng)驗(yàn)和簡(jiǎn)單的邏輯分析并沒(méi)有做完備的模型正確性推演和驗(yàn)證，因?yàn)榇藭r(shí)也沒(méi)有工具和手段在這個(gè)階段進(jìn)行概念級(jí)的驗(yàn)證，真正的軟件正確性主要還是依靠設(shè)計(jì)評(píng)審和功能測(cè)試兩個(gè)階段來(lái)保證。

但這兩個(gè)階段還是存在較大程度人為經(jīng)驗(yàn)的因素，包括評(píng)審組人員的構(gòu)成、背景、經(jīng)驗(yàn)，測(cè)試組人員對(duì)需求的理解程度、是否有相關(guān)領(lǐng)域的測(cè)試背景經(jīng)驗(yàn)都會(huì)最終影響設(shè)計(jì)正確性的保證，因此傳統(tǒng)的軟件工程方法是無(wú)法從根本上保證軟件設(shè)計(jì)的安全性、正確性，必須有一種客觀性的理論方法來(lái)保證在需求分析、概念建模階段就存在一個(gè)可量化、能夠驗(yàn)證的模型才能從根本上解決上述問(wèn)題。

這種方法在目前業(yè)界叫做形式化方法，形式化方法的核心就是形式化語(yǔ)言，以及基于形式化語(yǔ)言構(gòu)建出來(lái)的形式化模型。

對(duì)于一些高可靠性系統(tǒng)如：航天器、車(chē)載發(fā)動(dòng)機(jī)、工業(yè)自動(dòng)化控制器等來(lái)說(shuō)其系統(tǒng)的行為必須是可以預(yù)測(cè)的，即某些非法或不可預(yù)測(cè)的錯(cuò)誤行為都是不允許的，而傳統(tǒng)依靠測(cè)試和同行評(píng)審為主的軟件工程方法無(wú)法保證這些系統(tǒng)屬性行為的正確性，所以需要將這些高可靠性系統(tǒng)用語(yǔ)義明確的形式化語(yǔ)言進(jìn)行建模，采用模型檢測(cè)、定理證明的方法對(duì)系統(tǒng)目標(biāo)屬性進(jìn)行正確性推演和驗(yàn)證。

4.LTL（線性時(shí)態(tài)邏輯）簡(jiǎn)介

線性時(shí)態(tài)邏輯是由命題時(shí)態(tài)邏輯（PTL）和一階時(shí)態(tài)邏輯（FOTL）組成，其中PTL、FOTL本質(zhì)上是在命題邏輯、一階邏輯基礎(chǔ)上擴(kuò)展了模態(tài)詞或時(shí)態(tài)算子的模態(tài)邏輯。

線性時(shí)態(tài)邏輯所用到的時(shí)態(tài)算子如下：

□ always算子，□F表示F總是為真或者F永遠(yuǎn)為真。

◇ sometimes算子，◇F表示F最終為真或者F有時(shí)為真。

○ next算子，○F表示F在下一時(shí)刻為真。

? until算子，F(xiàn)1?F2表示F1一直為真直到F2為真。

命題時(shí)態(tài)邏輯公式：簡(jiǎn)稱PTL公式，定義如下：

公理1：原子命題（命題常元或者命題變?cè)┦荘TL公式。

公理2：如果F1、F2是PTL公式，那么﹁F1(非）、F1∧F2（合取）、F1∨F2（析取）、F1? F2（蘊(yùn)含）、F1?F2（等價(jià)）是PTL公式。

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

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

公理5：當(dāng)且僅當(dāng)有限次地使用公理1-4所組成的公式是PTL合法公式。

命題時(shí)態(tài)邏輯公式的BNF表示為：

Φ::= P|?Φ|Φ∧Φ|Φ∨Φ|Φ?Φ|Φ?Φ|□Φ|◇Φ|○Φ|Φ?Φ

一階時(shí)態(tài)邏輯公式：簡(jiǎn)稱FOTL公式，定義如下：

公理1：原子謂詞公式是FOTL公式。

公理2：如果F1、F2是FOTL公式，那么﹁F1（非）、F1∧F2（合取）、F1∨F2（析取）、F1? F2（蘊(yùn)含）、F1?F2（等價(jià)）是FOTL公式。

公理3：如果F是FOTL公式，x是F中出現(xiàn)的變量即個(gè)體變?cè)瑒t?x.F、?x.F是FOTL公式。

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

公理5：當(dāng)且僅當(dāng)有限次地使用公理1-4所組成的公式是FOTL合法公式。

一階時(shí)態(tài)邏輯公式的BNF表示為：

Φ::= P|?Φ|Φ∧Φ|Φ∨Φ|Φ?Φ|Φ?Φ|?x.Φ|?x.Φ|□Φ|◇Φ|○Φ|Φ?Φ

PTL公式和FOTL公式統(tǒng)稱為L(zhǎng)TL公式。

了解了上述基本概念后下面我們就可以開(kāi)始進(jìn)行形式化驗(yàn)證模型的設(shè)計(jì)工作。

5.基于LTL的形式化驗(yàn)證模型設(shè)計(jì)

目前我們做InterruptWindow這部分的形式化驗(yàn)證主要是采用經(jīng)典的LTL即線性時(shí)態(tài)邏輯來(lái)進(jìn)行，采用線性時(shí)態(tài)邏輯主要有兩方面的考慮：一是線性時(shí)態(tài)邏輯比較適合進(jìn)行算法的過(guò)程描述，可以快速由底層代碼的分析抽象生成上層的數(shù)學(xué)驗(yàn)證模型；二是時(shí)態(tài)邏輯屬性比較適合做模型檢測(cè)。

下面我們開(kāi)始通過(guò)對(duì)ACRN的InterruptWindow代碼分析進(jìn)行LTL形式化模型抽象，InterruptWindow的處理模型由以下幾個(gè)部分組成：

1）虛擬機(jī)運(yùn)行狀態(tài)

2）VM_Exit事件處理

3）外部中斷處理

4）虛擬中斷計(jì)算與分發(fā)

5）InterruptWindow計(jì)算

我們說(shuō)形式化方法并不是簡(jiǎn)單地去模擬一個(gè)CPU軟件運(yùn)行環(huán)境對(duì)被測(cè)目標(biāo)代碼進(jìn)行運(yùn)行時(shí)檢查，那是軟件測(cè)試的思路，形式化驗(yàn)證是指用數(shù)學(xué)方法對(duì)被驗(yàn)證的目標(biāo)系統(tǒng)包括軟硬件運(yùn)行環(huán)境、代碼功能進(jìn)行抽象建模，通過(guò)數(shù)學(xué)層面的定理推導(dǎo)或模型計(jì)算完成預(yù)期目標(biāo)正確性、可靠性的驗(yàn)證，因此形式化方法是無(wú)所不能的，只要你能夠把被驗(yàn)證的目標(biāo)系統(tǒng)用數(shù)學(xué)模型表達(dá)出來(lái)，那么剩下的事情都可以利用數(shù)學(xué)領(lǐng)域的知識(shí)來(lái)加以解決。

好了，通過(guò)上面的分析我們進(jìn)一步了解了形式化方法的基本思想，現(xiàn)在我們使用形式化思想對(duì)上述InterruptWindow機(jī)制涉及到幾個(gè)關(guān)鍵部件進(jìn)行建模：

構(gòu)建虛擬機(jī)運(yùn)行狀態(tài)模型

這個(gè)模型的抽象我們需要抓住核心要素剖析虛擬機(jī)運(yùn)行狀態(tài)下哪些是對(duì)模型驗(yàn)證起到核心作用的元素，實(shí)際上虛擬機(jī)在運(yùn)行階段無(wú)非就是完成三個(gè)關(guān)鍵動(dòng)作，一是響應(yīng)外部中斷；二是虛擬中斷執(zhí)行；三是InterruptWindow檢測(cè)與處理，因此我們只需要在模型里面表達(dá)出這三個(gè)核心要素即可完成目標(biāo)，在LTL邏輯里面我們使用一個(gè)外部中斷集合來(lái)表達(dá)外部中斷在虛擬機(jī)運(yùn)行階段的響應(yīng)動(dòng)作，使用虛擬中斷集合來(lái)表達(dá)虛擬中斷控制器，那么虛擬機(jī)運(yùn)行狀態(tài)數(shù)學(xué)模型表示如下：

解釋一下，這個(gè)模型每次執(zhí)行vm_run狀態(tài)都會(huì)觸發(fā)external_interrupts的一次中斷，在數(shù)學(xué)上我們表示為如果external_interrupts集合不為空則表明有外部中斷過(guò)來(lái)，則虛擬機(jī)執(zhí)行vm_exit跳轉(zhuǎn)到下一個(gè)狀態(tài)l2執(zhí)行，當(dāng)external_interrupts集合為空時(shí)表明當(dāng)前沒(méi)有外部中斷需要處理，這時(shí)虛擬機(jī)要處理自身的虛擬中斷，如果當(dāng)前vapic集合不為空則從vapic集合里面選取一個(gè)最高優(yōu)先級(jí)中斷代表中斷注入執(zhí)行，執(zhí)行完畢后檢測(cè)irq_window_enabled時(shí)態(tài)變量是否為T(mén)RUE，如果為T(mén)RUE則表明InterruptWindow被使能，則需要模擬一個(gè)vm_exit事件跳轉(zhuǎn)到下一個(gè)狀態(tài)l2執(zhí)行，如果當(dāng)前vapic集合為空則表明目前沒(méi)有需要處理的虛擬中斷，此時(shí)需要查看pending_intr集合，這個(gè)集合是用來(lái)模擬IRR中斷請(qǐng)求寄存器，如果此時(shí)IRR也為空則代表確實(shí)無(wú)中斷需要處理則直接跳轉(zhuǎn)到pc=“done”狀態(tài)結(jié)束，如果IRR不為空而vapic集合為空那么說(shuō)明模型處理一定有問(wèn)題則跳轉(zhuǎn)回原狀態(tài)死循環(huán)，別擔(dān)心這個(gè)死循環(huán)不是真的程序死循環(huán)而是狀態(tài)循環(huán)，目的是讓模型檢查器能夠及時(shí)捕捉到BUG所在。

VM_Exit事件處理

這部分功能的代碼邏輯是：如果IRR為空表明沒(méi)有虛擬中斷需要注入則irq_window_enabled需要關(guān)閉使能，然后跳轉(zhuǎn)到下一個(gè)狀態(tài)l3繼續(xù)處理，模型如下所示：

外部中斷處理

ACRN針對(duì)外部中斷的處理主要是放在softirq軟中斷處理過(guò)程執(zhí)行，這部分我們只完成一個(gè)操作那就是從external_interrupts集合里面取出一個(gè)中斷放入pending_intr集合，模擬實(shí)際硬件的動(dòng)作，執(zhí)行完成后跳轉(zhuǎn)到下一個(gè)狀態(tài)l4，實(shí)現(xiàn)如下：

虛擬中斷計(jì)算與分發(fā)

這部分處理按照代碼設(shè)計(jì)是放在acrn_do_intr_process過(guò)程中實(shí)現(xiàn)，我們的數(shù)學(xué)抽象是從pending_intr集合中取出一個(gè)中斷然后加入到vapic集合中，完成虛擬中斷的計(jì)算與分發(fā)注入動(dòng)作，處理完成后繼續(xù)跳轉(zhuǎn)到下一個(gè)狀態(tài)l5，實(shí)現(xiàn)如下：

InterruptWindow計(jì)算

這部分直接按照ACRN的代碼邏輯照抄即可，邏輯本身并不復(fù)雜就不做過(guò)多的解釋了直接看公式模型可以很容易搞懂，這部分邏輯執(zhí)行完畢則跳轉(zhuǎn)到l1即vm_run狀態(tài)模擬vm_entry指令動(dòng)作進(jìn)入虛擬機(jī)運(yùn)行態(tài)，模型如下：

6.LTL并發(fā)處理模型構(gòu)建

ACRN的InterruptWindow代碼是可被多個(gè)VCPU線程重入的并發(fā)處理模型，因此需要針對(duì)該代碼模型進(jìn)行死鎖或異常運(yùn)行檢查，這是確保安全性的關(guān)鍵要素之一，那么需要我們首先基于上述處理模型的推導(dǎo)進(jìn)一步構(gòu)造出并發(fā)處理模型的數(shù)學(xué)描述，LTL是將并發(fā)模型表示為時(shí)序狀態(tài)的不確定性組合，因此我們可以使用時(shí)態(tài)邏輯狀態(tài)機(jī)模型來(lái)表達(dá)這種不確定性組合，這也是上述不同時(shí)序狀態(tài)對(duì)應(yīng)的邏輯公式為什么都有一個(gè)self的原因，這個(gè)self是代表著并發(fā)執(zhí)行的不同VCPU線程，為了達(dá)到獨(dú)立并發(fā)執(zhí)行目的我們需要將每個(gè)VCPU線程的vapic、pending_intr、interruptwindow、external_interrupts設(shè)計(jì)成獨(dú)立的時(shí)態(tài)邏輯變量，因此我們可以采取Function+Record的方式，實(shí)現(xiàn)如下所示：

現(xiàn)在我們可以設(shè)計(jì)一個(gè)時(shí)序狀態(tài)機(jī)讓這些時(shí)序狀態(tài)并發(fā)運(yùn)行起來(lái)，為了達(dá)到這個(gè)目的我們需要給每個(gè)狀態(tài)賦一個(gè)PC狀態(tài)指針作為狀態(tài)遷移的使能標(biāo)識(shí)，由于每個(gè)VCPU線程擁有一個(gè)獨(dú)立的PC狀態(tài)指針，因此PC狀態(tài)指針的設(shè)計(jì)可以采取Function方式，如下：

：

我們的時(shí)序狀態(tài)機(jī)可以如下設(shè)計(jì)：

解釋一下這個(gè)時(shí)序狀態(tài)機(jī)分為四部分：

Init是時(shí)序狀態(tài)初始化

vm是并發(fā)計(jì)算的語(yǔ)義描述

Next是下一個(gè)時(shí)序狀態(tài)計(jì)算，語(yǔ)義是：當(dāng)前VCPU線程集合必定存在一個(gè)VCPU線程可以滿足vm的狀態(tài)，并把這個(gè)狀態(tài)作為下一個(gè)時(shí)序狀態(tài)

Spec就是上述時(shí)序狀態(tài)機(jī)運(yùn)行語(yǔ)義模型的規(guī)格化描述

7.安全性驗(yàn)證之程序終止性檢查

InterruptWindow機(jī)制的安全性檢查包括兩部分：第一部分是程序能夠正常終止，這部分檢查是為后續(xù)正確性檢查做準(zhǔn)備工作，因?yàn)椴荒芙K止的程序是不能做正確性驗(yàn)證的，本質(zhì)上InterruptWindow機(jī)制是一個(gè)循環(huán)的處理流程無(wú)法正常終止，但是我們可以通過(guò)數(shù)學(xué)抽象的手段將我們需要驗(yàn)證的狀態(tài)屬性模擬完畢后讓時(shí)序狀態(tài)機(jī)處于stuttering狀態(tài)即處于終止?fàn)顟B(tài)，這樣外部我們可以通過(guò)pc狀態(tài)指針pc=“done”來(lái)設(shè)計(jì)一個(gè)時(shí)態(tài)屬性進(jìn)行檢查；另一部分是并發(fā)程序終止性檢查可以驗(yàn)證并發(fā)程序是否存在死鎖或異常運(yùn)行狀態(tài)，程序終止性檢查時(shí)態(tài)屬性設(shè)計(jì)如下：

現(xiàn)在我們根據(jù)上述的時(shí)態(tài)屬性設(shè)計(jì)開(kāi)始使用數(shù)學(xué)模型驗(yàn)證工具來(lái)進(jìn)行安全性檢查，我們選取TLA+工具來(lái)做檢查工作，至于TLA+工具如何使用由于網(wǎng)絡(luò)上介紹性的文章比較多，使用方法本身也非常簡(jiǎn)單，不是本文講解的重點(diǎn)就不做過(guò)多說(shuō)明了，大家可以自行上網(wǎng)進(jìn)行學(xué)習(xí)，書(shū)歸正傳我們現(xiàn)在開(kāi)始用TLA+的TLC工具進(jìn)行模型驗(yàn)證，配置檢查屬性后的驗(yàn)證結(jié)果表明：1.程序可以正常結(jié)束；2.并發(fā)VCPU線程不存在死鎖和異常運(yùn)行狀態(tài)，TLC檢測(cè)截圖如下：

8.安全性驗(yàn)證之程序正確性檢查

我們已經(jīng)完成了程序可終止性驗(yàn)證，但是能夠正常終止不發(fā)生死鎖的程序并不代表一定是正確的，即我們需要有一種模型來(lái)檢查程序的設(shè)計(jì)是否符合我們的預(yù)期目標(biāo)，那么如何做到這一點(diǎn)呢？我們說(shuō)一般程序設(shè)計(jì)是否符合預(yù)期需要驗(yàn)證兩個(gè)目標(biāo)：一是結(jié)果正確性，二是過(guò)程正確性。對(duì)于InterruptWindow算法模型我們的時(shí)序狀態(tài)最終需要滿足的結(jié)果是：

即任意一個(gè)VCPU的pending_intr和vapic集合都為空。

那么過(guò)程正確性是什么呢？我們可以抽象為一個(gè)可歸納性不變式來(lái)表達(dá)：

即任意一個(gè)VCPU，如果pending_intr集合不為空，當(dāng)前pc狀態(tài)指針為l1，那么InterruptWindow一定使能，說(shuō)的更通俗些就是如果當(dāng)前VCPU除了當(dāng)前中斷還有其他中斷要處理并且VCPU處于運(yùn)行態(tài)，那么必須使能InterruptWindow機(jī)制。這條可歸納性不變式即是InterruptWindow功能的核心模型，你的軟件設(shè)計(jì)正確性與否在于是否滿足這條不變式性質(zhì)，根據(jù)上面的設(shè)計(jì)我們使用TLC對(duì)正確性屬性和不變式進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如下圖：

可以看到驗(yàn)證結(jié)果正確，證明了ACRN的InterruptWindow軟件模型設(shè)計(jì)是符合預(yù)期的。

9.推廣建議

這部分代碼是Intel從KVM模塊中繼承過(guò)來(lái)的，經(jīng)過(guò)了千錘百煉可以看到還是比較穩(wěn)定可靠的，實(shí)際上歐美的軟件公司在設(shè)計(jì)階段一般都會(huì)有不同程度的模型驗(yàn)證，而不是簡(jiǎn)單地上來(lái)就開(kāi)始做設(shè)計(jì)直接寫(xiě)代碼，這樣做的目的是為了保證后期的設(shè)計(jì)具有扎實(shí)的理論依據(jù)和可靠性基礎(chǔ)，Intel的Hypervisor設(shè)計(jì)據(jù)了解也是做了局部模型驗(yàn)證的，沒(méi)有形式化建模分析單純依靠業(yè)務(wù)和編碼經(jīng)驗(yàn)是很難設(shè)計(jì)出真正可靠的軟件產(chǎn)品的，而且基于形式化模型的設(shè)計(jì)開(kāi)發(fā)效率要比普通軟件開(kāi)發(fā)方法效率高出不止一個(gè)數(shù)量級(jí)，因此形式化方法對(duì)我司的軟件產(chǎn)品質(zhì)量提升具有非常重要的意義，在物聯(lián)網(wǎng)操作系統(tǒng)、車(chē)載操作系統(tǒng)、高可靠性通信設(shè)備軟件包括光傳輸、路由器、交換機(jī)核心業(yè)務(wù)模型、協(xié)議模型、5G通訊協(xié)議安全性驗(yàn)證領(lǐng)域比較適合采取形式化驗(yàn)證方法來(lái)保證軟件模型的正確性、可靠性。