?

一種檢測控制流錯誤的多層分段標簽方法

2020-08-17 13:59鄭偉寧顧浩為
計算機與現代化 2020年8期
關鍵詞:控制流前驅O型

鄭偉寧,莊 毅,顧浩為

(1.南京航空航天大學計算機科學與技術學院,江蘇 南京 211106; 2.中華中學,江蘇 南京 211106)

0 引 言

在計算機運行過程中,因為信號或者數據不正確造成的故障被稱為軟錯誤[1]。導致軟錯誤的原因有多種,從電路設計出現問題到元件之間相互干擾,乃至于空間輻射均有可能造成軟錯誤[2]。軟錯誤會改變寄存器或數據存儲器中的值,從而導致處理器將程序帶入錯誤循環或者直接進入死循環無法跳出。雖然軟錯誤通常不會對硬件電路造成永久性損壞,但仍會造成嚴重的后果。比如,2000年,美國SUN UNIX因緩存出現軟錯誤而影響了全美數十個服務器的正常工作,造成了數百萬美元的經濟損失;2011年,我國首顆火星探測衛星“螢火一號”升空后,由于負責運載的俄方Fregat上級控制系統遭受空間粒子輻射誘發軟錯誤,致使火星探測失敗。在其他領域,如工業生產、民用設施,軟錯誤也在不同程度上影響了電子設備的正常運行,降低了系統的可靠性。而根據應用場景的不同,對計算機的可靠性要求也不相同。例如發生在衛星控制系統上的錯誤比發生在視頻游戲中的錯誤造成的后果更加嚴重。因此,在設計加固方案時需要綜合考慮應用場景、加固效果、需求成本等多方面因素。所以在性能受限的平臺上,及時有效地對軟錯誤進行檢測恢復,針對計算機系統進行軟錯誤加固,減少故障的發生以提高系統的可靠性具有重要的意義。開發一種能夠有效檢測軟件中軟錯誤,同時檢測成本較低,可以被接受的檢測系統,也是目前的研究重點。

本文著眼于解決軟錯誤中控制流錯誤的檢測問題。程序控制流錯誤是軟錯誤的一大類型,根據Zhu等人[3]和Ohlsson等人[4]的實驗結果可知,在程序發生的軟錯誤中,有33%~77%的可能性造成程序的控制流錯誤。當高能粒子在與程序調用地址相關的位置引發故障時,就有可能造成控制流錯誤[5]。對于任何計算機程序,只要給程序輸入,其內部執行指令的順序就是固定的,但是控制流錯誤會改變這種順序,從而影響程序的正確執行[6]。目前檢測控制流錯誤的軟件技術通常是維護并更新一個全局的動態變量,通過監測變量的變化間接監控程序的控制流,這一變量也就是標簽。這種技術也被稱為基于標簽實現的控制流錯誤檢測技術[7]。

1 研究現狀

目前國內外對控制流檢測技術已經有了許多研究成果。Yau等人[8]在1980年提過一種使用數據庫來記錄程序控制流的方法,但是這種方法需要維護一個數據庫且不同程序控制流信息不同,最終會導致數據庫不斷擴充,開銷太高。該方法雖然本身存在著局限性,但是它提出了一種程序無循環間隔的概念,這一概念就是程序基本塊劃分的前身。ECCA(Enhanced Control-flow Checking using Assertions)也屬于早期軟件實現的控制流錯誤檢測方法,該方法通過在程序無分支間隔的入口和出口處插樁斷言來檢測錯誤[9]。此文獻中的無分支間隔和斷言與后來的基本塊和標簽已經非常接近了,但是由于更新操作采用乘除法,并且插樁的斷言本身較為復雜,會產生較大的開銷。CFCSS(Control-Flow Checking by Software Signatures)是基于標簽實現的控制流錯誤檢測方法中最為經典的方法,它將程序執行的指令劃分為眾多集合,并以此正式提出了基本塊的概念。CFCSS將程序劃分為基本塊后,通過對每一基本塊分配唯一的標簽并添加錯誤檢測指令來實現控制流錯誤檢測。作為早期以純軟件方法實現的控制流錯誤檢測技術之一,它有著重要的參考比較價值[10]。

