一種安全關(guān)鍵軟件系統(tǒng)符號(hào)執(zhí)行優(yōu)化方法

戴延軍，吳志強(qiáng)，劉 杰，劉朝暉，陳 智，肖安紅

(1.南華大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，湖南 衡陽(yáng) 421000;2.中國(guó)核動(dòng)力研究設(shè)計(jì)院核反應(yīng)堆系統(tǒng)設(shè)計(jì)技術(shù)國(guó)家級(jí)重點(diǎn)實(shí)驗(yàn)室，四川 成都 610000)

0 引 言

安全關(guān)鍵系統(tǒng)(Safety-Critical Systems, SCS)是指系統(tǒng)功能一旦失效將引起生命、財(cái)產(chǎn)的重大損失以及環(huán)境可能遭到嚴(yán)重破壞的系統(tǒng)[1]。此類系統(tǒng)廣泛存在于航空航天、核電及國(guó)防軍工等諸多安全關(guān)鍵領(lǐng)域?？刂栖浖前踩P(guān)鍵系統(tǒng)的重要組成部分[2]，高效的測(cè)試方法的研究是提高安全關(guān)鍵系統(tǒng)可靠性的重要途徑[3]。

符號(hào)執(zhí)行技術(shù)是一種重要的程序分析技術(shù),由King等[4]于1976年提出，其優(yōu)勢(shì)是能以較少的測(cè)試用例集獲得較高覆蓋率，從而探測(cè)軟件深層錯(cuò)誤。符號(hào)執(zhí)行將實(shí)際輸入用符號(hào)代替,程序的操作轉(zhuǎn)換為符號(hào)表達(dá)式操作，程序的執(zhí)行隨著遇到分支指令進(jìn)行分叉,以探索各分支,同時(shí)將分支條件加入到當(dāng)前路徑條件，通過(guò)約束求解判定路徑是否可行，若路徑條件有解,則表明路徑可行;反之,則終止該路徑分析。符號(hào)執(zhí)行的研究主要經(jīng)歷傳統(tǒng)符號(hào)執(zhí)行[4]→動(dòng)態(tài)符號(hào)執(zhí)行[5]→選擇符號(hào)執(zhí)行[6]的發(fā)展過(guò)程。

符號(hào)執(zhí)行生成測(cè)試用例優(yōu)勢(shì)明顯，但符號(hào)執(zhí)行工業(yè)應(yīng)用面臨著2個(gè)方面的困難和挑戰(zhàn):1)路徑爆炸問(wèn)題[7]，針對(duì)該問(wèn)題的相關(guān)研究較多，例如基于懶符號(hào)執(zhí)行的路徑求解算法[8]、控制流污點(diǎn)信息導(dǎo)向的符號(hào)執(zhí)行技術(shù)[9]、符號(hào)摘要方法[10]；2)約束求解困難[11]，這是符號(hào)執(zhí)行過(guò)程中最為耗時(shí)的部分,有研究表明其約占到執(zhí)行時(shí)間的40%～90%[12]。文獻(xiàn)[13]將多次約束求解合并成一次求解,從而減少約束求解消耗的時(shí)間,并使用蟻群算法提高路徑成功猜測(cè)率。文獻(xiàn)[14]使用機(jī)器學(xué)習(xí)的方法來(lái)簡(jiǎn)化復(fù)雜約束。文獻(xiàn)[15]使用擴(kuò)展的并行KLEE[16]約束求解器來(lái)縮短約束求解的時(shí)間。

安全關(guān)鍵軟件系統(tǒng)的模塊之間存在耦合性，這類系統(tǒng)直接使用符號(hào)執(zhí)行生成測(cè)試用例會(huì)遇到符號(hào)執(zhí)行技術(shù)工業(yè)應(yīng)用中的約束求解困難，這直接決定了符號(hào)執(zhí)行對(duì)這類系統(tǒng)生成測(cè)試用例的可能性。

