模塊化構(gòu)造軟件系統(tǒng)安全性證明的研究.pdf

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

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

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

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

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

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