可信軟件開發(fā)框架下的出具證明編譯研究.pdf

1、隨著國(guó)家和社會(huì)對(duì)軟件的依賴程度日益增長(zhǎng)，軟件的安全性越來(lái)越受到關(guān)注，軟件的安全性主要包括safety和security兩個(gè)方面。Safety是指軟件運(yùn)行時(shí)不引起危險(xiǎn)、災(zāi)難的能力，而security是指軟件系統(tǒng)對(duì)數(shù)據(jù)和信息提供保密性、完整性、可用性、真實(shí)性保障的能力。本文的研究主要關(guān)注軟件的safety，但是軟件的safety和security是有聯(lián)系的，黑客通常就是利用緩沖區(qū)溢出、數(shù)組訪問(wèn)越界、懸空指針訪問(wèn)等低級(jí)的safety錯(cuò)誤，來(lái)破

2、壞系統(tǒng)和獲得未經(jīng)授權(quán)的控制等。因此提高safety有助于保證security。 提高safety的目標(biāo)是：所有的程序錯(cuò)誤在程序運(yùn)行前被發(fā)現(xiàn)或者在程序運(yùn)行時(shí)被溫和地捕獲，以保證程序不會(huì)導(dǎo)致不可預(yù)測(cè)的系統(tǒng)行為。軟件安全性研究主要是探索建立一個(gè)管理安全性的健全的科學(xué)和技術(shù)基礎(chǔ)，其中軟件滿足安全策略的證明方法(即程序性質(zhì)證明)‘是研究的熱點(diǎn)之一。程序性質(zhì)證明既可以采用基于類型的方法也可以采用基于邏輯的方法，近年來(lái)還有人提出了邏輯和類型相

3、結(jié)合的方法。然而在程序性質(zhì)證明方面，現(xiàn)有的研究不是集中于高級(jí)語(yǔ)言層次就是集中于低級(jí)語(yǔ)言層次，而很少同時(shí)考慮高級(jí)語(yǔ)言和低級(jí)語(yǔ)言的。基于高級(jí)語(yǔ)言的研究易于程序員使用、且可以更早發(fā)現(xiàn)程序的安全問(wèn)題，但是被信任計(jì)算基礎(chǔ)(TCB)比較大，而基于低級(jí)語(yǔ)言的研究雖然TCB比較小但是形式大多比較復(fù)雜，難以被程序員使用從而也難以應(yīng)用到實(shí)際當(dāng)中。一些出具證明的編譯器雖然能根據(jù)源程序信息產(chǎn)生其匯編代碼的證明，但可證明的程序性質(zhì)大都是一些源級(jí)類型系統(tǒng)可以表達(dá)的

4、性質(zhì)，一些復(fù)雜的性質(zhì)例如值相關(guān)的性質(zhì)并沒有在考慮的范圍內(nèi)。 基于上述考慮，本文設(shè)計(jì)了一種可信軟件開發(fā)框架，該框架的特點(diǎn)是同時(shí)包含了源級(jí)和目標(biāo)級(jí)的程序性質(zhì)證明，并且使用出具證明編譯器根據(jù)源級(jí)規(guī)范和證明自動(dòng)生成目標(biāo)級(jí)證明。該框架可以表達(dá)的程序性質(zhì)不僅局限于類型，還可以是更復(fù)雜的程序性質(zhì)，比如值相關(guān)的部分正確性。本文在該框架下主要探討了出具證明編譯的相關(guān)技術(shù)，即編譯器在翻譯源代碼到匯編代碼的同時(shí)，根據(jù)源級(jí)安全規(guī)范和證明附帶生成匯編代碼

5、滿足等效規(guī)范的證明，并同匯編代碼一同輸出。這些證明可以被底層證明檢查器所檢查，以證明生成的匯編代碼滿足安全規(guī)范。本文的工作主要基于類型化匯編語(yǔ)言(Typed Assembly Language)、驗(yàn)證匯編編程(Certified Assembly Programming)和攜帶證明代碼(Proof-CarryingCode)等研究，采用的是類型和邏輯相結(jié)合的研究方法。本文首先介紹了國(guó)內(nèi)外基于程序性質(zhì)證明的軟件安全的相關(guān)研究和出具證明編譯

6、的研究，然后提出了一個(gè)可信軟件開發(fā)框架，隨后本文著重介紹了在這個(gè)框架下的出具證明編譯技術(shù)，以及一個(gè)相應(yīng)的出具證明編譯器的設(shè)計(jì)和實(shí)現(xiàn)。這些技術(shù)包括驗(yàn)證條件生成技術(shù)，底層代碼規(guī)范(斷言)的翻譯和生成技術(shù)，以及底層證明的生成技術(shù)。本文還討論了出具證明的編譯特性對(duì)傳統(tǒng)編譯技術(shù)的影響。 本文的主要特色和貢獻(xiàn)為： ·提出了一個(gè)可信軟件開發(fā)框架。它向程序員提供源級(jí)程序性質(zhì)證明接口，允許程序員提供源級(jí)規(guī)范和源程序滿足規(guī)范的證明，并通過(guò)出

7、具證明編譯器產(chǎn)生目標(biāo)程序滿足等效規(guī)范的證明。對(duì)目標(biāo)級(jí)證明的檢查可以將代碼編譯器排除出系統(tǒng)TCB，從而提高程序可信性：而目標(biāo)級(jí)證明的自動(dòng)生成則減輕了程序員的負(fù)擔(dān)。 ·改進(jìn)設(shè)計(jì)了源級(jí)驗(yàn)證條件生成算法。該算法將證明源程序滿足安全規(guī)范的問(wèn)題轉(zhuǎn)化為證明驗(yàn)證條件正確性的問(wèn)題。該算法還合并了源語(yǔ)言定型規(guī)則中的附加條件收集，同時(shí)也考慮了生成的驗(yàn)證條件的化簡(jiǎn)問(wèn)題。源級(jí)驗(yàn)證條件的證明可以使程序的安全問(wèn)題盡早暴露。 ·設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)出具證明