一種利用圖同構驗證編譯器的方法

一種利用圖同構驗證編譯器的方法

《一種利用圖同構驗證編譯器的方法》是北京廣利核系統工程有限公司中國廣核集團有限公司於2013年10月25日申請的專利,該專利的申請號為2013105124379,公布號為CN103559125A,授權公布日為2014年2月5日,發明人是馮素梅、江國進、白濤、孫永濱、劉建龍、李幼媛、袁勁濤、楊曉豫、寧祾、趙雲飛。

《一種利用圖同構驗證編譯器的方法》公開一種利用圖同構驗證編譯器的方法,包括待處理的源程式和將源程式生成目標程式的編譯器,在選定環境下建立一個反編譯器,通過反編譯器將目標程式反編譯成對比程式,驗證對比程式和源程式之間的語義一致性,並在此基礎上,分別建立源程式和對比程式的控制流圖相關結點信息後進行同構判定,從而得到編譯器是否安全的結論。該發明通過判斷對比程式與源程式的控制流圖是否同構,來驗證編譯器的安全性。

2018年12月20日,《一種利用圖同構驗證編譯器的方法》獲得第二十屆中國專利優秀獎。

(概述圖為《一種利用圖同構驗證編譯器的方法》摘要附圖)

基本介紹

  • 中文名:一種利用圖同構驗證編譯器的方法
  • 公告號:CN103559125A
  • 授權日:2014年2月5日
  • 申請號:2013105124379
  • 申請日:2013年10月25日
  • 申請人:北京廣利核系統工程有限公司、中國廣核集團有限公司
  • 地址:京市海淀區永豐路5號院5號樓100094
  • 發明人:馮素梅、江國進、白濤、孫永濱、劉建龍、李幼媛、袁勁濤、楊曉豫、寧祾、趙雲飛
  • Int.Cl.:G06F11/36(2006.01)I; G06F9/45(2006.01)I
  • 代理機構:北京元中智慧財產權代理有限責任公司
  • 代理人:王明霞
  • 類別:發明專利
專利背景,發明內容,專利目的,技術方案,改善效果,附圖說明,技術領域,權利要求,實施方式,榮譽表彰,

專利背景

編譯器作為軟體的生成工具,在那些對軟體安全性要求十分高的特殊環境裡面,其安全性至關重要,特別是用於核安全級保護系統的軟體。在核安全級系統中,一方面為了保證軟體運行的安全性,程式設計師經常會引入查錯程式或者防禦性的程式,而經過編譯後的目標代碼為了保持原始碼的安全性,要求編譯器不能在無警告或提示下刪除程式設計師引入的防禦程式或查錯程式,從而導致目標程式不符合安全級軟體的要求;另一方面,由於編譯器的漏洞以及人為的後門程式可能會對整個軟體造成根本性的破壞,所以,要求編譯器在編譯的過程中不會人為的插入惡意代碼。由此,在驗證編譯正確性的基礎上必須從以上兩個方面驗證編譯器的安全性。
截至2013年10月25日,對於編譯器的驗證技術主要有形式化驗證技術以及測試驗證技術,其中,形式化驗證技術是從編譯器本身的正確性或者是從保證被編譯對象的正確性入手進行證明,但是這個方法實現難度較大,成功案例也僅限套用於某個語言子集的證明,很難推廣到工程套用上來。而測試驗證技術由於無法對其輸入進行全覆蓋,以及編譯器的複雜性所帶來的巨大工作量,使得僅靠測試驗證技術難以完成對編譯器的完整的驗證。
此外,這些驗證技術僅基於編譯器邏輯正確性的驗證,即對原始碼和目標代碼行為是否一致的驗證,且都沒有很好的解決編譯器對惡意代碼注入的問題,以及編譯器對那些不影響動態語義的防禦程式的刪除的問題。故除了依賴對編譯器的邏輯正確性驗證之外,還需要多遍交叉編譯、目標檔案結構化比較、目標檔案反編譯邏輯比較等理論和方法完成對安全性的驗證。
在截至2013年10月25日技術中驗證代表包括:
(1)ISTec利用反編譯技術由獨立的小組開發從目標程式翻譯到源程式的反編譯器,比較原始碼與目標代碼反編譯後的代碼的一致性,來實現對編譯器的正確性驗證的方式。
(2)XavierLeroy帶領的CompCert項目組利用定理證明的形式化方法首次完成了從Clight到PowerPC轉換過程的正確性形式化驗證。但是,這種針對編譯器本身的形式化驗證方法一般較難實現,且證明整個編譯器的正確性也比較困難,即使是CompCert小組也只是針對編譯器的後端進行了證明。
(3)俞甲子基於GCC編譯器提出了一種除了能夠驗證編譯器邏輯正確性之外,還可對編譯器的安全性進行驗證的方法。該方法結合了編譯器代碼分析及對比驗證方案和原始碼與目標代碼控制流圖同構比較方案。其中編譯器代碼分析及對比驗證方案首先對編譯器的設計及原始碼進行分析,針對每個函式進行分類,對能夠改變輸入數據的函式進行重新編寫,對比原始版本的數據結構和重新設計的數據結構;控制流圖同構比較方案是採用對原始碼和目標代碼抽取控制流圖,並判斷控制流圖是否同構來排除編譯時是否人為的插入惡意代碼。

