一種用于指針程序安全性證明的指針邏輯.pdf

1、在社會(huì)逐漸走入信息時(shí)代的今天，社會(huì)的各個(gè)層面，包括工業(yè)界、政府機(jī)關(guān)、學(xué)校、商業(yè)部門等，都和計(jì)算機(jī)軟件等信息系統(tǒng)結(jié)合越來越緊密。信息系統(tǒng)中的任何一個(gè)環(huán)節(jié)工作失敗或是遭受攻擊都會(huì)帶來難以預(yù)料的災(zāi)難性后果，因而軟件安全的重要性與日俱增。用形式化的方法對軟件進(jìn)行嚴(yán)格推理是提高軟件質(zhì)量的根本途徑。在眾多的形式化方法中，近十年來基于程序設(shè)計(jì)語言理論和實(shí)現(xiàn)技術(shù)的軟件安全研究引起了廣泛的關(guān)注。基于語言理論的研究從程序基礎(chǔ)出發(fā)考慮軟件安全，有利于減小運(yùn)算

2、系統(tǒng)的受信任計(jì)算基礎(chǔ)(Trusted Computing Base，簡稱TCB)。 未來高安全軟件設(shè)計(jì)和開發(fā)的一種行之有效的方式將是基于程序性質(zhì)證明的開發(fā)框架。在這個(gè)框架中，程序設(shè)計(jì)者將軟件的安全策略等描述成程序應(yīng)滿足的規(guī)范，連同程序一起提交給編譯器；編譯器生成為證明程序滿足規(guī)范所需的驗(yàn)證條件，并且利用內(nèi)嵌的定理證明器自動(dòng)地或交互地證明這些驗(yàn)證條件；編譯器在把源程序翻譯成目標(biāo)代碼的同時(shí)，將源程序滿足規(guī)范的證明翻譯成目標(biāo)代碼滿足等

3、效規(guī)范的證明，這樣的編譯器稱為出具證明的編譯器(certifyingcompiler)；在目標(biāo)代碼一級由證明檢驗(yàn)器利用代碼所攜帶的證明自動(dòng)進(jìn)行代碼滿足規(guī)范的檢驗(yàn)。該框架的主要優(yōu)點(diǎn)是，它向程序設(shè)計(jì)者提供源級而不是目標(biāo)級的程序性質(zhì)證明方法，以提高安全程序的開發(fā)效率，同時(shí)它將編譯器、證明器等排除出受信任的計(jì)算基礎(chǔ)，以盡量縮小系統(tǒng)的TCB。 作為上述基于程序性質(zhì)證明的軟件安全長期研究工作的一個(gè)環(huán)節(jié)和組成部分，本文在指針邏輯以及基于指針邏

4、輯的源代碼性質(zhì)描述和性質(zhì)證明方面做了有益探索。 本文首先研究了一個(gè)強(qiáng)調(diào)指針類型的類C的命令式語言源語言PointerC的設(shè)計(jì)并給出了它的安全性證明。PointerC語言設(shè)計(jì)的主要出發(fā)點(diǎn)是：已有軟件安全和出具證明編譯的研究大多集中在類型安全等簡單安全策略上；而本文研究的高安全程序設(shè)計(jì)框架關(guān)注更實(shí)際、更豐富的安全策略，如內(nèi)存安全等，因此，PointerC保留了C語言指針特性。本文給出了一種易于程序員理解的安全語言描述方式，并嘗試以類

5、型系統(tǒng)和邏輯系統(tǒng)相結(jié)合的靜態(tài)機(jī)制來推理程序的安全性。本文利用輔助定理證明工具Coq，機(jī)械證明了PointerC語言的安全性定理。 本文研究了一種指針邏輯系統(tǒng)。指針邏輯擴(kuò)展了傳統(tǒng)Hoare邏輯，并加入了新的推理規(guī)則以支持對指針操作的推理，因此指針邏輯為證明指針程序的安全性提供了可行的途徑。本文給出了針邏輯系統(tǒng)在一個(gè)出具證明編譯器原型系統(tǒng)中的實(shí)現(xiàn)，該原型證明系統(tǒng)包括一個(gè)驗(yàn)證條件生成器和定理證明器，能夠根據(jù)指針邏輯的公理和推理規(guī)則，自

6、動(dòng)完成斷言的生成和證明；并且，這些代碼、斷言和證明可以被出具證明的編譯器繼續(xù)翻譯到目標(biāo)語言級。本文利用輔助定理證明工具Coq，機(jī)械證明了指針邏輯對于操作語義的可靠性定理。本文研究了指針邏輯在面向?qū)ο笳Z言上的應(yīng)用。本文設(shè)計(jì)了一個(gè)小的面向?qū)ο笳Z言Cool并定義了它的形式語義；Cool保留了Java語言核心的的語法元素，如類、對象、繼承等。本文擴(kuò)展了指針邏輯以增加對這些新語言特性的支持。除了作為通用的程序邏輯外，本文還研究了指針邏輯在靜態(tài)垃圾