1.ACRN背景簡介

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

圖1 ACRN架構(gòu)

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

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

Intel InterruptWindow功能是專門為運行在x86_64平臺上的虛擬機處理虛擬中斷設(shè)計的硬件功能，那么為什么要有InterruptWindow功能我們還要從虛擬中斷的處理流程開始說起，一般來講基于x86_64平臺物理機中斷處理簡化流程如下所示：

圖2 x86_64平臺物理機中斷處理流程

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

運行中的虛擬機如何處理外部中斷？

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

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

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

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

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

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

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

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

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

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

我們的目標(biāo)是通過對開源這個功能模型的形式化模型檢測來驗證這部分設(shè)計是否安全可靠，在做驗證之前我們先來簡單了解一下形式化驗證的兩個基本概念。

3.形式化驗證概念介紹

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

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

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

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

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

4.LTL（線性時態(tài)邏輯）簡介

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

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

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

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

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

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

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

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

公理2：如果F1、F2是PTL公式，那么﹁F1(非）、F1∧F2（合?。1∨F2（析?。1? F2（蘊含）、F1?F2（等價）是PTL公式。

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

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

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

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

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

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

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

公理2：如果F1、F2是FOTL公式，那么﹁F1（非）、F1∧F2（合?。?、F1∨F2（析?。1? F2（蘊含）、F1?F2（等價）是FOTL公式。

公理3：如果F是FOTL公式，x是F中出現(xiàn)的變量即個體變元，則?x.F、?x.F是FOTL公式。

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

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

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

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

PTL公式和FOTL公式統(tǒng)稱為LTL公式。

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

5.基于LTL的形式化驗證模型設(shè)計

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

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

1）虛擬機運行狀態(tài)

2）VM_Exit事件處理

3）外部中斷處理

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

5）InterruptWindow計算

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

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

構(gòu)建虛擬機運行狀態(tài)模型

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

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

VM_Exit事件處理

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

外部中斷處理

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

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

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

InterruptWindow計算

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

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

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

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

：

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

解釋一下這個時序狀態(tài)機分為四部分：

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

vm是并發(fā)計算的語義描述

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

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

7.安全性驗證之程序終止性檢查

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

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

8.安全性驗證之程序正確性檢查

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

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

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

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

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

9.推廣建議

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