約束求解困難是阻礙符號(hào)執(zhí)行工業(yè)應(yīng)用的重要因素，同時(shí)這類問(wèn)題是一個(gè)NP完全問(wèn)題，相關(guān)研究在解決這類通用問(wèn)題的基本思路是大約束化為小約束求解，其中較為突出的是約束獨(dú)立求解的思想[20]，即如果2個(gè)約束相互獨(dú)立，單獨(dú)求解即可。然而，安全關(guān)鍵系統(tǒng)的軟件耦合使得約束獨(dú)立優(yōu)化方法不能直接使用，局部解可能造成全局約束的不可解。為了在分割約束的過(guò)程中，各約束子集之間的依賴最小，以使分割后約束的可解性更高，本文提出一種帶權(quán)最小割集的分割方法對(duì)大約束進(jìn)行分割，這種帶權(quán)最小割集的優(yōu)化方法將軟件系統(tǒng)的各模塊解耦，降低約束求解的難度，使符號(hào)執(zhí)行能用到安全關(guān)鍵軟件耦合系統(tǒng)的測(cè)試用例生成。

1 安全關(guān)鍵軟件系統(tǒng)的耦合性

控制軟件是安全關(guān)鍵軟件系統(tǒng)的重要組成部分，在工業(yè)領(lǐng)域，常使用算法組態(tài)來(lái)建立控制算法模型。許多現(xiàn)代控制理論算法都是基于狀態(tài)空間描述或傳遞函數(shù)矩陣[17]，這種集中描述方式難用于實(shí)際的分布式工業(yè)過(guò)程。組態(tài)控制[18]的思路則不同，其通過(guò)簡(jiǎn)單的標(biāo)準(zhǔn)結(jié)構(gòu)單元(如積分器、基本PIO等)的任意連接組成復(fù)雜的控制算法，如前饋、串級(jí)和微分導(dǎo)前等。如圖1所示的圖形就是一個(gè)counter圖形組態(tài)，實(shí)現(xiàn)按周期加1的功能。安全關(guān)鍵控制系統(tǒng)由基本的組態(tài)搭建而成，組態(tài)之間共同變量的存在使得軟件存在耦合性。圖2所示為一個(gè)控制算法功能模塊的組態(tài)組合模型。耦合性是程序模塊之間關(guān)聯(lián)性的度量，它取決于各模塊間接口復(fù)雜程度、模塊調(diào)用方式和接口傳遞的信息。在安全關(guān)鍵系統(tǒng)中，存在4種耦合方式。

1)非直接耦合。

2個(gè)控制算法組態(tài)之間無(wú)直接關(guān)系，雙方的聯(lián)系通過(guò)主控模塊的控制和調(diào)節(jié)實(shí)現(xiàn)，此類耦合稱為非直接耦合。

圖1 counter圖形組態(tài)

圖2 控制算法組態(tài)模型

2)數(shù)據(jù)變量耦合。

當(dāng)2個(gè)組態(tài)之間通過(guò)數(shù)據(jù)變量傳遞信息時(shí)，則稱2個(gè)組態(tài)之間存在數(shù)據(jù)變量耦合。

3)控制參數(shù)耦合。

如果一個(gè)組態(tài)通過(guò)傳遞開關(guān)、標(biāo)示或其他枚舉值等控制信息，對(duì)另一組態(tài)的功能產(chǎn)生了影響，則這2個(gè)組態(tài)稱為控制參數(shù)耦合。

4)混合型耦合。

如果2個(gè)模塊之間既存在數(shù)據(jù)變量耦合，也存在混合型耦合，則稱這種耦合為混合型耦合。

安全關(guān)鍵系統(tǒng)的耦合性相當(dāng)復(fù)雜，但在使用組態(tài)的方式進(jìn)行建模的過(guò)程中，可以將復(fù)雜的耦合性概括為以上4種情況。實(shí)際生產(chǎn)中，大型系統(tǒng)通常會(huì)包含以上4種情況。

2 安全關(guān)鍵系統(tǒng)的符號(hào)執(zhí)行