發明內容

專利目的

《一種利用圖同構驗證編譯器的方法》提供一種利用源程式和對比程式的控制流圖是否同構的方法來檢測編譯器的安全性。

技術方案

《一種利用圖同構驗證編譯器的方法》包括待處理的源程式和將源程式生成目標程式的編譯器,在選定環境下建立一個反編譯器,通過反編譯器將目標程式反編譯成對比程式,驗證對比程式和源程式之間的語義一致性,其特徵在於,在此基礎上分別建立源程式和對比程式的控制流圖相關結點信息後進行同構判定,從而得到編譯器是否安全的結論,具體步驟如下:
步驟1、首先對源程式和對比程式的語句按順序進行掃描,並利用帶序號的結點進行標識,同時標明各結點的出邊信息;
步驟2、同時建立一個輔助棧表,並將當前結點及相關結點信息壓入輔助棧表;
步驟3、對條件結構的所有結點進行簡化並用簡化結點替代,然後將簡化結點壓入輔助棧表原條件結構的結點位置處形成簡化棧表,並且在程式中所有結點被掃描完成之後,將棧表中的結點依次出棧,在上述簡化過程中,建立該結點的鄰接鍊表,同時建立一個記錄簡化結點信息的簡化信息表;
步驟4、根據結點的鄰接鍊表和簡化信息表建立源程式和對比程式的出入度信息,並生成相應的n點連通子圖的出入度序列;
步驟5、根據出入度序列判斷源程式和對比程式的控制流圖是否同構;其中,當兩個控制流圖中的任意n點連通子圖的出入度序列相同時,則表明兩個控制流圖是同構的,進而表明源程式與目標程式是相同的,並得到編譯器是安全的結果;反之,則證明編譯器是不安全的。
為根據不同的結構設定相應的結點:所述步驟1中,結點的添加標準如下:
步驟11、首先在源程式和對比程式的開始和結尾分別增加一個開始結點和終止結點;
步驟12、順序執行的語句(程式)用一個結點標識;
步驟13、條件語句的起始句用一個條件起始結點標識,中間的各條件表達式分別用一個中間結點標識,同時增加一個條件語句的條件結束結點;
步驟14、循環語句的起始句用一個執行結點標記,結尾語句用一個判斷結點標記;
步驟15、在分析時遇到RETURN語句則單獨添加一個返回結點。
為建立出入度信息:各結點的出邊連線方法如下:
步驟31、按各結點排列順序依次連線;
步驟32、遇到條件語句的結點時,條件起始結點與各中間條件表達式的中間結點按順序連線,如遇到返回結點時,則返回結點的出邊直接與終止結點連線,否則按順序連線條件結束結點;
步驟33、遇到循環語句的結點時,執行語句結點指向判斷結點,判斷結點分別指向執行語句結點和順序排列的下一個結點。
為方便後續檢索:所述輔助棧表的基本信息包括如下內容:
A、按分析順序生成的各結點的類型,包括順序類型、條件類型和循環類型,各類型以相應結構的起始句為標識進行區分;
B、各結點對應的排列序號;
C、每個結點所包含的結點數量;
D、所包含的return語句數量。
為方便查找各結點:所述步驟3中,鄰接鍊表記錄每個結點的出邊信息,並記錄所有鄰接鍊表的表頭指針信息以作為檢索信息。
為方便查找簡化結點的信息:所述步驟3中,簡化信息表的內容包括結點名、被簡化結構包含的結點個數、起始結點和終止結點名,以及所涉及的return分支數量。
為方便源程式和對比程式的對比:所述步驟4中,出入度序列的建立方法如下:
步驟41、根據鄰接鍊表中的結點信息統計出各結點的出度和入度信息;
步驟42、然後依次讀取簡化棧表中各結點的信息,遇到簡化結點時,並用簡化結點及其出度、入度信息去更換被簡化結構相應位置結點的出度、入度信息,同時更新該被簡化塊的出入度信息,並且連同該簡化塊的結點總數一起記錄下來;
步驟43、分別統計更新後源程式和對比程式的n點連線子圖的出入度序列,並對其中的出度和入度按大小進行排序。

