編譯過程安全性基礎(chǔ)研究.pdf

1、程序安全性已成為現(xiàn)代軟件開發(fā)中必須重視的關(guān)鍵問題。在軟件開發(fā)流程中，從設(shè)計到編碼到編譯為最終的可執(zhí)行代碼，任何一個階段的安全隱患都可能導(dǎo)致最終軟件的安全性問題。因此，對軟件開發(fā)流程的各個階段進(jìn)行安全性測試是保證軟件質(zhì)量的一個必要部分。在軟件開發(fā)過程中，編譯器負(fù)責(zé)從軟件源代碼到目標(biāo)代碼的變換這一重要階段，因此編譯過程的正確性和安全性對軟件的安全性有著非常大的影響。目前，針對軟硬件系統(tǒng)的形式化驗證技術(shù)發(fā)展迅速，相關(guān)工具的工具也逐步成熟，這些

2、進(jìn)步使得對編譯器這類復(fù)雜的軟件進(jìn)行驗證成為可能。由于編譯驗證在安全軟件開發(fā)中的重要意義，它已經(jīng)成為當(dāng)前研究的一個熱點。 本文以編譯過程驗證為主要研究方向，針對編譯驗證的核心問題，對編譯器安全性的驗證方法進(jìn)行了探索研究，其中包括對程序?qū)傩缘拿枋雠c分析方法的研究，以及對基本的編譯驗證方案的探索。文中提出了一種基于程序分析的編譯驗證框架，該框架基于對編譯過程中個階段的編譯中間表示形式的分析驗證編譯過程是否保證了特定的安全特性。文中研究

3、了對源語言程序和中間代碼的安全屬性分析方法，提出了一種新穎的算法，并將利用其對重要的軟件安全屬性進(jìn)行分析。另外，文中還提出了一種新穎有效的二進(jìn)制代碼的分析方案，將對高級語言程序的屬性檢查方法擴(kuò)展到了可執(zhí)行程序的領(lǐng)域，因此使得能夠采用統(tǒng)一的分析方法完成程序在編譯各個階段的各種形式的安全屬性驗證，從而為本文提出的編譯驗證框架提供了有效的安全屬性分析手段。主要研究內(nèi)容包括： (1)在深入分析編譯驗證的根本問題和研究方法的基礎(chǔ)上，提出了

4、一種基于程序分析的編譯驗證框架。在該驗證框架中，編譯驗證與分析作為一個獨立的大模塊集成到一個已有編譯器實現(xiàn)中，通過對編譯各個階段中的程序形式的安全屬性檢查，驗證編譯器實現(xiàn)的正確性與安全性。 (2)針對基于程序分析的編譯驗證框架的基本需求，在深入分析程序基本屬性的形式化描述方法的基礎(chǔ)上，研究了內(nèi)存安全屬性與信息流安全屬性這兩種重要的安全屬性的描述方法，提出了基于類型精化方法的內(nèi)存安全性的統(tǒng)一表示方法。類型精化是基于對已有類型進(jìn)行擴(kuò)

5、展的一種方法，這種方法對于描述程序的安全屬性有著重要的意義。另外，還將類型擴(kuò)展技術(shù)應(yīng)用在信息流安全屬性描述方面，并以SSA中間語言作為載體進(jìn)行了信息流安全屬性描述的一個實例研究。 (3)在分析了編譯器的典型實現(xiàn)技術(shù)的基礎(chǔ)上，提出了對編譯幾個主要階段的正確性驗證方法。在分析了parse(從具體語法到抽象語法的語法解析技術(shù))與unparse(從抽象語法到具體語法，將抽象語法樹線性化)之間的關(guān)系，提出基于parse-unparse的編譯前端驗

6、證方案?；趯Υa實現(xiàn)算法的分析與研究，提出了基于對樹重寫條件檢查的正確性驗證方案，對樹模式匹配的條件進(jìn)行檢驗，從而驗證代碼生成算法的正確性?；趯幾g優(yōu)化算法實現(xiàn)的深入分析，提出了一種能夠有效地表示程序中的數(shù)據(jù)流屬性以及控制流屬性的擴(kuò)展屬性文法，并基于此提出了基于屬性文法計算程序?qū)傩圆⑸沙绦虻某橄竽Ｐ?，進(jìn)而利用模型檢測工具檢驗編譯優(yōu)化正確性的驗證方案。 (4)在深入研究了程序分析方法之后，提出了基于類型分析與模型檢測方法相結(jié)

7、合的混合式分析方法TCMC(Type Checking and Model Checking)，并將其應(yīng)用于程序的內(nèi)存安全屬性以及信息流安全性分析。其中特別針對內(nèi)存泄漏的靜態(tài)分析方法，說明了TCMC算法的應(yīng)用，及其相對于類型分析方法的優(yōu)勢。 (5)在深入分析底層代碼的驗證問題及其研究方法的基礎(chǔ)上，提出了一種新的目標(biāo)機(jī)器代碼分析方法。該方法基于反編譯技術(shù)恢復(fù)程序中的控制流，并基于恢復(fù)的控制流圖對程序進(jìn)行數(shù)據(jù)流分析和類型分析，也可以

8、將控制流圖轉(zhuǎn)換到SSA形式，進(jìn)而利用TCMC算法進(jìn)行程序安全屬性的分析。 本文做出的主要貢獻(xiàn)如下： (1)提出一個基于程序分析的編譯驗證框架。該框架建立在一個具有良好模塊化結(jié)構(gòu)的編譯器實現(xiàn)之上，各個主要驗證模塊作為對編譯器的擴(kuò)展很方便地集成到編譯器的編譯過程中。該框架利用SSA形式作為統(tǒng)一的編譯中間表示形式，便于程序?qū)傩苑治?，也便于向框架中添加自定義的分析模塊。 (2)提出基于類型精化的內(nèi)存安全性統(tǒng)一表示，同時提

9、出了在SSA中間表示形式上基于類型擴(kuò)展進(jìn)行信息流安全編碼的方法。這部分程序?qū)傩悦枋龇椒ǖ难芯繛轵炞C框架中的屬性檢測方法研究打下了基礎(chǔ)。 (3)提出了類型分析與模型檢測方法相結(jié)合的TCMC算法，并將其應(yīng)用于程序安全屬性的分析過程中。該算法避免了類型分析算法對控制流不敏感的不足，利用模型檢測算法對類型分析的結(jié)果進(jìn)行分析，提高了分析的精度，同時也避免了單純使用模型檢測算法進(jìn)行分析可能造成的較大時間開銷。 (4)提出了基于反編譯