目前主流的控制流錯誤檢測方法大多是基于標簽實現的方法,不同方法之間的主要區別在于標簽設置的數量、標簽更新的方式以及標簽比較的位置。Vemu等人[11]提出的CEDA(Control-flow Error Detection using Assertions)就屬于標簽控制流錯誤檢測技術中表現出色的一種。CEDA繼承了部分CFCSS的特性,在每一基本塊的入口和出口處添加了標簽更新與驗證體系,展現出了不錯的性能。Chielle等人在CEDA和一種偏硬件的方法HETA[12]的基礎上提出了S-SETA[13](Selective Software-only Error-detection Technique using Assertions)方法。S-SETA和CEDA較為相似,利用雙層標簽機制,通過基本塊之間的關聯性來計算更新運行時的標簽。Zhu等人[14]提出了一種雙標簽的控制流錯誤檢測方法RCFC (Regularized Control Flow Checking algorithm)。該方法無論是開銷還是檢測性能上均不太理想,但是其提出的雙標簽機制卻提供了一種新的思路。在檢測性能要求較高但開銷可以放松限制的情況下,雙標簽機制就是一種能有效提高錯誤檢測率的手段。國內對基于標簽的控制流錯誤檢測方法也有了較為深入的研究。張鵬等人[15]提出了一種使用雙指令環設計標簽的SSCFC(Structural Signatures for Control Flow Checking)技術,該技術通過引入的雙指令環可以有效地解決塊間滯后性和配置不靈活的缺點。李愛國等人[16]提出了能夠記錄基本塊關系的RSCFC(Relationship Signatures for Control Flow Checking)技術。RSCFC和其他的標簽控制流檢測技術不同,它的基本塊在設計上可以將基跳轉關系直接編碼進來,間接地節省了標簽更新語句和標簽檢查語句的開銷。但是該方法對于基本塊總數有要求,嚴格受到了機器字長的限制,使算法的靈活性受到了極大的影響,難以在大體量程序上使用。張倩雯[17]提出了名為CEDBR(Control-flow Error Detection based on Basic-block Repartition)的雙標簽控制流錯誤檢測技術,該方法有完善的規則和算法設計,有效地提高了錯誤檢錯率,是一種較為成熟的雙標簽算法。帕爾哈提江·斯迪克等人[18]通過分析程序控制流,限制間接調用函數的方法來降低調用指令的數量,再加上一種二進制的檢查代碼,從而達到檢測目的。姬秀娟等人[19]基于程序控制流程圖設計了一種基于投影的模型檢測靜態分析算法,來提高錯誤檢測的有效性和準確率。

目前大部分基于標簽的控制流錯誤檢測方法的原理大體相似,只是標簽設計的結構、規則和位置有所不同,各個方法的檢測率與時空開銷的差異也來源于此,就目前而言,基于標簽的控制流檢測算法普遍存在著開銷與漏檢率矛盾的問題,如何權衡兩者以達到最好的檢測效果,是本文研究的重點。本文對已有的控制流方法進行改進,提出一種多層分段標簽控制流檢測方法CFMSL(Control Flow detection method based on Muti-layer Segmented Labels)。

2 多層分段標簽方法

2.1 相關定義

目前已有的面向軟件的控制流錯誤檢測方法大多需要依靠程序控制流程圖[20],它由基本塊及基本塊之間跳轉關系構成的二元組組成。本文借用LLVM[21](Low Level Virtual Machine)平臺及相關圖片生成工具,實現程序控制流程實體化,并成功嵌入到程序加固系統中。相關定義如下:

定義1基本塊(Basicblock, b)是一組滿足特定條件的最小有序指令集合,記為b={Iin,…,Ii,…,Ibra}?;緣K內部除去最后一條指令外,沒有其它的跳轉指令。

定義2控制流(Control-flow, CF)為軟件運行時基本塊之間的跳轉順序。一般來說,這種跳轉順序是固定不變的,一旦發生改變就有可能產生控制流錯誤。本文定義控制流為E={eij|1i,jn},其中eij為bi到bj之間的跳轉邊,n代表了整個程序中基本塊的總數量。

定義3任意一個程序均可表示為程序控制流程圖(Program control-flow Graph, PG),由二元組PG=〈B,E〉表示。其中B={bin,…,bi,…,bend}代表程序基本塊的集合,E={eij|1i,jn}則代表了程序的控制流。

定義4前驅是指程序控制流中任意一段跳轉關系的起點基本塊,前驅集合是指基本塊所有前驅基本塊的集合,本文使用pred來表示,如果eij∈E,則bi∈pred(bj)。與前驅集合不同,前驅序列是一種基本塊有序集合。某基本塊的前驅序列是指在程序的某一條控制流中,按照執行順序所有處于該基本塊前方的基本塊集合,并依照與該基本塊的距離從近至遠排序。如控制流{b1→b2→b3→b4}中,b4的前驅序列為{b3,b2,b1}。

定義5與前驅對應,后繼是指程序控制流跳轉時的終點基本塊。后繼集合是指基本塊所有后繼基本塊的集合,本文使用succ來表示。如果eij∈E,則bj∈succ(bi)。

定義6軟件運行時因軟錯誤導致軟件發生錯誤跳轉,這種軟件錯誤被稱為控制流錯誤。設指令Ii∈bi={Ii1,Ii2,…,Iiend},在程序中存在指令Ii→Ij之間的合法跳轉,則指令Ij需滿足以下2個條件:1)若i

定義7至多只有一個前驅且至多只有一個后繼的基本塊為O型基本塊,記為TO?;緣K若不是O型,則為M型,記為TM。

定義8本文為每一個基本塊匹配一個具有唯一性的標簽,稱為基本塊標簽,記為BS。當程序正確執行時,動態全局標簽需要與其相等。

