基于Büchi自動機(jī)化簡的JavaMOP監(jiān)控器構(gòu)造方法

葉玲玲， 錢俊彥， 查顯偉

(桂林電子科技大學(xué) 計(jì)算機(jī)與信息安全學(xué)院，廣西 桂林 541004)

隨著軟件系統(tǒng)規(guī)模和復(fù)雜性的不斷增加，驗(yàn)證軟件系統(tǒng)正確性和安全性的難度也越來越大。對于大規(guī)模的軟件系統(tǒng)，傳統(tǒng)的驗(yàn)證技術(shù)(如模型驗(yàn)證[1]和測試[2])會出現(xiàn)狀態(tài)爆炸和難以覆蓋系統(tǒng)所有執(zhí)行分支等問題。運(yùn)行時驗(yàn)證[3-4]是一種輕量級的形式化驗(yàn)證方法，它根據(jù)軟件系統(tǒng)的實(shí)際執(zhí)行情況來驗(yàn)證系統(tǒng)的正確性，能夠?yàn)槿藗兲峁┫到y(tǒng)運(yùn)行時行為的準(zhǔn)確信息。運(yùn)行時驗(yàn)證技術(shù)通過分析系統(tǒng)的一個或多個執(zhí)行軌跡來驗(yàn)證系統(tǒng)，避免了傳統(tǒng)形式化驗(yàn)證技術(shù)復(fù)雜性高的問題。運(yùn)行時驗(yàn)證的核心部分是監(jiān)控器[3]，對系統(tǒng)進(jìn)行運(yùn)行時驗(yàn)證就是將待驗(yàn)證的系統(tǒng)置于監(jiān)控下，監(jiān)控器通過驗(yàn)證系統(tǒng)的執(zhí)行軌跡是否滿足給定的屬性來判斷系統(tǒng)是否正確。

近年來，為了確保軟件系統(tǒng)的正確性，運(yùn)行時驗(yàn)證得到了廣泛的應(yīng)用。Asadollah等[5]在多核并行軟件環(huán)境下，提出了一種基于運(yùn)行時驗(yàn)證的漏洞檢測模型，用于檢測系統(tǒng)故障；Incki等[6]運(yùn)用運(yùn)行時驗(yàn)證技術(shù)來防止物聯(lián)網(wǎng)中的網(wǎng)絡(luò)攻擊。然而，對系統(tǒng)進(jìn)行運(yùn)行時驗(yàn)證，通常會產(chǎn)生一些額外的驗(yàn)證開銷，因此，減少運(yùn)行時驗(yàn)證工具的監(jiān)控開銷成為了一個非常重要的研究內(nèi)容。

為了減少運(yùn)行時驗(yàn)證的開銷，Reger等[7]提出MARQ驗(yàn)證工具，通過索引技術(shù)和對監(jiān)控對象的冗余刪除來減少運(yùn)行時開銷；Reger[8]運(yùn)用靜態(tài)分析去除運(yùn)行時驗(yàn)證不可達(dá)對象，減少需檢測的對象，從而減少監(jiān)控開銷；Chen等[9]提出了弱監(jiān)控性的定義，排除不可監(jiān)控的屬性，以減少運(yùn)行時監(jiān)控開銷。這些控制運(yùn)行時驗(yàn)證開銷的方法，主要考慮的是找到并刪除無用的監(jiān)控對象。為了達(dá)到減少運(yùn)行時監(jiān)控開銷的目的，還可以對JavaMOP[10]、TraceMatches[11]等運(yùn)行時驗(yàn)證工具生成監(jiān)控器代碼的過程進(jìn)行優(yōu)化，進(jìn)而控制監(jiān)控器在構(gòu)造過程中的開銷。鑒于此，提出一種基于Büchi自動機(jī)化簡的監(jiān)控器構(gòu)造方法,降低JavaMOP運(yùn)行時驗(yàn)證的時間和內(nèi)存開銷。

1 相關(guān)知識

1.1 線性時態(tài)邏輯

線性時態(tài)邏輯(linear temporal logic，簡稱LTL)是一種與時間有關(guān)的模態(tài)時序邏輯。引入LTL公式來描述系統(tǒng)行為屬性，通過使用原子命題、析取操作符(∨)、next算子(X)、until算子(U)和否定操作符號()定義LTL公式的集合。