組態(tài)開發(fā)方式也是基于模型開發(fā)思想的。通常這類系統(tǒng)不會(huì)手工編寫代碼，而是使用經(jīng)過(guò)相關(guān)認(rèn)證工具設(shè)計(jì)控制算法模型，然后生成通用高級(jí)語(yǔ)言[19](如C和Ada)。圖2所示的模型通常會(huì)轉(zhuǎn)換為一個(gè)通用高級(jí)語(yǔ)言的函數(shù)，每個(gè)單獨(dú)的算法塊也會(huì)轉(zhuǎn)換成等價(jià)的高級(jí)語(yǔ)言的函數(shù)，連線表示共同變量傳遞，即，設(shè)模型生成的函數(shù)OP(Pn)，其中，n為共同變量的個(gè)數(shù)，Pn={p1,p2，…，pn}為變量。設(shè)Fs(Qm)為基本算法塊生成的函數(shù)，其中，s為函數(shù)的個(gè)數(shù)，m為每個(gè)Fs包含的變量個(gè)數(shù)，F(xiàn)s={f1,f2，…，fs}，Qm={q1,q2，…，qm}，Q?P。對(duì)于2個(gè)函數(shù)F1和F2，如果Q1∩Q2=K≠?，則函數(shù)F1和F2存在依賴，且K為Q1和Q2的共同變量集。設(shè)符號(hào)執(zhí)行將OP(Pn)生成路徑約束公式C，每個(gè)單獨(dú)的函數(shù)fi生成路徑約束公式Ci，則對(duì)于安全關(guān)鍵系統(tǒng)符號(hào)執(zhí)行生成的路徑約束可表述如公式(1)所示：

(1)

定義1約束獨(dú)立。如果Ci和Cj不含共同變量，則約束Ci和Cj相互獨(dú)立，如x+y<3∧z>5。

定義2約束耦合。如果Ci和Cj包含共同變量，則約束Ci和Cj存在耦合，如x+y<3∧y>4。

安全關(guān)鍵軟件使用符號(hào)執(zhí)行生成路徑約束會(huì)包含定義1和定義2所示的2種情況。2個(gè)路徑約束公式要么相互獨(dú)立，要么包含共同變量出現(xiàn)約束耦合現(xiàn)象。組態(tài)所體現(xiàn)的4種耦合性最終會(huì)表現(xiàn)為約束耦合。

約束求解是一個(gè)NP完全問(wèn)題，引言部分已介紹通用的處理方法，其中，約束獨(dú)立求解的思想較為通用。然而，約束耦合使得約束獨(dú)立優(yōu)化無(wú)法直接使用。局部解可能造成全局約束的不可解，如x+y<3∧y>4∧y+z<3∧z>1，將y用5替換使得子公式x+y<3∧y>4可解，但對(duì)于y+z<3∧z>1不可解。如果不可解，則不進(jìn)行分割求解。為了在分割約束的過(guò)程中，各約束子集之間的依賴最小，以使分割后約束的可解性更高，本文提出一種帶權(quán)最小割集的分割方法對(duì)大約束進(jìn)行分割。

3 解約束耦合的優(yōu)化方法

圖3 約束的圖模型

算法1帶權(quán)最小割集Min_Weight_Constraint_Cut

輸入:約束集C

輸出:分割出的約束子集PC1和PC2

1. Min_Weight_Constraint_Cut(C)

2.For i←1 to |C|

3.圖G push Ci

4.For j←1 to |組合(|C|,2)|

5.s,t←組合序列(|C|,2)

6.If Vst=Cs∩Ct≠? Then

8.圖G push Eij

9.End If

10.End For

11.End For

12.Return PC1,PC2=MinimunCut(圖G)

算法重點(diǎn)處理約束的公共變量提取以及權(quán)值的計(jì)算，最小割集算法MinimunCut較為通用。由于變量在約束中出現(xiàn)的頻率會(huì)對(duì)約束的依賴產(chǎn)生影響，因此在求解最小依賴時(shí)需要考慮。

4 實(shí) 驗(yàn)