定義9程序運行時有一個全局動態標簽,會根據相應的標簽規則進行動態更新,記為GS。當程序正確執行時,更新后的GS要與BS相等。

定義10差值參數主要用于更新全局動態標簽GS,使程序在正確執行時,GS能更新成期望值BS。本文使用d來表示差值參數,如d(bi)代表的是基本塊bi的差值參數。

定義11層級是一組非空基本塊的集合,記為Lv。以M型基本塊為核心,所有該M型基本塊的前驅序列中從頭至尾連續的O型基本塊和該M型基本塊處于同一層級,直至遇到另一個M型基本塊為止?;緣K可以同時屬于多個層級。

定義12基本塊多前驅矛盾是指當一個基本塊同時具備多個前驅時,不同前驅跳轉至同一基本塊需要讓不同標簽值通過同一更新語句獲得同一標簽值。但標簽具有唯一性,標簽更新語句也大多結果唯一,這種唯一性與上述要求產生了矛盾。

圖1以數據管理系統的部分邏輯代碼為例,給出上述程序控制流相關定義的進一步說明。圖1(a)為由if語句實現跳轉的示例代碼。圖1(b)為源代碼級基本塊劃分圖。圖1(c)為程序控制流程圖PG,整個程序由%0、%9、%10和%11這4個基本塊構成,分別記為b1、b2、b3、b4,其中b1、b4為M型基本塊,b2、b3為O型基本塊。依照程序正常執行流程,基本塊b1的后繼為b2和b3。由于程序內變量b為0~3之間的隨機數,與a之間的比較結果隨機,故跳轉至b2或b3均為正??刂屏?。若程序執行過程中受軟錯誤影響發生錯誤跳轉,如圖1(b)中由b1跳至b4,此時變量c的值仍為0,發生控制流錯誤。

(d) 程序控制流相關定義

2.2 基本塊按層次劃分規則

依照定義7將基本塊分為2類,M型基本塊與O型基本塊。本文設計的分層標簽需要程序滿足一種特定的控制流跳轉規律:2個M型基本塊不可連續執行,后文將這條規律稱為M不連續原則。以此為基礎設計標簽生成、更新及校驗規則。不滿足跳轉規律的程序,需要使用基本塊按層次劃分規則來改變程序控制流結構。

規則1若程序中存在一條控制流,其中有2個M型基本塊連在一起,則替換其原本跳轉路徑,在二者之間插入1個空基本塊。

規則2以M型基本塊為核心,所有該M型基本塊的前驅序列中從頭至尾連續的O型基本塊和該M型基本劃分為同一層,直至遇到另一個M型基本塊為止。對于任意一個程序,若入口基本塊為M型基本塊,則將其單獨劃分為一個層級。若入口基本塊為O型基本塊,則將之歸入程序流中的第一個M型基本塊所處的層級。

引理1通過規則1對程序控制流重構后,得到的新程序控制流程圖中,不存在可以連續執行2個M型基本塊的控制流。即:?bi∈B,若bi∈TM,則(succ(bi)?TO)∨(pred(bi)?TO)。

證明:對?bi∈TM,若?bj∈succ(bi)?TM,則根據規則1調整,必?bp∈TO,使得bp∈pred(bj),bp∈succ(bi)且bi?pred(bj),bj?succ(bi),這與bj∈succ(bi)產生矛盾。因此,任何經過規則1調整后的程序,一定不存在可以連續執行2個M型基本塊的控制流。

圖2為基本塊層次劃分規則應用的典型情況。其中,圖2(a)和圖2(b)分別對應規則1與規則2。虛線所代表的基本塊表示新插入的空基本塊。圖2(a)中b1和b2均為M型基本塊,整個程序有2條控制流{b1→b2}與{b1→b3→b2},前者不滿足M不連續原則,故根據規則1插入空基本塊bp以重構控制流。圖2(b)中有一條控制流從b4又跳回了b1,導致b1同時歸屬2個層級Lv1和Lv3。

圖2 基本塊按層次劃分示例

2.3 多層分段標簽規則

本文采用靜態標簽[22]插樁技術,插樁全局動態標簽GS(Global Signature),使程序執行時連續地更新GS,并隨時檢查標簽以監視程序的運行狀態。這一過程可以被概括地分成3個階段:標簽分配階段、標簽更新階段以及標簽檢查階段。標簽分配階段會為程序中的每一基本塊靜態地計算并分配基本塊標簽值;標簽更新階段根據標簽分配規則為每一基本塊添加標簽更新語句,使程序正確運行時得到正確的標簽。標簽檢查階段在基本塊內部添加檢查指令,以保證發生標簽錯誤時可以盡早檢測出來。

本文設計了用于標簽分配的具體規則,給出了相關定理,為了方便描述,引入下列術語:

1位&1位集合:1位是指本文所設計的二進制標簽中數值為1的位置(位數從1開始,并且從右向左計算),1位集合是指標簽中所有1位的集合,本文中將1位集合表示為1set。如:011的1位集合為{1,2},110的1位集合為{2,3},即1set(011)={1,2},1set(110)={2,3}。

