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通訊協議安全性驗證領域比較適合采取形式化驗證方法來保證軟件模型的正確性、可靠性。