改善效果

《一種利用圖同構驗證編譯器的方法》在利用反編譯技術的基礎上,將目標代碼反編譯之後的對比程式與源程式利用常規手段進行語義一致性比較,驗證編譯器的正確性;然後判斷反編譯之後的對比程式與源程式的控制流圖是否同構,來驗證編譯器的安全性。該方法直接將反編譯後的代碼與原始碼進行語義比較,避免了驗證過程中由於原始碼信息丟失導致驗證不全面的問題,並且在進行安全性驗證時,提出了在同一語言下進行程式控制流圖同構判定算法,該算法只需要實現一種語言下程式的信息提取,並藉此信息進行控制流圖同構的判定,不需要再次遍歷控制流圖,使得控制流圖同構判斷算法簡單,易於實現。另外,由於惡意代碼和防禦程式以及查錯程式一般包含一定的條件判斷語句,能夠改變程式的控制流圖,因此,通過驗證程式的控制流圖是否同構來判斷編譯器在編譯的過程中是否改變了程式的結構,從而達到驗證編譯器的安全性的目的。

附圖說明

圖1源程式和對比程式正確性和安全性驗證的示意圖;
一種利用圖同構驗證編譯器的方法
圖2《一種利用圖同構驗證編譯器的方法》中順序結構的結點標識示意圖;
圖3《一種利用圖同構驗證編譯器的方法》中條件結構的結點標識示意圖;
圖4《一種利用圖同構驗證編譯器的方法》中do_while循環結構的結點標識示意圖;
圖5《一種利用圖同構驗證編譯器的方法》中while_do循環結構的結點標識示意圖;
一種利用圖同構驗證編譯器的方法
圖6《一種利用圖同構驗證編譯器的方法》的流程示意圖。
一種利用圖同構驗證編譯器的方法

技術領域

《一種利用圖同構驗證編譯器的方法》涉及核電領域,具體涉及核電中用於生成安全級代碼的編譯器的安全性驗證方法。

權利要求

