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

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

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

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

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

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

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

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

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

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