GCC編譯器安全驗(yàn)證方法研究.pdf

1、編譯器作為計(jì)算機(jī)軟件中最為基礎(chǔ)的軟件之一，與操作系統(tǒng)、數(shù)據(jù)庫(kù)系統(tǒng)一起被列為構(gòu)成計(jì)算機(jī)系統(tǒng)軟件的關(guān)鍵性的基礎(chǔ)設(shè)施。而編譯器作為任何軟件的產(chǎn)生器，它的安全性、可靠性和穩(wěn)定性更是至關(guān)重要。特別是在那些對(duì)軟件的可靠性要求十分高的特殊環(huán)境里面，我們必須保證編譯器編譯出來(lái)的代碼是對(duì)程序源代碼的正確、真實(shí)的反應(yīng)，保證編譯器在編譯過(guò)程中邏輯上的正確性以及行為上的透明性。 本文首先研究了目前國(guó)內(nèi)外對(duì)于軟件驗(yàn)證，特別是編譯器驗(yàn)證領(lǐng)域的一些工作進(jìn)展。

2、主要包括形式化的驗(yàn)證方法、模型校驗(yàn)、目標(biāo)文件結(jié)構(gòu)比較等等方法，分析并討論了這些方法在理論上的優(yōu)缺點(diǎn)以及它們?cè)趯?shí)踐應(yīng)用中的效果。本文對(duì)于編譯器的安全性的關(guān)注點(diǎn)在于：驗(yàn)證編譯器是否在編譯階段在輸出目標(biāo)代碼中插入惡意的代碼或者后門(mén)程序。 之后本文提出了兩種可行的編譯器驗(yàn)證方案：編譯器代碼分析及對(duì)比驗(yàn)證以及目標(biāo)碼邏輯結(jié)構(gòu)對(duì)比驗(yàn)證。 在第一個(gè)方案中，我們以GCC編譯器為例，試圖將GCC編譯器源代碼中的所有函數(shù)分成兩類：對(duì)于那些會(huì)在

3、函數(shù)內(nèi)部改變它的輸入數(shù)據(jù)的函數(shù)，影響編譯器最終輸出結(jié)果的，我們將它們歸類為第一類；對(duì)于那些在函數(shù)內(nèi)部不會(huì)改變輸入數(shù)據(jù)的函數(shù)，不影響編譯器最終輸出結(jié)果的，我們將它們歸類為第二類。對(duì)于第二類函數(shù)，我們?cè)诤瘮?shù)的入口處將所有輸入數(shù)據(jù)保存，然后在函數(shù)返回時(shí)將所有輸入數(shù)據(jù)與之前保存的數(shù)據(jù)進(jìn)行對(duì)比，如果對(duì)比成功，則證明該函數(shù)的確沒(méi)有改變編譯器的最終輸出結(jié)果；對(duì)于第一類函數(shù)，我們將人工地檢查這些函數(shù)的代碼并且由一組獨(dú)立的小組將這些函數(shù)根據(jù)描述重新實(shí)現(xiàn)，

4、然后對(duì)比原先這些函數(shù)的運(yùn)行結(jié)果以及獨(dú)立實(shí)現(xiàn)的函數(shù)運(yùn)行結(jié)果，如果結(jié)果一致，則表示該函數(shù)安全。 第二個(gè)方案中，本文采用了一種對(duì)比編譯器的輸出目標(biāo)文件與源文件的控制流邏輯結(jié)構(gòu)的方案。在這個(gè)方案中，我們采用GCC編譯器編譯一份源代碼，然后提取源代碼和編譯以后目標(biāo)碼的控制流圖的結(jié)構(gòu)，使用同構(gòu)圖算法對(duì)這兩個(gè)控制流圖進(jìn)行比較，如果這兩份控制流圖的邏輯對(duì)比一致，那么可以證明該編譯器在編譯過(guò)程中沒(méi)有插入惡意代碼，即證明這目標(biāo)編譯器在行為上安全的。