1位包含:1位包含是指某一標簽的1位集合包含于另一標簽的1位集合。如:010的1位集合包含于011的1位集合,即{2}?{1,2}。

多層分段標簽:本文所設計的多層分段標簽通過分段設計使其具備了雙標簽的功效。標簽共分為前后2段,分別為層號段與標簽值段。層號段標識基本塊所屬層次,記為BS1。標簽值段則在同層內標識不同的基本塊,記為BS2。

作為標簽檢錯技術的一種,多層分段標簽控制流錯誤檢測方法也不可避免地遇到了一個問題:基本塊多前驅矛盾。CFCSS為了解決這一問題增加開銷引入了變量D,RCFC為了解決這一問題放棄了標簽唯一性從而造成了檢錯率的下降。多層分段標簽控制流錯誤檢測方法利用特殊的標簽機制及更新規則,在解決這一矛盾的同時未增加任何開銷,同時也保證了標簽的唯一性,具體規則如下。

規則3程序執行時,全局動態標簽GS的更新語句在基本塊入口位置,O型基本塊執行異或運算,M型基本塊執行或運算。即:

規則4程序內所有O型基本塊標簽的1位集合包含于其后繼M型基本塊標簽的1位集合。即:?bi,bj∈B,若bi=pred(bj),bi∈TO且bj∈TM,則1set(BS(bi))?1set(BS(bj))。

若基本塊為O型基本塊,分段差值參數為基本塊分配標簽與其前驅基本塊分配標簽異或運算的結果。即:?bi,bj∈B,若bi∈TO,bj∈pred(bi)且bi∈succ(bj),則d(bi)=BS(bi)xor BS(bj)。

規則5若基本塊為M型基本塊,其分段差值參數層號段為0,標簽值段為該基本塊所有前驅標簽值段或運算的結果。即:?bi,bj1,…,bjn∈B,若?bi∈TM,bj1,…,bjn∈pred(bi),則d(bi)=BS(bj1) or BS(bj2) or…or BS(bjn)。

規則6所有M型基本塊標簽中標簽值段為該基本塊所有前驅基本塊標簽中標簽值段或運算的結果。即:?bi,bj1,…,bjn∈B,若?bi∈TM,bj1,…,bjn∈pred(bi),則BS2(bi)=BS2(bj1) or BS2(bj2) or…or BS2(bjn)。

規則7將程序所有基本塊按層次劃分,并在標簽層號段標識層號。層號具備唯一性,且互相滿足1位不包含原則。一般來說,層號僅取標簽層號段的某一位為1。即:?bi,bj∈B,若Lv(bi)≠Lv(bj),則(1set(BS1(bi))?1set(BS1(bj)))∪(1set(BS1(bj))?1set(BS1(bi)))。

規則8若程序中存在循環控制流,即某一基本塊同時處于多個層級中,則該基本塊必為M型基本塊,且其層號為其所有前驅基本塊層號or運算的結果。即:?bi∈B,bj1,…,bjn∈pred(bi),則BS2(bi)=BS1(bj1) or BS1(bj2) or…or BS1(bjn)。

規則9不同層級間基本塊標簽值段可重復,但同一層基本塊間標簽值段必須唯一,且該層所有O型基本塊之間互相滿足1位不包含原則,M型基本塊之間也互相滿足1位不包含原則,非前驅后繼關系的O型基本塊與M型基本塊也互相滿足1位不包含原則。

規則10程序內每一個基本塊均要有標簽檢查指令,位置在標簽更新指令之后,用于比較全局動態標簽GS與基本塊標簽BS的值以檢測控制流錯誤。

上述規則為多層分段標簽控制流錯誤檢測方法的基本規則,也是必要規則。規則3~規則6是多層分段標簽控制流錯誤檢測方法可以獲得較低開銷的基礎,本文將基本塊劃分為2種類型:O型與M型。由于O型基本塊至多只有一個前驅,故基本塊多前驅矛盾都集中發生在M型基本塊中。多層分段標簽控制流錯誤檢測方法在M型基本塊的標簽更新語句中使用or運算來替換xor運算。但or運算本身不具備唯一性,有可能導致某些控制流錯誤無法檢測。如圖3(a)所示,依照規則3~規則6分配標簽,通過or運算解決了b2→b4和b3→b4的基本塊多前驅矛盾問題,但發生b1→b4的控制流錯誤跳轉時,就無法檢測出來。為了解決該問題,本文引入了層號的概念,并在標簽的設計上做出了調整。如圖3(b)所示,層號可以檢測出程序中發生的b1→b4控制流錯誤。層號在設計時也要遵循一定規則,否則如圖3(c)所示,層號未解決問題。因此,本文提出了規則7。對于整個程序而言,層號之間必須有所區分且唯一。在此基礎上,也不允許存在1位集合包含的情況,即任意的2個不同層號之間,1位集合互不包含。層號不允許設置為0,一般層號僅取標簽中的某一位為1即可。如程序共分為3層,則層號可分別設為:001,010,100。程序的循環結構是一種較為常見的結構,體現到程序控制流程圖中就代表會出現如圖3(d)中b1的結構。這種情況下使得基本塊b4同時處于010層和100層中,故層號也包含了010和100。為了解決這一現象,本文引入了規則8,依照此規則此時基本塊b4的所屬層號為010 or 100=110,同時兼顧了b2→b4、b3→b4和b5→b4的控制流跳轉。