1.一種利用圖同構驗證編譯器的方法,包括待處理的源程式和將源程式生成目標程式的編譯器,在選定環境下建立一個反編譯器,通過反編譯器將目標程式反編譯成對比程式,驗證對比程式和源程式之間的語義一致性,其特徵在於,在此基礎上分別建立源程式和對比程式的控制流圖相關結點信息後進行同構判定,從而得到編譯器是否安全的結論,具體步驟如下:
步驟1、首先對源程式和對比程式的語句按順序進行掃描,並利用帶序號的結點進行標識;
步驟2、同時建立一個輔助棧表,並將當前結點及相關結點信息壓入輔助棧表框;
步驟3、對條件結構的所有結點進行簡化並用簡化結點替代,然後將簡化結點壓入輔助棧表原條件結構的結點位置處形成簡化棧表,並且在程式中所有結點被掃描完成之後,將棧表中的結點依次出棧,在上述簡化過程中,建立該結點的鄰接鍊表,同時建立一個記錄簡化結點信息的簡化信息表;
步驟4、根據結點的鄰接鍊表和簡化信息表建立源程式和對比程式的出入度信息,並生成相應的n點連通子圖的出入度序列,1<=n<N-1,N是結點個數;
步驟5、根據出入度序列判斷源程式和對比程式的控制流圖是否同構;其中,當兩個控制流圖中的任意n點連通子圖的出入度序列相同時,則表明兩個控制流圖是同構的,進而表明源程式與目標程式是相同的,並得到編譯器是安全的結果;反之,則證明編譯器是不安全的。
2.如權利要求1所述的一種利用圖同構驗證編譯器的方法,其特徵在於,所述步驟1中,結點的添加標準如下:
步驟11、首先在源程式和對比程式的開始和結尾分別增加一個開始結點和終止結點;
步驟12、順序執行的語句用一個結點標識;
步驟13、條件語句的起始句用一個條件起始結點標識,中間的各條件表達式分別用一個中間結點標識,同時增加一個條件語句的條件結束結點;
步驟14、循環語句的起始句用一個執行結點標記,結尾語句用一個判斷結點標記;
步驟15、在分析時遇到return語句則單獨添加一個返回結點。
3.如權利要求1所述的一種利用圖同構驗證編譯器的方法,其特徵在於,各結點的出邊連線方法如下:
步驟31、按各結點排列順序依次連線;
步驟32、遇到條件語句的結點時,條件起始結點與各中間條件表達式的中間結點按順序連線,如遇到返回結點時,則返回結點的出邊直接與終止結點連線,否則按順序連線條件結束結點;
步驟33、遇到循環語句的結點時,執行語句結點指向判斷結點,判斷結點分別指向執行語句結點和順序排列的下一個結點。
4.如權利要求1所述的一種利用圖同構驗證編譯器的方法,其特徵在於,所述輔助棧表的基本信息包括如下內容:
A、按分析順序生成的各結點的類型,包括順序類型、條件類型和循環類型,各類型以相應結構的起始句為標識進行區分;
B、各結點對應的排列序號;
C、每個結點所包含的結點數量;
D、所包含的return語句數量。
5.如權利要求1所述的一種利用圖同構驗證編譯器的方法,其特徵在於,所述步驟3中,鄰接鍊表記錄每個結點的出邊信息,並記錄所有鄰接鍊表的表頭指針信息以作為檢索信息。
6.如權利要求1所述的一種利用圖同構驗證編譯器的方法,其特徵在於,所述步驟3中,簡化信息表的內容包括結點名、被簡化結構包含的結點個數、起始結點和終止結點名,以及所涉及的return分支數量。
7.如權利要求1所述的一種利用圖同構驗證編譯器的方法,其特徵在於,所述步驟4中,出入度序列的建立方法如下:
步驟41、根據鄰接鍊表中的結點信息統計出各結點的出度和入度信息;
步驟42、然後依次讀取簡化信息表中各結點的信息,並用簡化結點及其出度、入度信息去更換被簡化結構相應位置結點的出度、入度信息,同時更新該被簡化塊的出入度信息,並且連同該簡化塊的結點總數一起記錄下來;
步驟43、分別統計更新後源程式和對比程式的n點連線子圖的出入度,並對其中的出度和入度按大小進行排序。

實施方式