定義2(LTL語義) 令u=u0u1…∈Σω是一個無限狀態(tài)序列，且Σ=2P，u滿足LTL公式φ，當(dāng)且僅當(dāng)uφ，LTL公式的語義定義為：

utrue；

up，當(dāng)且僅當(dāng)p∈u；

uφ，當(dāng)且僅當(dāng)u/φ；

uφ1∨φ2，當(dāng)且僅當(dāng)uφ1或者uφ2；

uφ1∧φ2，當(dāng)且僅當(dāng)uφ1且uφ2；

uXφ，當(dāng)且僅當(dāng)ui+1φ；

uφ1Uφ2，當(dāng)且僅當(dāng)?k≥0,ukuk+1…φ2和?0≤i

使用這些定義能夠推導(dǎo)出eventually算子(F)、always算子(G)和release算子(R)：Fφ等價(jià)于trueUφ；Gφ等價(jià)于Fφ；φ1Rφ2等價(jià)于(φ1Uφ2)。

1.2 Büchi自動機(jī)

Büchi自動機(jī)是ω自動機(jī)的一種，它將有限狀態(tài)自動機(jī)擴(kuò)展到無限，接受一個無限的輸入序列，可以替代和處理ω正則語言。由于Büchi自動機(jī)在布爾操作[12]下是封閉的，它常被用于基于自動機(jī)的形式化驗(yàn)證方法。

定義3(Büchi自動機(jī)) Büchi自動機(jī)是一個五元組B=(Σ,Q,I,δ,F)。其中：Σ為非空有限字母表，且Σ′?2Σ；δ?Q×2Σ′×Q是遷移關(guān)系；Q為非空有限狀態(tài)集合；I?Q為初始狀態(tài)集合；F?Q為接受狀態(tài)集合。

1.3JavaMOP

JavaMOP是一種基于Java語言、支持軟件開發(fā)與分析的運(yùn)行時驗(yàn)證工具，它支持多種邏輯，如線性時態(tài)邏輯(LTL)、上下無關(guān)文法(CFG)、擴(kuò)展正則表達(dá)式(ERE)等，并將形式化規(guī)約以邏輯插件的形式集成在JavaMOP工具中，實(shí)現(xiàn)對不同形式化規(guī)約的監(jiān)控。其中，LTL插件用于驗(yàn)證軟件系統(tǒng)運(yùn)行時是否滿足給定的LTL屬性。JavaMOP是目前最高效的運(yùn)行時驗(yàn)證工具之一，在軟件運(yùn)行時驗(yàn)證中，將LTL語言描述的屬性轉(zhuǎn)換成監(jiān)控器代碼插裝到待監(jiān)控的系統(tǒng)程序中，實(shí)現(xiàn)實(shí)時監(jiān)控系統(tǒng)程序的運(yùn)行并返回監(jiān)控結(jié)果。JavaMOP運(yùn)行時監(jiān)控軟件系統(tǒng)程序的過程如圖1所示。

圖1 JavaMOP運(yùn)行時監(jiān)控軟件系統(tǒng)程序的過程

JavaMOP在驗(yàn)證軟件系統(tǒng)時，根據(jù)給定的屬性規(guī)約會自動生成相應(yīng)的監(jiān)控器代碼，并插裝到目標(biāo)程序中進(jìn)行實(shí)時監(jiān)控。JavaMOP生成監(jiān)控器基于自動機(jī)的驗(yàn)證算法，對于給定的LTL屬性，通過轉(zhuǎn)換算法[13]將LTL公式轉(zhuǎn)化為Büchi自動機(jī)，再將Büchi自動機(jī)轉(zhuǎn)化為確定性有限自動機(jī)(determine finite automata，簡稱DFA)，生成監(jiān)控器的抽象表示，之后得到監(jiān)控器代碼，實(shí)現(xiàn)對軟件系統(tǒng)程序驗(yàn)證的功能。

2 自動機(jī)化簡規(guī)則與算法

在生成監(jiān)控器的過程中，減小Büchi自動機(jī)的大小，能夠減少內(nèi)存消耗并加快監(jiān)控器代碼的生成。為此，提出自動機(jī)化簡規(guī)則對由LTL公式轉(zhuǎn)化得到的Büchi自動機(jī)進(jìn)行化簡。首先對自動機(jī)中接受語言為空的狀態(tài)進(jìn)行移除操作；再將滿足合并規(guī)則的狀態(tài)進(jìn)行合并化簡，使得目標(biāo)Büchi自動機(jī)最小化。