(a) (b)

(c) (d)

規則3~規則8解決了控制流跨層錯誤跳轉的問題,但未顧及同層錯誤跳轉問題,尤其是當同一層含有2個或2個以上的M型基本塊的情況。如圖4(a)所示,b2、b4和b5均為M型基本塊,在程序中存在2條控制流b2→b4和b2→b5,依照規則1在上述2條控制流中插入了空基本塊bp1和bp2,按照規則2劃分層次。如圖4(b)所示,在僅考慮規則3~規則8的情況下,本文設計了一款樣例標簽??梢钥闯鰣D4(b)中,標簽無法檢測出b1→b5或b4→b5的控制流錯誤跳轉。故此設計了規則9。同一層的O型基本塊間標簽值段必須唯一,且滿足互相1位不包含原則,M型基本塊同理。圖4(b)程序中的O型基本塊b1的1位集合被同層O型基本塊b2和b3所包含,M型基本塊b4的1位集合被同層M型基本塊b5所包含,故產生了上述2條無法被檢測的控制流錯誤。依據規則10可插入檢查指令,考慮所有規則重新設計了如圖4(c)所示的標簽方案,解決了上述問題。

(a)

(b)

(c)

接下來,本文引入一些定理來證明本文提出CFMSL的安全性及完備性。安全性是指當程序正確執行時,多層分段標簽方法所分配的標簽不會檢測出錯誤。完備性則是指若程序在執行過程中發生了基本塊間錯誤跳轉,多層分段標簽方法可以將其檢測出來。

引理2通過規則1重構后,得到的程序控制流任意M型基本塊均與其前驅基本塊處于同一層次。

證明:若存在一基本塊為M型基本塊前驅,且和該基本塊不屬于同一層次。根據規則2,所有M型基本塊的前驅序列中的O型基本塊和該M型基本劃分為同一層,可知該前驅基本塊只能為M型基本塊。根據引理1,M型基本塊的前驅不可為M型基本塊,產生矛盾。因此,不存在這樣的基本塊前驅,即任意M型基本塊均與其前驅基本塊處于同一層次。

定理1當程序正確執行時,若標簽在進入基本塊前滿足GS=BS,則無論程序執行至基本塊內任何位置,仍滿足GS=BS。

證明:設?bi,bj∈B,且程序中存在控制流eji,即bi∈succ(bj)且bj∈pred(bi)。當全局動態標簽GS到達基本塊bi時GS=BS(bj),所執行的標簽更新語句取決于此時基本塊的類型。根據定義,程序中任意基本塊均屬于O型或者M型,故分2種情況討論:

1)bi∈TO。根據規則3,此時基本塊的更新語句為GS=GS xord(bi)=BS(bj) xor BS(bi) xor BS(bj)=BS(bi)。

2)bi∈TM。根據規則3,此時基本塊的更新語句為GS=GS ord(bi)。根據規則6和規則8,GS更新語句為GS=GS or d(bi)=BS(bj) or BS(bj1) or … or BS(bjn)=BS(bi)。

綜上所述,此時的全局動態標簽在基本塊任何位置均滿足GS=BS。

引理3若因程序發生錯誤跳轉而導致全局動態標簽層號段在程序中任何一處與基本塊標簽層號段不同,則此錯誤會被檢查出來。

證明:若層號與期望值不同,證明此時發生了跨層錯誤跳轉。錯誤產生后,GS會在基本塊入口處進行標簽更新。GS抵達不同類型的基本塊,會遇到不同的標簽更新運算。若抵達O型基本塊,則更新語句為GS=GS xord。異或運算的結果具備唯一性,已有的層號段錯誤不會被掩蓋,故此錯誤可以被檢查出來。若抵達M型基本塊,則更新語句為GS=GS ord。根據規則7,此時層號段與期望值不同,但也滿足1位互不包含原則。根據規則8,更新語句中的差值參數d層號段1位與基本塊所處層次1位相同,即d1和GS的1位不同。顯然,1位是無法被或運算掩蓋的,故此錯誤也能被檢查出來。

引理4若因程序發生錯誤跳轉而導致全局動態標簽值段在程序中任何一處與基本塊標簽值段不同,則此錯誤會被檢查出來。

