臧偉旺，朱健

（南京電子技術(shù)研究所，江蘇 南京 210039）

0 引 言

隨著雷達(dá)系統(tǒng)不斷發(fā)展，以及結(jié)構(gòu)工藝的優(yōu)化提高，對雷達(dá)軟件設(shè)計(jì)提出了更高的要求，其中，軟件的安全性與可靠性尤為重要，影響著整個(gè)雷達(dá)系統(tǒng)的行為是否符合預(yù)期以及性能的高低。傳統(tǒng)的測試仿真方法可以有效提高軟件的可靠性，但無法遍歷所有的執(zhí)行路徑，從而不能證明一個(gè)軟件沒有漏洞。因此，需要引入形式化方法來保證軟件的安全性。

形式化方法是一種基于數(shù)理邏輯的軟硬件設(shè)計(jì)方法，也是目前安全關(guān)鍵軟件系統(tǒng)的一種嚴(yán)格的驗(yàn)證技術(shù)。通過形式化邏輯的方式來表示合約代碼，并加以嚴(yán)格地推理證明。這個(gè)過程依賴于數(shù)學(xué)邏輯推理的嚴(yán)密性，保證100%覆蓋到代碼的運(yùn)行行為，可以保證在一定范圍內(nèi)的絕對正確?；谛问交椒ǖ难芯吭谝恍┌踩P(guān)的領(lǐng)域，如雷達(dá)、核電、航空、區(qū)塊鏈等已經(jīng)逐步得到應(yīng)用，并且取得了非常好的效果。

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

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

1 總體轉(zhuǎn)換方法

我們提出基于形式模型的C 程序建模與驗(yàn)證方法，如圖1所示，一個(gè)C 程序主要包括賦值語句、條件語句、循環(huán)語句以及函數(shù)結(jié)構(gòu)，我們?yōu)槊恳粋€(gè)元素建立了與其語義保持一致的形式模型。其中，我們考慮C 語言子集包括：

圖1 C 程序建模與驗(yàn)證方法

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

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

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

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

目標(biāo)形式模型基于一階邏輯，其語法包括：

（1）量化符號?和?；

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

（3）括號、方括號以及其他自定義標(biāo)點(diǎn)符號；

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

（5）等式符號=。

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

2 轉(zhuǎn)換規(guī)則

2.1 輔助運(yùn)算子

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

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

2.2 形式化規(guī)約

下面分別給出賦值語句、條件語句、循環(huán)語句以及函數(shù)的轉(zhuǎn)換規(guī)則。

規(guī)定賦值語句的轉(zhuǎn)化規(guī)則如下：

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

規(guī)定條件語句的轉(zhuǎn)換規(guī)則如下：

即，首先將C 的條件語句轉(zhuǎn)為0（false）和非0（true），然后基于一階邏輯進(jìn)行析取操作，當(dāng)循環(huán)條件不滿足時(shí)候，規(guī)定蘊(yùn)含true，表示跳出循環(huán)

規(guī)定循環(huán)語句的轉(zhuǎn)換規(guī)則如下，其中表示的后繼。

即，構(gòu)造一個(gè)自然數(shù)到集合{?（），?（?（）），…}的映射，每個(gè)?（）函數(shù)對Cond（）進(jìn)行判斷并析取操作。存在某個(gè)自然數(shù)使得其對應(yīng)的{?（），?（?（）），…}的某個(gè)值為p2 語句的執(zhí)行，跳出循環(huán)。

下面考慮函數(shù)定義的轉(zhuǎn)換規(guī)則：

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

第一種：

其中，_為返回值的類型，為參數(shù)類型，默認(rèn)無參數(shù)為true，body 為函數(shù)體，為函數(shù)返回值。

第二種：

使用蘊(yùn)含的形式，類似霍爾邏輯，表示經(jīng)過函數(shù)體的執(zhí)行后可以蘊(yùn)含函數(shù)值的類型

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

函數(shù)體內(nèi)每調(diào)用一次其他函數(shù)，則觸發(fā)該映射，生成新的全局變量映射g，和當(dāng)前自然數(shù)x 一一對應(yīng)，當(dāng)＞，保證了g和之前的所有g（≤）不一樣，用于保存調(diào)用函數(shù)的局部變量。如果是對全局變量更新，則對進(jìn)行更新。

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

首先用一階邏輯描述遞歸不動點(diǎn)定理，首先定義連續(xù)函數(shù)的集合：

然后描述不動點(diǎn)定理：

即任何連續(xù)函數(shù)都存在不動點(diǎn)。使用lambda 演算來表示上述形式函數(shù)，則，取參數(shù)，后的演算結(jié)果為

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

3 實(shí)例演示

以一個(gè)簡單的C 程序?yàn)槔?，如?所示，該程序包含賦值語句、條件語句、循環(huán)語句以及兩個(gè)函數(shù)，其中一個(gè)函數(shù)是inf_1，遞歸調(diào)用自身，另外一個(gè)是main 函數(shù)，作為C程序的啟動入口，其中調(diào)用inf_1 函數(shù)。C 程序案例：

根據(jù)上節(jié)給出的轉(zhuǎn)換規(guī)則，可以得到基于一階邏輯的形式模型：

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

4 結(jié) 論

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