本文選題：驗(yàn)證編譯器　切入點(diǎn)：機(jī)器檢測(cè)　出處：《武漢大學(xué)》2016年博士論文

【摘要】：編譯器是將高級(jí)語(yǔ)言編寫的程序轉(zhuǎn)換到能在目標(biāo)平臺(tái)上運(yùn)行指令集的重要系統(tǒng)軟件。但是,由于高級(jí)語(yǔ)言的規(guī)范復(fù)雜,多以自然語(yǔ)言描述,導(dǎo)致編譯器編寫者在實(shí)現(xiàn)語(yǔ)言時(shí),對(duì)一些模糊的語(yǔ)義定義理解困難,不知道應(yīng)該翻譯為怎樣的機(jī)器指令；此外,編譯器本身是一個(gè)大型復(fù)雜的軟件,即使編譯器編寫者明確知道了語(yǔ)言的準(zhǔn)確定義,他們?cè)趯?shí)現(xiàn)該編程語(yǔ)言時(shí)也很可能存在編碼問(wèn)題。因此,大多數(shù)編譯器雖然在發(fā)布前已經(jīng)進(jìn)行了大量測(cè)試,但仍存在許多問(wèn)題。這些問(wèn)題對(duì)于安全攸關(guān)的軟件系統(tǒng)來(lái)說(shuō),即使出現(xiàn)概率很小,也可能造成重大的人員傷亡與經(jīng)濟(jì)損失。因此,通過(guò)測(cè)試手段檢測(cè)的編譯器仍然是不可信任的。編譯器問(wèn)題使得在高級(jí)語(yǔ)言程序上進(jìn)行程序驗(yàn)證的努力很可能付之東流,因此,需要對(duì)編譯器的正確性進(jìn)行形式化證明。本文以“語(yǔ)義等同性”來(lái)形式化定義編譯器的正確性為指導(dǎo)思想,研究了一個(gè)機(jī)器檢測(cè)的驗(yàn)證編譯器,它的源語(yǔ)言是符合面向?qū)ο?Object-Oriented,OO)語(yǔ)言特性的一個(gè)具有較大實(shí)用性的Java語(yǔ)言子集mJava,目標(biāo)語(yǔ)言是一種寄存器架構(gòu)的虛擬機(jī)(Virtual Machine,VM),Micro-Dalvik,以Android Dalvik VM作為參考。為了達(dá)到這個(gè)研究目標(biāo),使用定理證明助手Isabelle/HOL,本文從以下三個(gè)方面展開(kāi)了研究。(1)機(jī)器檢測(cè)的mJava源語(yǔ)言及目標(biāo)機(jī)器Micro-Dalvik VM語(yǔ)言的形式語(yǔ)義對(duì)于mJava源語(yǔ)言,定義了一個(gè)具有較大實(shí)用性的Java語(yǔ)言子集,除了塊、順序、條件、循環(huán)語(yǔ)句等基本語(yǔ)法結(jié)構(gòu)外,它包括封裝、繼承、方法重載和覆蓋以及異常處理等。然后基于抽象語(yǔ)法,歸納定義了每一個(gè)抽象語(yǔ)法結(jié)構(gòu)的語(yǔ)義規(guī)則,從而定義出mJava語(yǔ)言的大步操作語(yǔ)義(big-step operational semantics),并定義mJava源語(yǔ)言表達(dá)式的類型規(guī)則以及程序的良構(gòu)性。對(duì)于目標(biāo)機(jī)器,對(duì)Dalvik VM指令集進(jìn)行抽象,支持封裝、繼承、方法重載和覆蓋以及異常處理等,得到Micro-Dalvik VM指令集,定義Micro-Dalvik VM狀態(tài),定義單條指令執(zhí)行的語(yǔ)義函數(shù)和語(yǔ)義關(guān)系,程序執(zhí)行是任意有限步的單條指令執(zhí)行,是單條指令執(zhí)行語(yǔ)義關(guān)系的自反傳遞閉包。(2) mJava程序到Micro-Dalvik VM程序的編譯及正確性證明定義了中間語(yǔ)言程序Ji_prog的抽象語(yǔ)法和語(yǔ)義,通過(guò)生成中間語(yǔ)言程序,將mJava程序分兩步翻譯成Micro-Dalvik目標(biāo)機(jī)器指令程序。首先,mJava源程序中的本地變量名按照其聲明順序轉(zhuǎn)換為所對(duì)應(yīng)的序號(hào),成為中間語(yǔ)言程序；然后,將組成Ji_prog程序中的每個(gè)子表達(dá)式轉(zhuǎn)換成一條或多條Micro-Dalvik指令,并生成異常表。編譯正確性的證明也分為兩步,對(duì)編譯前后的語(yǔ)義等同性分別進(jìn)行歸納證明,從而證明了編譯mJava程序到Micro-Dalvik VM程序的正確性。(3)Micro-Dalvik字節(jié)碼驗(yàn)證器和類型保持的編譯字節(jié)碼驗(yàn)證器(Bytecode Verifier,BV)是DalvikVM的重要組成部分,其主要任務(wù)是類型檢查。因此,從類型的角度對(duì)Micro-Dalvik虛擬機(jī)進(jìn)一步展開(kāi)研究。首先基于數(shù)據(jù)流分析算法,定義了Micor-Dalvik VM的類型系統(tǒng),并證明了它的可靠性。接著實(shí)現(xiàn)了一個(gè)可執(zhí)行的字節(jié)碼驗(yàn)證器,證明了它的正確性。最后,對(duì)于良類型(well-typed)的mJava程序,證明編譯后生成的字節(jié)碼程序通過(guò)了字節(jié)碼驗(yàn)證器的檢查,從而證明了語(yǔ)義等同的驗(yàn)證編譯器也保持了類型的可靠性,于是進(jìn)一步奠定了它的正確性。因此,本文在定理證明助手Isabelle/HOL的支持下,驗(yàn)證了一個(gè)具有面向?qū)ο筇匦缘脑凑Z(yǔ)言,mJava,編譯到寄存器架構(gòu)的虛擬機(jī),Micro-Dalvik的語(yǔ)義等同性,并證明了良類型的mJava源程序經(jīng)該驗(yàn)證編譯器編譯后,所生成的字節(jié)碼程序的類型可靠性。在這個(gè)實(shí)現(xiàn)過(guò)程中,提出了一個(gè)較為完整的寄存器架構(gòu)的Micro-Dalvik VM形式模型,該模型包括了虛擬機(jī)的抽象語(yǔ)法和語(yǔ)義,以及一個(gè)基于數(shù)據(jù)流分析算法的類型系統(tǒng),證明了該類型系統(tǒng)的可靠性,并實(shí)現(xiàn)了一個(gè)證明正確的字節(jié)碼驗(yàn)證器。同時(shí),本文研究工作也證實(shí)了機(jī)器(交互式定理證明工具Isabelle/HOL)驗(yàn)證一個(gè)復(fù)雜程序,即編譯Java語(yǔ)言子集到Dalvik VM子集正確性的可行性。本文給出的形式化定義和證明較為清晰和直觀,易于擴(kuò)展,可維護(hù)性高,應(yīng)該有潛力應(yīng)用于安全攸關(guān)的工業(yè)軟件開(kāi)發(fā)中。
[Abstract]:......
【學(xué)位授予單位】：武漢大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP314

【參考文獻(xiàn)】

相關(guān)期刊論文 前3條

1 何炎祥;吳偉;劉陶;李清安;陳勇;胡明昊;劉健博;石謙;;可信編譯理論及其核心實(shí)現(xiàn)技術(shù):研究綜述[J];計(jì)算機(jī)科學(xué)與探索;2011年01期

2 田波;陳意云;王偉;李兆鵬;王志芳;;一個(gè)出具證明編譯器后端的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)工程;2009年07期

3 胡榮貴,陳意云,郭帆,張昱;基于類型注解的認(rèn)證編譯器設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)研究與發(fā)展;2004年01期

，

本文編號(hào)：1665264