模塊化構造軟件系統安全性證明的研究.pdf

1、計算機程序正逐步影響到人類社會的方方面面。無論在互聯網還是個人電腦上，計算機程序的安全問題日益嚴峻。然而現實世界中的程序并不盡如人意，病毒肆虐，網絡攻擊防不勝防。這些問題都源于程序中潛伏著許多錯誤，其中一個小的錯誤有可能會導致整個軟件系統的崩潰。而在諸多關鍵的領域，例如核反應堆、航天飛機的控制系統等等，計算機程序的半點閃失都將帶來不可計數的慘痛損失。在軟件開發(fā)過程中使用形式化的方法是提高軟件質量的途徑。在眾多的形式化方法中，程序的靜態(tài)驗

2、證是一種非?？煽康姆椒ā?本文采用方法是在攜帶證明的代碼的框架中靜態(tài)地驗證程序。所謂攜帶證明的代碼是首先靜態(tài)地驗證代碼的安全性，然后將這個驗證的詳細過程作為安全性證明附加在程序上。主機在運行程序前檢查程序攜帶的安全性證明的正確性。如果安全性證明是正確的，那么說明程序滿足主機的安全策略，可以安全地運行而不破壞主機上的軟件系統。 本文首先在一個簡單的驗證框架中定義了程序、抽象機器、抽象機器的操作語義、安全，還有一個用來靜態(tài)驗

3、證程序的推理系統。此框架可以用來構造簡單的攜帶證明的代碼。然而與以前的許多相關研究一樣，此框架不能很好地支持模塊化的程序驗證?，F實中的大量程序通常使用模塊化的開發(fā)方式，模塊化的開發(fā)方式可以把一個復雜的程序分解為若干個小的模塊，不同的模塊分別被開發(fā)，最后這些模塊可以被鏈接到一起從而構成完整的程序。模塊性在軟件工程方面占有重要的地位。程序靜態(tài)驗證也應該具備模塊性，即不同模塊的驗證可以分別進行，然后鏈接成為完整的安全性證明。另一方面，一個程序

4、的不同模塊可能是不同風格的代碼，難以使用同一種驗證推理系統去驗證所有的模塊。 本文在簡單驗證框架上進行擴展，使之支持模塊化驗證。在此模塊化框架中不同的模塊可以分開進行驗證，并分別得到各自的安全性證明，模塊在鏈接的同時安全性證明也被鏈接到一起，從而得到整個程序的安全性證明。而且此框架支持不同的模塊使用不同的驗證邏輯進行驗證。框架的特點是采用一個抽象的程序推理系統，它支持良好的模塊驗證。多個驗證推理系統可以被統一嵌入到這個抽象的程序

5、推理系統中。通過采用這種方法，一個模塊不管使用哪些推理系統進行驗證，只要這個驗證推理系統可以被嵌入到抽象層次上，那么這個模塊的安全性證明就可以被轉換成抽象的推理系統中的安全性證明。本文研究了如何將一個支持控制棧推理的驗證推理系統嵌入到驗證框架中，并移植了一個已有的動態(tài)內存分配模塊。同時本文還研究了如何將一個類型化的驗證推理系統嵌入到驗證框架中，并驗證了一個小的調用動態(tài)內存分配的模塊。最后本文介紹了如何將兩個使用不同的推理系統驗證的模塊連

6、同安全性證明鏈接到一起。 本文還研究了框架中的各個模塊的安全性證明產生的自動性問題。本文不僅提出了驗證推理系統SCAP中的驗證條件生成器，而且提出了驗證推理系統TALP的類型檢查器。通過驗證條件生成器與類型檢查器的可靠性證明，模塊的安全性證明的構造過程被大大簡化。有利于驗證規(guī)模較大的模塊。 文中所有的形式化定義，形式化描述以及證明都已使用的定理輔助證明工具Coq實現。因此所有的證明，包括框架的性質證明，示例程序的安全性證