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

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

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

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

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

5、架的擴(kuò)展，主要貢獻(xiàn)和創(chuàng)新包括：1）通過(guò)對(duì)線程的動(dòng)態(tài)創(chuàng)建和銷毀機(jī)制進(jìn)行研究，擴(kuò)展框架在運(yùn)行時(shí)系統(tǒng)及并發(fā)用戶代碼部分都形式化的給出了線程動(dòng)態(tài)創(chuàng)建和銷毀的規(guī)范，并在原框架中加入顯式的內(nèi)存推理機(jī)制，從而提出了一個(gè)推理帶有線程動(dòng)態(tài)創(chuàng)建和銷毀機(jī)制多線程程序的方法；2）提出了對(duì)程序內(nèi)存劃分的顯式的推理機(jī)制，該機(jī)制可用于驗(yàn)證底層程序的內(nèi)存劃分；3）使用計(jì)算機(jī)輔助定理證明工具Coq實(shí)現(xiàn)了框架的形式化定義及可靠性證明。
　　 本文的工作是在原有工作