驗證帶有線程動態(tài)創(chuàng)建和退出的多線程程序.pdf

1、隨著計算機硬件平臺運算能力的不斷提升，計算機軟件的規(guī)模及復(fù)雜度日益增長，同時軟件安全性問題也日益突出。如何解決軟件安全性，已然成為目前計算機工業(yè)領(lǐng)域與研究領(lǐng)域關(guān)注的熱點問題。當(dāng)前軟件主要依靠安全的程序設(shè)計語言與軟件測試來提高軟件的可靠性。然而安全的程序設(shè)計語言，如Java、C＃等提供的眾多安全特性都依賴于其運行環(huán)境；軟件測試則很大程度依賴于測試者的能力，且軟件測試有著與生俱來的不完備性，測試用例很難覆蓋軟件使用時所遇到的全部情況，因此經(jīng)

2、過測試的軟件依然可能存在著安全隱患。程序驗證是計算機研究領(lǐng)域針對解決軟件安全性問題，從而構(gòu)建高可信軟件提出的一種應(yīng)對方案。程序驗證中使用形式化的方法對軟件進(jìn)行驗證，形式化的方法基于數(shù)學(xué)的特種技術(shù)，因此程序驗證具有完備性和可靠性，經(jīng)過程序驗證為安全的軟件，安全性具有極高的可信度。綜上所述，為了提高軟件的安全性和可靠性，使用程序驗證的方法驗證軟件的安全性具有重要意義。
　　 在目前的軟件開發(fā)中，多線程技術(shù)大量應(yīng)用，為研究如何驗證應(yīng)用

3、多線程技術(shù)的軟件的安全性，本文使用程序驗證的方法對帶有線程動態(tài)創(chuàng)建和退出操作的多線程程序的安全性進(jìn)行驗證。本文的工作使用基于攜帶證明的代碼技術(shù)，使用Hoare邏輯的匯編語言級形式化程序驗證方法(CAP)，提出了一種驗證帶有線程動態(tài)創(chuàng)建和退出的多線程程序的驗證框架。該驗證框架包含抽象機模型、指令規(guī)范、邏輯推理系統(tǒng)、驗證框架的可靠性定理及證明。本文的具體工作，包括驗證框架的形式化定義以及驗證框架的可靠性證明，是在計算機輔助定理證明工具Coq

4、[4]中實現(xiàn)的，這些實現(xiàn)是計算機可檢查的，從而保證了整個驗證框架的嚴(yán)格性和可靠性。
　　 通過驗證工作，本文研究了多線程程序在線程的動態(tài)創(chuàng)建和退出中出現(xiàn)的問題，特別是內(nèi)存劃分的改變及內(nèi)存的初始化和銷毀。同時，本文還介紹了這些工作在計算機輔助定理證明工具Coq中的實現(xiàn)，包括如何在Coq中定義數(shù)據(jù)結(jié)構(gòu)、機器指令等，以及Coq證明中的難點。
　　 本文的工作是對原有的AIM驗證框架的擴展，主要貢獻(xiàn)和創(chuàng)新包括：1)通過對線程的動

5、態(tài)創(chuàng)建和銷毀機制進(jìn)行研究，擴展框架在運行時系統(tǒng)及并發(fā)用戶代碼部分都形式化的給出了線程動態(tài)創(chuàng)建和銷毀的規(guī)范，并在原框架中加入顯式的內(nèi)存推理機制，從而提出了一個推理帶有線程動態(tài)創(chuàng)建和銷毀機制多線程程序的方法；2)提出了對程序內(nèi)存劃分的顯式的推理機制，該機制可用于驗證底層程序的內(nèi)存劃分；3)使用計算機輔助定理證明工具Coq實現(xiàn)了框架的形式化定義及可靠性證明。
　　 本文的工作是在原有工作基礎(chǔ)上對證明操作系統(tǒng)做出的進(jìn)一步嘗試。操作系統(tǒng)包