規(guī)則1(移除規(guī)則) 設(shè)Büchi自動機(jī)B=(Σ,Q,I,δ,F)，對自動機(jī)中的任一狀態(tài)q，若從狀態(tài)q開始的自動機(jī)接受語言為空，則狀態(tài)q為冗余狀態(tài)可移除。

規(guī)則1即取自動機(jī)中的任意一個狀態(tài)，判斷Büchi自動機(jī)接受的語言是否為空，若接受的語言為空，則進(jìn)行冗余標(biāo)記，并移除操作將其刪除。移除冗余算法描述如下。

算法1RemoveRedundant(B)

輸入：Büchi自動機(jī)B=(Σ,Q,I,δ,F)；

輸出：新的Büchi自動機(jī)B′=(Σ′,Q′,I′,δ′,F′)，且有L(B′)=L(B)。

1 fors∈Qdo；

2 計(jì)算從狀態(tài)s出發(fā)的后繼狀態(tài)集合nodes(s)；

3 if nodes(s)∩F=? then//狀態(tài)s開始的自動機(jī)語言為空；

4 標(biāo)記狀態(tài)s為冗余狀態(tài)；

5 移除狀態(tài)s；

6 返回Büchi自動機(jī)B′。

規(guī)則2(合并規(guī)則) 設(shè)Büchi自動機(jī)中狀態(tài)a和狀態(tài)b都有n條遷移關(guān)系，若狀態(tài)a的下一個狀態(tài)是b,且狀態(tài)a遷移到狀態(tài)b的條件也是狀態(tài)b的自旋條件，同時狀態(tài)a剩下n-1條遷移與狀態(tài)b的另外n-1遷移相同，則狀態(tài)a和狀態(tài)b可以合并。

合并規(guī)則對自動機(jī)冗余刪除后進(jìn)一步化簡自動機(jī)，用于得到狀態(tài)數(shù)更少的自動機(jī)。首先將自動機(jī)中的狀態(tài)集分為2個集合S1和S2，集合S1用于存儲接受狀態(tài)，集合S2存儲除了接受狀態(tài)的自動機(jī)狀態(tài)；然后分別對集合S1和集合S2中的狀態(tài)s和s′進(jìn)行判斷，是否符合合并規(guī)則；若滿足，則可將狀態(tài)s′合并到狀態(tài)s，狀態(tài)s′的環(huán)移動到狀態(tài)s。具體執(zhí)行過程如下。

算法2Merge(B)

輸入：Büchi自動機(jī)B′=(Σ′,Q′,I′,δ′,F′)；

輸出：新的Büchi自動機(jī)B″=(Σ″,Q″,I″,δ″,F″)，且有L(B″)=L(B′)。

1 fors∈Qdo；

2 ifs∈Fthen；

3S1:=S1∪s//把s加入到接受狀態(tài)集合S1中；

4 else；

5S2:=S2∪s//把s加入到非接受狀態(tài)集合S2中；

6 //對S1集合中狀態(tài)進(jìn)行合并操作；

7 fors∈S1do；

8 fors′∈S1do；

9 ifs,s′滿足合并規(guī)則 then；

10 合并狀態(tài)s和狀態(tài)s′；

11 //對S2集合中狀態(tài)進(jìn)行合并操作；

12 fors∈S2do；

13 fors′∈S2do；

14 ifs，s′滿足合并規(guī)則then；

15 合并狀態(tài)s和狀態(tài)s′；

16 返回Büchi自動機(jī)B″。

圖2為運(yùn)用合并規(guī)則化簡自動機(jī)狀態(tài)的例子。使用一個三元組δ表示2個狀態(tài)之間的遷移關(guān)系，如δ=(s1,c,s2)表示從狀態(tài)s1遷移到狀態(tài)s2的條件是c。圖2(a)為化簡之前的自動機(jī)，它有6個狀態(tài)和13條遷移關(guān)系，其中狀態(tài)s0有3條遷移關(guān)系δ1=(s0,a,s1)，δ2=(s0,c,s2)，δ3=(s0,b,s3)。狀態(tài)s1也有3條遷移關(guān)系δ4=(s1,a,s1)，δ5=(s1,c,s2)，δ6=(s1,b,s3)。狀態(tài)s0遷移到狀態(tài)s1與狀態(tài)s1到自身的條件相同，并且剩下的2條遷移也相同，因此，狀態(tài)s0和s1滿足合并規(guī)則，可將s0與s1合并。同樣地，狀態(tài)s3和s4滿足合并規(guī)則，可以合并。化簡得到新的自動機(jī)如圖2(b)所示，它包含4個狀態(tài)和7條遷移關(guān)系，與化簡前相比簡單了很多。

