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

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

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

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

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

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

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