《一種利用圖同構驗證編譯器的方法》利用圖同構驗證編譯器的方法,包括待處理的源程式和將源程式生成目標程式的編譯器,在選定環境下建立一個反編譯器,通過反編譯器將目標程式反編譯成對比程式,驗證對比程式和源程式之間的語義一致性,在此基礎上分別建立源程式和對比程式的控制流圖相關結點信息後進行同構判定,《一種利用圖同構驗證編譯器的方法》的驗證環境是C語言。
如圖1所示,例:首先用待驗證編譯器Generator將源程式programA轉換成目標程式programB;
新開發一個針對目標程式programB的反編譯器Generator_verify;
將目標程式programB利用反編譯器Generator_verify編譯生成對比程式programA’;
如果想驗證編譯器Generator的正確性,可以通過靜態分析、模型檢驗或者自動定理證明等方式來驗證programA和programA’的語義一致性來達到目的。
而為檢測編譯器Generator的安全性則需要首先建立源程式programA和對比程式programA’控制流圖信息,然後進行同構判定。
《一種利用圖同構驗證編譯器的方法》的實現原理是:控制流圖可以由鄰接鍊表表示法來存儲,並且這種方法便於計算每個結點的出入度,因此《一種利用圖同構驗證編譯器的方法》採取鄰接鍊表的存儲方式記錄結點的出邊信息;為獲得程式的控制流圖結點信息,並且便於後續圖同構的判定,只需要計算每個連通子圖的出入度,所以,在蒐集程式控制流圖信息的過程中重點記錄圖中每個結點的出入度,以及連通子圖的出入度信息;然後根據記錄的結點信息建立連通子圖的出入度序列並進行比較,以判斷源程式和對比程式的控制流圖是否同構的結論。
程式控制流圖是描述程式控制邏輯的一種有向圖,圖中的每個結點對應於一個順序流程的程式代碼塊或者謂詞,弧對應程式的轉移。對於程式來說,其控制流圖比較特殊,只有循環結構塊的部分存在強連通子圖,其餘的結構只存在單向連通子圖,所以在對程式結構進行歸約的過程中重點記錄每個被簡化結構塊的結點個數,以及該結構與圖中其餘結點相聯繫的連線點。
在符合結構化程式設計思想這一前提下,一個程式的控制流圖可由下述三種基本結構組合而成:順序結構、if-elseif-…-else和switch代表的分支結構、while-do和do-while代表的循環結構,其中順序結構中的語句可以擴展,可以是分支結構或循環結構。
如圖6所示,《一種利用圖同構驗證編譯器的方法》的具體步驟如下:
101、首先對源程式和對比程式的語句按順序進行掃描,並利用帶序號的結點進行標識,同時標明各結點的出邊信息;
1、首先在源程式和對比程式的開始和結尾分別增加一個開始結點和終止結點,如:START和END分別表示起始和結束結點。
2、然後對整個程式進行分析並增加相應結點,在出入邊的連線上,基本原則是按各結點排列順序依次連線,遇到條件語句的結點時,條件起始結點與各中間條件表達式的中間結點按順序連線,如遇到返回結點時,則返回結點的出邊直接與終止結點連線,否則按順序連線條件結束結點;如:
如圖2所示,順序執行的語句作為一個基本塊,如果最後的語句不是return語句,由一個結點代替;否則,除return之外的語句由一個結點代替,而return單獨一個結點。
如圖3所示,對於條件語句的選擇結構塊,起始句用一個條件起始結點標識,中間的各條件表達式分別用一個中間結點標識,同時增加一個條件語句的條件結束結點;如:是if-elseif-…-else,則增加一個中間結點IFELSE_END1,並將所有的條件表達式作為謂詞結點,順次連線,所有的條件語句按照順序結構處理,該結構塊的入邊連線點為對應的條件表達式,出邊連線點為IFELSE_END1。但選擇結構塊中如果含有return語句,則出邊連線END結點。
是switch時,將表達式及其對應的case值都作為謂詞結點順次連線,case語句的處理和if一致,記增加的中間結點為SWITCH_END1。結點之間的連線關係和if-elseif-…-else結構一致。
遇到循環語句的結點時,執行語句結點向判斷結點出邊,判斷結點分別向執行語句結點和順序排列的下一個結點出邊。如圖4、5所示,分別是do_while和while_do兩種循環結構的結點標識示意。
102、同時建立一個輔助棧表,並將當前結點及相關結點信息壓入輔助框;
其中輔助棧表用於壓入順序掃描時標識的結點及相關結點信息,這些結點信息與生成的後繼結點有關,為結點的連線提供信息,其中的結點信息包括結點類型、結點序號和當前結點的數量以及return語句數量,當是條件結構時,結點的數量則為此結構所包含的結點個數,上述信息為判定控制流圖同構時提供信息,
1、其中的結點類型記錄每條語句的類型,如:是return語句記為RETURN,其餘順序結構的語句記為STATEMENT,如果是do_while循環結構的第一條語句序號,其類型記為DOWHILE_STATEMENT;每個塊結構的開始謂詞則記為IFELSE_PREDICATE、SWITCH_PREDICATE、WHILEDO_PREDICATE,其餘謂詞的均為PREDICATE;
2、結點序號為每條語句或者塊的序號;
3、結點數目num,記錄每個結點的個數,如果是簡化結點,則記錄的是被簡化結構塊所包含的結點個數;
4、Retrun語句數目retun_num,記錄return語句的數目,主要是為了在簡化條件結構時,統計該結構與其它結點的連線信息。
輔助棧表的內容如下表所示:
一種利用圖同構驗證編譯器的方法
為了解每個結點的信息,《一種利用圖同構驗證編譯器的方法》針對輔助棧表中的每一個結點分別建立一個鄰接鍊表Li,用於記錄每個結點的出邊對應的鄰接點,即對控制流圖的每個結點建立一個鄰接關係的單鍊表,每個結點的單鍊表表示以該結點為起點的所有的下一個鄰接點的信息。並把他們的表頭指針及結點存儲起來,便於檢索。並增加結點START和END的鍊表,分別表示開始結點和結束結點。
103、對條件結構的所有結點進行簡化並用簡化結點替代,然後將簡化結點壓入輔助棧表原條件結構的結點位置處形成簡化棧表,並且在程式中所有結點被掃描完成之後,將棧表中的結點依次出棧,在上述簡化過程中,建立該結點的鄰接鍊表,同時建立一個記錄簡化結點信息的簡化信息表;
1、具體簡化過程為:讀取輔助棧表中的內容並依次出棧去更新簡化棧表,如遇到選擇結構塊IFELSE_PREDICATE時,增加一個替換的簡化結點並壓入輔助棧表中,將該IFELSE_PREDICATE選擇結構塊中包含的所有結點由此簡化結點代替,即用名稱為IFELSE_BLOCK1的簡化結點代表當前的選擇結構塊結點名,如用IFELSE_BLOCK1表示簡化結點名,在輔助棧表中的信息即為STATEMENT,IFELSE_BLOCK1,sum,sum_return其中四項所表示的內容與輔助棧表中的意思一致,只是sum在這裡代表的是此簡化結點共簡化了幾個結點數量,sum_return代表該被簡化結構直接相聯接地return分支數量,對應於該結構的出邊,而壓入了簡化結點的輔助棧表就變成了簡化棧表。
針對簡化棧表中的簡化結點,用一個簡化信息表來記錄,包括簡化結點的名稱、簡化前的結點數量,被簡化結構塊的起始和終止結點,被簡化塊中包含的return分支個數,例:
IFELSE_BLOCK1在簡化信息棧表中的記錄信息為IFELSE_BLOCK1,sum,IFELSESTART1,IFELSE_END1,sum_return,其中IFELSESTART1為IFELSE_PREDICATE對應結點名,IFELSE_END1為結束結點。如果sum:=1,則不存在結點IFELSE_END1,記錄為IFELSE_BLOCK1,1,IFELSESTART1,/\,sum_return。如下表所示,
一種利用圖同構驗證編譯器的方法
在處理SWITCH選擇結構塊時,其處理過程與IFELSE相同。
2、如果遇到循環結構塊,如是while_do循環結構,則將當前輔助棧表的棧頂元素對應的輔助鍊表指向類型為WHILEDO_PREDICATE對應的結點。
更新鄰接鍊表:輔助棧表的次棧頂元素對應的鄰接鍊表指向棧頂元素,更新sum:=sum+top(S).num,棧頂元素出棧,依次執行此動作,直到遇到類型為WHILEDO_PREDICATE的元素。
當WHILEDO_PREDICATE對應的元素出棧後,sum:=sum+top(S).num;增加新的結點,假設序號名為WHILEDO_BLOCK1,將STATEMENT,WHILEDO_BLOCK1,sum,0信息壓入簡化棧表中。然後更新簡化棧表的內容:假設W6HILEDO_PREDICATE對應結點名為WHILEDO_START1,則將WHILEDO_BLOCK1,num,WHILEDO_START1,/\,0信息壓入簡化棧表。如WHILEDO循環結構的簡化過程如下表所示:
一種利用圖同構驗證編譯器的方法
如果是do_while循環結構,則:將當前輔助棧表的棧頂元素對應的鄰接鍊表指向類型為DOWHILE_STATEMENT對應的結點,並將棧頂元素對應的name記錄下來,假設為DOWHILE_END1。
如果當前棧頂元素類型不為DOWHILE_STATEMENT,則次棧頂元素對應的鄰接鍊表指向棧頂元素,更新sum:=sum+top(s).num,棧頂元素出棧。依次執行此動作,直到遇到類型為DOWHILE_STATEMENT的元素。當DOWHILE_STATEMENT對應的元素出棧,sum:=sum+top(s).num;增加新的結點,假設結點名為DOWHILE_BLOCK1,將STATEMENT,DOWHILE_BLOCK1,sum,0信息壓入簡化棧表中。
假設DOWHILE_STATEMENT對應結點名為DOWHILE_START1,將DOWHILE_BLOCK1,num,DOWHILE_START1,DOWHILE_END1,0壓入簡化棧表然,再返回輔助棧表的處理。如DOWHILE循環結構的簡化過程如下表所示:
一種利用圖同構驗證編譯器的方法
3、當程式中的所有語句被掃描完之後,輔助棧表的棧頂元素對應的鄰接鍊表指向END結點;如果棧頂元素類型為STATEMENT,num=1,retun_num!=0,則棧頂元素不指向任何結點。然後次棧頂元素對應的輔助鍊表指向棧頂結點,棧頂元素出棧。如果次棧頂元素不為空,依次執行此動作。將START結點對應的鄰接鍊表指向輔助棧表中最後一個元素對應的結點,結束。
104、根據結點的鄰接鍊表和簡化信息表建立源程式和對比程式的出入度信息,並生成相應的n點連通子圖的出入度序列;
由於前面步驟已經對程式進行了簡化,將選擇和循環結構歸約為一條語句的結點形式,針對每層被簡化結構塊,其內部的結點是順序結構,只有一個入邊和一個出邊,因此,在判斷同構時,只需要統計單個結點的出入度和被簡化連通子圖的出入度信息即可。首先根據每個結點的鄰接鍊表,統計出各結點的出度和入度信息,再讀取簡化棧表中各結點的信息,遇到簡化結點時,用簡化結點及其出度、入度信息去更新被簡化結構塊相關結點的出度、入度信息,其中對源程式和對比程式的控制流圖的出入度信息獲取步驟如下:
1、需要遍歷每個結點的鄰接鍊表,以計算出每個結點的出度di和入度do,再採用依次讀取簡化信息表的方式,逐個更新被簡化結構塊的起始和終止結點的出入度信息,更新方法如下:
2、如簡化棧表的棧頂元素類型為IFELSE選擇結構塊化簡類型,形式如(IFELSE_BLOCK1,num,IFELSESTART1,IFELSE_END1,return_num)。如果num!=1,被簡化的選擇結構塊包含多個結點,IFELSE_BLOCK1的入度為該選擇結構塊的第一個結點的入度,IFELSE_BLOCK1的出度為該選擇結構塊最後一個結點的出度,因此更新原選擇結構塊的第一個結點入度和最後一個結點的出度的內容如下:IFELSESTART1.di:=IFELSE_BLOCK1.di+IFELSESTART1.di,IFELSE_END1.do:=IFELSE_END1.do+IFELSE_BLOCK1.do;同時記錄該結構被簡化前的出入度信息和結點個數,假設記為S_IFELSE_BLOCK1:=(IFELSE_BLOCK1,num,IFELSE_BLOCK1.di,IFELSE_BLOCK1.do+return_num)。如果num:=1,被簡化的選擇結構塊分支都指向END結點,此時IFELSE_BLOCK1結點實際上是原選擇結構塊的第一個結點,且IFELSE_BLOCK1沒有後繼結點,出度為0,因此更新原選擇結構塊的第一個結點的入度如下:IFELSESTART1.di:=IFELSE_BLOCK1.di+IFELSESTART1.di;
如果簡化棧表棧頂元素類型為SWITCH選擇結構塊化簡類型,形式如(SWITCH_BLOCK1,num,SWITCH_START1,SWITCH_END1,return_num),其處理過程和IFELSE選擇結構塊處理方式一致;
3、如果簡化棧表的棧頂元素類型為WHILEDO循環結構塊化簡類型,形式如(WHILEDO_BLOCK1,num,WHILEDO_START1,/\,0),則記錄該結構的出度和入度,以及num值,假設記為LOOP_WHILEDO_BLOCK1:=(WHILEDO_BLOCK1,num,WHILEDO_BLOCK1.di,WHILEDO_BLOCK1.do);然後更新WHILEDO_START1.di=WHILEDO_START1.di+WHILEDO_BLOCK1.di,WHILEDO_START1.do=WHILEDO_START1.do+WHILEDO_BLOCK1.do;
如果簡化棧表的棧頂元素類型為DOWHILE循環結構塊化簡類型,形式如(DOWHILE_BLOCK1,num,DOWHILE_START1,DOWHILE_END1,0),則記錄結點DOWHILE_BLOCK1的出度和入度,以及num值,假設為LOOP_DOWHILE_BLOCK1:=(DOWHILE_BLOCK1,num,DOWHILE_BLOCK1.di,DOWHILE_BLOCK1.do);然後更新DOWHILE_START1.di:=DOWHILE_START1.di+DOWHILE_BLOCK1.di,DOWHILE_END1.do:=WHILEDO_BLOCK1.do+WHILEDO_END1.do。
4、分別統計更換後源程式和對比程式的各結點的出入度序列,並對其中的出度和入度按大小進行排序;對被簡化的結構,根據對其結構塊包含的結點個數,以及該結構塊的出入度信息記錄,建立n點連通子圖的出入度序列,方法如下:
其中需要將所有結點的出度和入度分別從大到小進行排序(簡化後的結點除外),構成n=1時的出入度序列:Si(1),So(1);
針對所有的條件塊簡化後對應的結點信息記錄,按照其結點個數進行分類,如LOOP_DOWHILE_BLOCK1:=(DOWHILE_BLOCK1,num,DOWHILE_BLOCK1.di,DOWHILE_BLOCK1.do)歸類為num=k點聯通子圖,其入度為di,出度為do;將所有的k點類連通子圖的出入度從大到小進行排序,構成k點連通子圖的出入度序列Si(k),So(k)。
105、根據出入度序列判斷源程式和對比程式的控制流圖是否同構。
根據出入度序列判斷源程式和對比程式的控制流圖是否同構。
其中,當兩個控制流圖中的任意n點連通子圖的出入度序列相同時,則表明兩個控制流圖是同構的,進而表明源程式與目標程式是相同的,並得到編譯器是安全的結果;反之,則證明編譯器是不安全的。
即對於任意的1<=n<N-1,N是結點個數,分別比較兩個圖的出入度序列Si(n),So(n),如果均相同,則同構;否則不同構。

榮譽表彰

2018年12月20日,《一種利用圖同構驗證編譯器的方法》獲得第二十屆中國專利優秀獎。

相關詞條

熱門詞條

聯絡我們