基于雷達軟件安全的C程序到形式模型的轉換方法

臧偉旺，朱健

（南京電子技術研究所，江蘇 南京 210039）

0 引 言

隨著雷達系統不斷發展，以及結構工藝的優化提高，對雷達軟件設計提出了更高的要求，其中，軟件的安全性與可靠性尤為重要，影響著整個雷達系統的行為是否符合預期以及性能的高低。傳統的測試仿真方法可以有效提高軟件的可靠性，但無法遍歷所有的執行路徑，從而不能證明一個軟件沒有漏洞。因此，需要引入形式化方法來保證軟件的安全性。

形式化方法是一種基于數理邏輯的軟硬件設計方法，也是目前安全關鍵軟件系統的一種嚴格的驗證技術。通過形式化邏輯的方式來表示合約代碼，并加以嚴格地推理證明。這個過程依賴于數學邏輯推理的嚴密性，保證100%覆蓋到代碼的運行行為，可以保證在一定范圍內的絕對正確。基于形式化方法的研究在一些安全攸關的領域，如雷達、核電、航空、區塊鏈等已經逐步得到應用，并且取得了非常好的效果。

常見雷達軟件編程語言如C 語言可以編寫可執行程序，具有圖靈完備屬性，實現較為復雜的功能，但是其安全性較差，容易產生漏洞，如整數溢出、數組越界、函數重入等等，從而給軟件安全帶來潛在的威脅，造成不可預料的損失。一階邏輯是具有明確語法和語義的形式語言，且具有豐富的表達能力，可用于規約、定理證明和模型檢測。

本文提出從C 程序到基于一階邏輯的形式模型的轉換方法，首先定義了C 語言的核心子集，通過定義輔助運算子，給出了保持語義一致的映射關系，從而使用基于一階邏輯的形式模型來規約C 程序語言，包括賦值語句、條件語句、循環語句以及函數的規約，指導生成的形式模型可以自動地被驗證工具執行并驗證程序的正確性，有效提高了C 程序的安全性，以及程序驗證的效率。

1 總體轉換方法

我們提出基于形式模型的C 程序建模與驗證方法，如圖1所示，一個C 程序主要包括賦值語句、條件語句、循環語句以及函數結構，我們為每一個元素建立了與其語義保持一致的形式模型。其中，我們考慮C 語言子集包括：

圖1 C 程序建模與驗證方法

（1）賦值語句：{p1, v=e, p2},其中p1,p2 表示賦值語句執行前后的程序，v 表示程序變量，e 為表達式；

（2）條件語句if: {p1,if (Cond(v)) e1 else e2,p2},其中Cond(v),表示從包含變量集合v 的布爾表達式到true 或者false 布爾值的映射，e1,e2 為語句集合；

（3）循環語句while：{p1, while(Cond(v)){e},p2}，其中e 為循環體內部語句集合；

（4）函數定義{p1,return_t func_name(para_list){e},p2},其中return_t 為函數返回值類型，func_name 為函數名，para_list 為包含參數類型和參數名的列表，e 表示函數體的語句集合。

目標形式模型基于一階邏輯，其語法包括：

（1）量化符號?和?；

（2）邏輯連接詞蘊含→、否定?、雙條件?、且∧以及或∨；

（3）括號、方括號以及其他自定義標點符號；

（4）集合的變量，通常標記為英文字母的小寫形式如，，等；

（5）等式符號=。

對于程序而言，用戶最關心的是程序的安全屬性是否得到滿足，如類型檢查、可達性、死鎖、無狀態二義性等。通過轉換規則，可以使用基于一階邏輯的形式語言對程序建模以及對期望屬性規約。當得到形式模型后，可以進行模型轉換，轉換為更加復雜的形式模型。同時，借助驗證平臺，如Rodin，Isabelle，SPIN 等證明工具對模型進行驗證與仿真。通過工具提供的交互式定理證明助手，自動驗證生成的證明義務，從而驗證模型是否滿足給定的屬性。對于一些狀態比較簡單的模型，可以通過模型檢測工具，對狀態空間進行搜索窮舉，如果找到反例，則需要修改C 程序，反之，則通過驗證。