圖2 運(yùn)用合并規(guī)則化簡自動機(jī)的例子

3 實(shí)驗(yàn)與分析

為了驗(yàn)證自動機(jī)化簡規(guī)則的可行性，用Java語言實(shí)現(xiàn)了基于自動機(jī)的監(jiān)控器構(gòu)造過程，并與JavaMOP中原有構(gòu)造運(yùn)行時監(jiān)控器的方法進(jìn)行比較。為了使2種監(jiān)控器構(gòu)造方法的實(shí)驗(yàn)數(shù)據(jù)具有可比性和公平性，采用相同的測試用例，所有實(shí)驗(yàn)在相同的環(huán)境下進(jìn)行。實(shí)驗(yàn)運(yùn)行環(huán)境的配置如下：處理器為Inter (R) Core (TM) i5-4690 CPU@3.5 GHz和內(nèi)存為8 GiB的臺式電腦，電腦配備的操作系統(tǒng)為Ubuntu 14.04，同時配置了Sun Java SE 8環(huán)境。使用DaCapo[14]數(shù)據(jù)集，選取其中4個測試屬性作為實(shí)驗(yàn)的測試對象，分別為：

HasNext：對于每個迭代器對象，要求在執(zhí)行函數(shù)next()前調(diào)用函數(shù)hasnext()，并且hasnext()的返回值為true；

SafeSyncColl：若一個集合是同步的，則它的迭代器也應(yīng)是同步訪問的；

UnSafeIterator：在使用迭代器接口迭代集合元素時不能更新集合元素；

UnSafeMapIterator：在集合上對映射的鍵值迭代時，Map無法進(jìn)行更新操作。

表1為2種監(jiān)控器構(gòu)造方法的性能比較。從表1可看出，在內(nèi)存開銷方面，化簡Büchi自動機(jī)能夠減少運(yùn)行時監(jiān)控器在構(gòu)造過程中的內(nèi)存消耗；在時間開銷上，簡化的Büchi自動機(jī)加速了生成監(jiān)控器的過程，從而節(jié)省了構(gòu)造監(jiān)控器代碼的時間，降低了整個監(jiān)控器構(gòu)造的時間開銷。對于測試的屬性HasNext，化簡操作前JavaMop時間和內(nèi)存開銷分別為92.88 s和629.71 MiB，本方法時間和內(nèi)存開銷分別為89.92 s和612.23 MiB，在時間和內(nèi)存開銷分別降低了3.19%和2.78%。對于屬性UnSafeIterator，本方法時間和內(nèi)存開銷分別降低4.93%和5.32%，比屬性HasNext性能提升更多，這是因?yàn)閷傩訳nSafeIterator操作更加復(fù)雜，經(jīng)過化簡操作后移除和約減的狀態(tài)和遷移關(guān)系更多，因此，性能提升也相對更多。

表1 2種監(jiān)控器構(gòu)造方法的性能比較

4 結(jié)束語

對于運(yùn)行時驗(yàn)證中基于自動機(jī)理論構(gòu)造監(jiān)控器的方法，通過化簡Büchi自動機(jī)來減小運(yùn)行時驗(yàn)證在監(jiān)控器構(gòu)造過程中的時間和內(nèi)存開銷，能夠提高監(jiān)控器生成的效率和運(yùn)行時驗(yàn)證的性能。針對運(yùn)行時驗(yàn)證工具JavaMOP中構(gòu)造監(jiān)控器的方法進(jìn)行研究實(shí)驗(yàn)，實(shí)驗(yàn)結(jié)果表明，本方法在提升運(yùn)行時監(jiān)控性能上有一定的效果。今后研究監(jiān)控器代碼生成后對程序進(jìn)行實(shí)時監(jiān)控過程中監(jiān)控算法的優(yōu)化，提高監(jiān)控算法效率，以進(jìn)一步降低運(yùn)行時驗(yàn)證的時間和內(nèi)存開銷。