證明:根據引理3,層號段出現錯誤會被檢查出來,所以現在考慮層號段未出錯,標簽值段出錯的情形。層號段未出錯,證明程序發生的是同層錯誤跳轉。根據GS抵達基本塊的類型進行分類討論。若抵達O型基本塊,則更新語句為GS=GS xord。異或運算結果具備唯一性,根據規則9同層基本塊標簽值段也具備唯一性,故此時的標簽值段錯誤不會被掩蓋。若抵達M型基本塊,則更新語句為GS=GS ord。因發生同層錯誤跳轉且跳到M型基本塊,故此時也有2種情況:1)O型基本塊錯誤跳轉到M型基本塊,由于是同層錯誤跳轉,此O型基本塊和M型基本塊不是前驅后繼關系;2)M型基本塊錯誤跳轉到M型基本塊,此時也是同層錯誤跳轉。根據規則9,無論是上述哪種情況,起點基本塊和錯誤跳轉基本塊的標簽值段均滿足1位不包含原則,故二者標簽值段有不同的1位,或運算無法掩蓋,故此錯誤可以被檢查出來。

引理5所有抵達O型基本塊的錯誤跳轉,均會被該基本塊內的檢查語句檢測出來。

證明:設?bi,bj∈B,程序發生錯誤跳轉bj→bi,且程序運行至bj前均正確執行。因發生的是錯誤跳轉,則bj?pred(bi),根據規則6~規則9,BS(bj)≠BS(pred(bi))。程序運行在至bj前均為正確執行,故此時全局動態標簽與其期望值相等,即GS=BS(bj)。跳轉后,全局動態標簽GS立刻進行更新操作,則GS=GS xord(bi)=BS(bj) xor BS(bi) xor BS(pred(bi))≠BS(pred(bi)) xor BS(bi) xor BS(pred(bi))?GS≠BS(bi)。根據引理3與引理4,GS任意一位與BS(bi)不相等,均會被檢測出來。

引理6所有抵達M型基本塊的錯誤跳轉,均會被該基本塊內的檢查語句檢測出來。

證明:?bi,bj∈B,程序發生錯誤跳轉bj→bi且至bj前均為正確執行。bj?pred(bi),BS(bj)≠BS(pred(bi)),GS=BS(bj),分情況討論。

若bj與bi屬于不同層次,則GS1=BS1(bj)≠BS1(bi)。據M型基本塊標簽更新語句,此時GS1=GS1xord1(bi)=BS1(bj) or BS1(bj1) or … or BS1(bjn),其中bj1,…,bjn∈pred(bi)。根據規則2,BS1(bj1)=BS1(bj1)=…=BS1(bjn)=BS1(bi),故GS1=BS1(bj) or BS1(bi)。根據規則7,BS1(bj)與BS1(bj)互相1位不包含,故GS1=BS1(bj) or BS1(bi)≠BS1(bi)。據引理3,層號段的錯誤會被檢測出來。

若bj與bi屬于相同層次,則錯誤跳轉不會引發層號錯誤。根據規則9,GS在錯誤抵達bi前GS2=BS2(bj)≠BS2(bi)。據M型基本塊標簽更新語句,GS2=GS2or d2(bi)=BS2(bj) or BS2(bj1) or…or BS2(bjn)=BS2(bj) or BS2(bi),其中bj1,…,bjn∈pred(bi)。據規則9,無論bj是O型還是M型基本塊,BS1(bj)與BS1(bj)互相1位不包含。故GS2=BS2(bj) or BS2(bi)≠BS2(bi),根據引理4,標簽值段的錯誤會被檢測出來。

定理2多層分段標簽控制流錯誤檢測技術是完備的。在程序中任何違反正確控制流的基本塊間錯誤跳轉均可被檢測出來。

證明:程序中的控制流錯誤會導致2種情況,程序非法跳轉至程序基本塊內部或跳出程序至非代碼部分。跳轉至非代碼部分代表程序進入了數據部分或者未經初始化的存儲區域,根據參考文獻[11],若跳轉至這一部分,處理器在嘗試執行數據或未初始化的存儲區域時會引發指令異常而導致系統報錯。如果跳轉至程序內部,則將跳轉至O型基本塊或者M型基本快。根據引理5與引理6,無論跳轉至哪種類型的基本塊,均會在檢查指令中檢測出錯誤。

根據上述定理可知,CFMSL方法是完備的,為了進一步說明定理2,本文給出了控制流非法跳轉示例,如圖5所示。

圖5 控制流非法跳轉示例圖

如圖5所示,灰色為M型基本塊,白色為O型基本塊,圖中共給出了8種控制流錯誤的示例。err1與err2為M型基本塊跳轉至M型基本塊,由于b1、b4和b6三者層級不同,err1/err2跳轉時層號段出錯,根據引理3和引理6,2個錯誤均會被檢查出來。err3/err4為O型基本塊跳轉至O型基本塊,b2、b3和b5處于不同層次,根據引理3和引理5,2個錯誤均會被檢查出來。err5/err6為M型基本塊跳轉至O型基本塊,b1與b5不同層,故err5可根據引理3和引理5檢查出來。b5與b6處于同一層次,但由于逆向跳轉,導致標簽值段發生了錯誤,故根據引理4和引理5可將err6檢查出來。err7/err8為O型基本塊跳轉至M型基本塊,此時b1與b3處于不同層級,b2與b6處于不同層級,故根據引理3與引理6可知,2個錯誤均會被檢查出來。

