形式化驗證簡析

本部落格是我發表在就技術來說，鴻蒙OS到底是個什麼層面的東西？上的科普形式化驗證的文章。我將其轉載到此處，方便更多人看到。

我目前做的工作是基於微核心OS來做無人機整體系統的安全性方面的研究，需對微核心進行形式化驗證。因為形式化驗證方法很多，驗證工具也有很多。在此我只能就我所研究的內容談一談。

什麼是形式化驗證：

所謂形式化驗證是指採用形式化方法對計算機軟體或硬體進行驗證的過程。而形式化方法是基於嚴格的數學基礎，對計算機硬體和軟體系統進行描述，開發和驗證的技術。其數學基礎是建立在形式語言、語義和推理證明三位一體的形式邏輯系統之上。正是由於形式化方法的數學嚴格性使得經過形式化驗證的程式安全性得以保證。

理論上形式化驗證的開發過程

原本的程式開發過程應該是從抽象到具體，先提出Requirements，再不斷加入開發過程中的細節知識，稱為Specifications，最後不斷求精（具體化）得到最終的程式：

這裡的每一個箭頭都表示一次精化（Refinement），其中每一個Spec（Specification）的抽象角度和層次是不同的。簡單的來說我們只需要證明最後的程式滿足最初提出的Requirements就完成了證明，這就要求我們最先提出的requirements是完全正確的。再驗證每一步的Refinement（或者稱作Transformation Step）是保持正確性的（Preserve Correctness）就可以驗證最後得到的程式是滿足Requirements的。 所以可以看出提Requirement和寫Specification是非常重要也是形式化驗證中最為困難的。

實際中形式化驗證怎麼做

實際應用中，我們往往是已經有了程式，而不是一步一步從Requirement逐步精化得到的，那對於這樣的程式，我們怎麼對它進行形式化驗證？

這裡，我們採用的是耶魯大學的FLINT實驗室提出的基於Deep Spec的形式化驗證方法。

將我們已有的OS進行分層；

在Coq中寫出每一層中所有函式的Specification；

使用可信編譯器CompCert提供的ClightGen將每個c程式碼函式轉換為Clight語言對應的函式（也就是在Coq中將C語言程式碼進行描述），因為Clight語言是C語言的子集去除了side-effect 所以我們可能需要對C程式碼進行調整以便驗證的順利進行。

與Clight相同抽象級別寫出C程式碼的函式LowSpec，因為它們處在同一抽象層，所以我們可以驗證該Clignt函式（也就是C函式，因為它們等價）和LowSpec之間的關係是identity的。

為LowSpec和HighSpec定義抽象關係包括資料和記憶體狀態兩個方面的關係

驗證它們之間確實滿足這樣的抽象關係

這樣就完成了一個層基本的證明。

最後需要使用Layer Calculate將所有驗證的層Link到一起得到從bottom到top的經過連結的完整OS，最後利用Coq的Extraction提取出可執行程式就得到了經過驗證的OS。

實際操作起來可不止這麼簡單，還需要考慮OS的部分程式碼是彙編寫的，需要處理彙編層和普通層之間的關係等等複雜的事情。

為什麼形式化驗證能做到Bug-free

首先Bug是由於我們的C程式碼函式沒有完成我們想讓它完成的工作，而做了不該做的事情從而被駭客利用。形式化驗證中為函式寫Specification就是使用數學語言描述函式應該做的事情，因為數學語言是嚴格的，不像自然語言那樣存在歧義所以一旦驗證了C程式碼程式確實和我們的Specification擁有某種數學關係，那就說明我們的程式滿足Specification。

總結

這裡只是簡單的對形式化驗證的實際應用過程做了描述。失去了很多的嚴謹性，所以有什麼錯誤或遺漏的滴地方還請各位諒解與補充，不慎感激。有想深入探討的可以繼續交流。