2 轉換規則

2.1 輔助運算子

我們首先定義ξ 操作符表示公式具有良好的條件。比如ξ（÷）：≠0，定義：

因此，可以定義＜+=∪（dom（）*），表示使用映射關系集合來更新集合中映射關系。更新表示如果有相同變量，則用中該變量的值來替代，如果中有新的變量，則引入該變量到該值的映射關系。

2.2 形式化規約

下面分別給出賦值語句、條件語句、循環語句以及函數的轉換規則。

規定賦值語句的轉化規則如下：

即，C 語言的賦值語句轉換為一階邏輯中對全局變量映射關系集合中變量的更新。

規定條件語句的轉換規則如下：

即，首先將C 的條件語句轉為0（false）和非0（true），然后基于一階邏輯進行析取操作，當循環條件不滿足時候，規定蘊含true，表示跳出循環

規定循環語句的轉換規則如下，其中表示的后繼。

即，構造一個自然數到集合{?（），?（?（）），…}的映射，每個?（）函數對Cond（）進行判斷并析取操作。存在某個自然數使得其對應的{?（），?（?（）），…}的某個值為p2 語句的執行，跳出循環。

下面考慮函數定義的轉換規則：

（1）函數自身沒有調用其他函數（包括自己），形如：{p1, return_tfunc_name(para_list){body; return e},p2}，這里給出兩種形式的轉換規則。

第一種：

其中，_為返回值的類型，為參數類型，默認無參數為true，body 為函數體，為函數返回值。

第二種：

使用蘊含的形式，類似霍爾邏輯，表示經過函數體的執行后可以蘊含函數值的類型

（2）函數調用其他函數，形如：{p1,return_t func_name(para_list){func1(para) ;body},p2}

函數體內每調用一次其他函數，則觸發該映射，生成新的全局變量映射g，和當前自然數x 一一對應，當＞，保證了g和之前的所有g（≤）不一樣，用于保存調用函數的局部變量。如果是對全局變量更新，則對進行更新。

（3）函數遞歸調用自身，形如：{p1,return_t func_name(para_list){func_name(para_list) ;body},p2}

首先用一階邏輯描述遞歸不動點定理，首先定義連續函數的集合：

然后描述不動點定理：

即任何連續函數都存在不動點。使用lambda 演算來表示上述形式函數，則，取參數，后的演算結果為

所以定義自然數集合到集合{（），（（）），…}的映射，表示遞歸的次數不斷增加。

3 實例演示

以一個簡單的C 程序為例，如表1所示，該程序包含賦值語句、條件語句、循環語句以及兩個函數，其中一個函數是inf_1，遞歸調用自身，另外一個是main 函數，作為C程序的啟動入口，其中調用inf_1 函數。C 程序案例：

根據上節給出的轉換規則，可以得到基于一階邏輯的形式模型：

該模型是基于一階邏輯，與同樣基于集合論的Event-B模型具有等價的語義，但是本文生成的形式模型比Event-B 模型的語法更加簡單。因此，可以考慮將形式模型轉換到Event-B 模型，借助Rodin 平臺對Event-B 模型進行定理證明和模型檢測。同樣，有限狀態機模型也是基于一階邏輯，因此可以考慮將本文的形式模型轉換到有限狀態機模型，從而借助狀態機可視化模型中狀態的遷移過程。

4 結 論

本文以雷達軟件安全為背景，研究了從C 程序到基于一階邏輯的形式模型的轉換方法，選取C 程序核心語法子集為對象，通過定義輔助運算子，建立了保持語義一致的映射關系，生成C 程序對應的形式模型，該模型是基于一階邏輯語法的可執行模型，從而借助驗證平臺自動地進行定理證明和進行模型檢測，驗證了C 程序的屬性，提高了程序的安全性。未來將進一步提高轉換的自動化程度，實現自動轉換的工具，并擴大C 程序的子集范圍，該方法已經針對運用C程序語言的雷達系統進行了檢驗，對軟件的測試更加充分，減少漏洞風險，具有重要的應用價值。