2.4 多層分段標簽控制流錯誤檢測算法描述

本文設計了多層分段標簽控制流錯誤檢測算法,針對以C語言編程的數據庫管理系統,通過相應規則進行基本塊層次劃分,并分配基本塊標簽層號段及標簽值段。插樁標簽更新指令和標簽檢查指令,最終生成具有檢錯能力的目標程序。具體的步驟如下:

Step1將目標程序編譯成中間代碼,以進行控制流分析。

Step2分析程序控制流關系,根據規則1重構程序基本塊,使整個程序滿足M不連續原則。

Step3根據規則2按層劃分基本塊,根據規則7、規則8分配基本塊標簽層號。

Step4依照基本塊層次遍歷基本塊,同層基本塊依照規則6、規則8和9分配基本塊標簽值段。

Step5遍歷所有基本塊,依照規則3、規則4和規則5插樁基本塊更新指令。

Step6根據規則10插樁標簽檢查指令。

3 實驗及結果分析

3.1 故障注入工具

在程序執行時,指令進行跳轉的目標地址受軟錯誤影響而改變,這會導致2種結果:

1)改變后的目標地址仍在程序代碼區內。此時程序計數器的值雖然發生了變化,但是并沒有跳出程序,只是在程序內部的基本塊間互相跳轉。

2)程序計數器發生改變后,指向了程序代碼區以外的地址。

根據上述控制流錯誤結果,使用2種錯誤類型來模擬軟件控制流錯誤:控制流錯誤跳轉和控制流錯誤跳出??刂屏麇e誤跳轉是指程序控制流執行時發生控制流錯誤,控制流發生錯誤跳轉,但仍然在程序內部??刂屏麇e誤跳出是指程序控制流執行時發生控制流錯誤,使控制流錯誤跳出至程序外。

本文使用的故障注入工具是基于GDB(GNU Project Debugger)[23]二次開發實現的。工具分為2種類型:控制流錯誤跳轉故障注入工具和控制流錯誤跳出故障注入工具,分別對應上述2種控制流錯誤類型。

1)控制流跳轉故障注入工具。

Step1啟動GDB并加載要注入控制流跳轉錯誤的程序。

Step2完整運行一次程序,記錄所有程序指令跳轉的PC值。

Step3隨機選擇一條PC值,記錄下來,作為控制流錯誤跳轉的起點。。

Step4使用GDB重新加載程序。

Step5運行程序,至Step3所選起點指令PC值處設置斷點。

Step6在剩余PC值中隨機選擇1條,控制程序跳轉過去。

Step7根據程序的輸出來統計故障注入的結果。

2)控制流跳出故障注入工具。

Step1啟動GDB并加載要注入控制流跳出錯誤的程序。

Step2完整運行一次程序,記錄所有程序指令跳轉的PC(Program Counter)值。

Step3隨機選擇一條PC值,記錄下來,作為控制流錯誤跳出的起點。

Step4使用GDB重新加載程序。

Step5運行程序,至Step3所選起點指令PC值處設置斷點。

Step6在程序計數器內的地址隨機選擇一位或者多位進行翻轉,同時保證翻轉后的地址不在Step2記錄的程序內部PC值中,將程序跳轉至翻轉后的地址。

Step7根據程序的輸出來統計故障注入的結果。

3.2 方法評估

本文使用錯誤檢錯率來評估CFMSL方法的錯誤檢測能力。CFMSL方法可以通過標簽檢測控制流錯誤。本文對測試程序注入控制流跳轉錯誤與控制流跳出錯誤,以此來模擬程序發生控制流錯誤時的狀態。為了驗證CFMSL方法的性能,本文另外選擇3種控制流錯誤檢測加固方法CFCSS、CEDBR和RCFC來進行橫向對比。CFCSS為2002年的方法,盡管年代較為久遠,但是作為最具代表性的單標簽控制流方法,仍然具有較高的參考價值。RCFC是2016年提出的一種雙標簽方法,盡管標簽設計有一定的缺陷,卻也提供了一種新思路。CEDBR是2018年提出的雙標簽方法,相比于RCFC,CEDBR已經有了較好的標簽設計和詳細的規則,屬于雙標簽方法中較為優秀的方法。分別使用這3種方法和CFMSL對快速排序算法、最短路徑算法和數據管理系統3個程序進行加固,得到了12個加固后的程序。為了體現魯棒性和有效性,本文對每個加固后程序分別注入了2500次控制流跳出錯誤和2500次控制流跳轉錯誤,共60000次故障來驗證CFMSL方法的性能。實驗結果如圖6所示。

圖6給出采用不同的加固方法下,錯誤檢測性能的對比。漏檢率與檢錯率的統計是綜合了控制流錯誤跳轉與控制流跳出2種故障注入實驗數據的綜合結果。其中CEDBR和RCFC是基于雙標簽的控制流加固方法,CFMSL和CFCSS則是單標簽多規則的加固方法。

