一種用于指針程序安全性證明的指針邏輯.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)難性后果，因而軟件安全的重要性與日俱增。用形式化的方法對(duì)軟件進(jìn)行嚴(yán)格推理是提高軟件質(zhì)量的根本途徑。在眾多的形式化方法中，近十年來基于程序設(shè)計(jì)語(yǔ)言理論和實(shí)現(xiàn)技術(shù)的軟件安全研究引起了廣泛的關(guān)注?；谡Z(yǔ)言理論的研究從程序基礎(chǔ)出發(fā)考慮軟件安全，有利于減小運(yùn)算

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

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

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

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