安全關(guān)鍵軟件耦合現(xiàn)象廣泛存在于此領(lǐng)域的各種軟件系統(tǒng)中。實(shí)驗(yàn)選取較為典型的核安全級(jí)儀控系統(tǒng)控制算法的功能模塊，從每個(gè)模塊中選取和其他模塊存在耦合性的路徑約束，算法塊和耦合約束圖模型統(tǒng)計(jì)信息如表1所示。實(shí)驗(yàn)工具為KLEE、CVC4和Z3[23]約束求解器，其中，KLEE是學(xué)術(shù)界和工業(yè)界較為成熟的符號(hào)執(zhí)行工具，CVC4[24]和Z3是學(xué)術(shù)界和工業(yè)界表現(xiàn)較好的約束求解器。實(shí)驗(yàn)對(duì)比了使用傳統(tǒng)的符號(hào)執(zhí)行工具KLEE+CVC4、KLEE+Z3求解器和使用KLEE+優(yōu)化算法+CVC4、KLEE+優(yōu)化算法+Z3所體現(xiàn)的求解時(shí)間上的優(yōu)勢(shì)。對(duì)比實(shí)驗(yàn)結(jié)果如表2所示，時(shí)間對(duì)比如圖4所示，分割后約束可滿足性如表3所示。從圖4可以看出，M1在不進(jìn)行符號(hào)約束優(yōu)化的情況下，CVC4所消耗的時(shí)間為53 ms，Z3所消耗的時(shí)間為34 ms。M4在不進(jìn)行符號(hào)約束優(yōu)化的情況下，CVC4所消耗的時(shí)間為113 ms，Z3所消耗的時(shí)間為86 ms。M1使用優(yōu)化算法后，CVC4求解的時(shí)間為35 ms，Z3求解時(shí)間為28 ms，求解的時(shí)間平均減少了25.80%。對(duì)于長(zhǎng)約束M4，CVC4和Z3所用時(shí)間分別為113 ms和86 ms，優(yōu)化后所用時(shí)間分別為101 ms和74 ms，求解時(shí)間平均減少了12.28%。M1～M4的平均求解時(shí)間減少了19.18%。大型系統(tǒng)通常會(huì)存在大量的這類約束耦合公式，處理多條路徑約束時(shí)間上會(huì)顯著減少。從表3可滿足性數(shù)據(jù)看出，由于考慮了變量在子公式出現(xiàn)的頻率，常量替換后的約束公式可滿足性比較接近直接求解。通過(guò)實(shí)驗(yàn)對(duì)比可以看到，帶權(quán)最小割集優(yōu)化分割一方面提高了約束求解的速度，另一方面也提高了約束分割后的可解性。

表1 核安全級(jí)儀控系統(tǒng)控制算法

控制算法算法塊數(shù)耦合約束圖模型M14M28M310M416

表2 時(shí)間對(duì)比結(jié)果 單位：ms

控制算法CVC4Z3優(yōu)化+CVC4優(yōu)化+Z3M153343528M271486140M374646244M41138610174

表3 帶權(quán)最小割集可滿足性

控制算法CVC4Z3優(yōu)化+CVC4優(yōu)化+Z3M1satsatsatsatM2satsatsatsatM3satsatsatsatM4satsatunsatsat

圖4 求解時(shí)間對(duì)比圖

5 結(jié)束語(yǔ)

對(duì)于安全關(guān)鍵系統(tǒng)而言，其可靠性需要通過(guò)大量的測(cè)試來(lái)進(jìn)行。符號(hào)執(zhí)行作為一種優(yōu)勢(shì)明顯的測(cè)試用例生成方式被用在自動(dòng)化測(cè)試方面。本文針對(duì)安全關(guān)鍵軟件系統(tǒng)的耦合性提出了一種基于最小割集的帶權(quán)約束分解方法。通過(guò)實(shí)驗(yàn)表明，優(yōu)化方法不僅提升了約束求解的速度，也提高了約束分割后的可解性。在以后的研究中，將對(duì)2個(gè)方面進(jìn)行改進(jìn)，一是對(duì)約束的分割方法進(jìn)行改進(jìn)，二是深度挖掘約束的變量之間的關(guān)系，使得分割后約束的可解性進(jìn)一步提高。