圖6 不同加固方法錯誤檢測性能

本文對使用方法加固后的每一個程序,注入了2500次控制流跳出錯誤和2500次控制流跳轉錯誤。即本文對每一個加固后的程序進行了5000次故障注入實驗。系統報錯率為這5000次實驗中系統報錯次數所占的比率。方法報錯率為實驗次數中由檢錯方法報錯次數所占的比率。無錯誤率為向程序注入故障,但未出現錯誤次數所占的比率。漏檢率為程序出現異常,但是方法和系統均未檢測出錯誤次數所占的比率。1減去漏檢率,即為錯誤檢測率。

表1 故障注入實驗數據

表1給出了具體實驗數據,SYS表示系統錯誤的次數,Find_err表示方法發現錯誤的次數,Correct表示程序盡管注入了錯誤,但仍正確執行的次數。從實驗結果可以看出,控制流錯誤跳出故障類型大部分可以通過系統直接檢測出來,小部分對程序沒有影響,只有極少的一部分錯誤會漏檢。與之相反的是,控制流錯誤跳轉故障中方法檢測出的錯誤占據了大部分。與圖6相同,表1中最后2欄的錯誤檢測率與錯誤漏檢率是綜合了控制流錯誤跳轉與跳出2種故障的實驗結果。根據圖6和表1,所有的加固方法中CFMSL具有最高的錯誤檢測率和最低的錯誤漏檢率。

各方法的時空開銷如圖7所示,具體實驗數據如表2所示。從中可以看出CEDBR方法的開銷是最高的,RCFC方法比它稍低一些,CFCSS和CFMSL方法比上2種方法開銷要低。

圖7 各方法的時空開銷

表2 方法開銷數據

綜合圖6和圖7的實驗結果,可以發現基于雙標簽的方法成本一般要比單標簽多規則的方法高,而且只要規則設置得合適,單標簽的方法錯誤漏檢率也可降低。而在上述4種方法中,單標簽的CFMSL開銷最低,漏檢率也是最低的。

RCFC是一種雙標簽算法,在O型基本塊插樁標簽G1,在M型基本塊插樁G2。其G2標簽僅使用1和0這2個數來區分標簽類型,不具備唯一性。且標簽更新函數為“store”賦值語句而非運算,容易將標簽錯誤掩蓋,故存在著較高的漏檢率。CEDBR是基于RCFC的改進算法,在標簽更新上進行了改進。CEDBR在基本塊內部使用加減運算進行G1標簽更新,盡管開銷增加,但顯著提高了檢錯率。另一方面,CEDBR的G2標簽仍使用1和0,只能區分基本塊類型,不具備唯一性,這導致CEDBR仍然存在漏檢情況。CFCSS則是一種傳統的單標簽方法,但是為了解決基本塊多前驅矛盾,引入了變量D來對標簽進行更新,導致開銷增大。CFMSL作為一種單標簽方法,卻通過分段的形式起到了雙標簽的作用。將基本塊劃分層級后,跨層的錯誤跳轉可以通過層號段檢測出來,同層的錯誤跳轉可以通過標簽值段進行檢測。CFMSL使用XOR和OR運算的組合,在不添加任何指令和標簽的情況下成功解決了基本塊多前驅矛盾問題,最后又使用標簽更新規則保證了標簽更新過程的唯一性。這使得CFMSL在具備較高檢錯率的同時具有較低的開銷。

4 結束語

本文提出了一種多層分段標簽控制流錯誤檢測方法CFMSL。通過分析程序中的控制流信息和基本塊結構,按層次重新劃分基本塊。對重構后的基本塊,分配多層分段標簽,插樁標簽更新指令和標簽檢查指令,最終可得到控制流檢錯加固后的程序。本文設計了基本塊按層劃分規則、基本塊標簽更新規則、基本塊標簽檢查規則。通過定理證明和邏輯分析證實了本文方法的正確性和完備性。最終通過控制流故障注入工具對程序進行故障注入實驗,通過實驗結果驗證了方法的有效性。

猜你喜歡
控制流前驅O型
抵御控制流分析的Python 程序混淆算法
基于返回地址簽名的控制流攻擊檢測方法
化學氣相沉積法從MTS-H2-N2前驅體制備碳化硅涂層
Mg2SiO4前驅體對電熔MgO質耐火材料燒結性能及熱震穩定性的影響
蚊子愛叮O型血的人?
基于控制流的盒圖動態建模與測試
XLNO型低溫脫除氧化亞氮催化劑性能研究
SRSF2、HMGA2和Caspase-3在卵巢高級別漿液性癌及其前驅病變中的表達及意義
基于Petri網數據流約束下的業務流程變化域分析
回收制備二氯二氨合鈀(Ⅱ)前驅體材料的工藝研究
91香蕉高清国产线观看免费-97夜夜澡人人爽人人喊a-99久久久无码国产精品9-国产亚洲日韩欧美综合