（計(jì)算機(jī)軟件與理論專業(yè)論文）基于uml行為模型的軟件漏洞檢測(cè)形式方法研究.pdf

a b s tr a c t w i 廿lt h ed e v e l o p m e n to ft h ea p p l i c a t i o no fc o m p u t e rt e c h n o l o g i e s ，t h eh i g h r e l i a b i l i t yo fs o f t w a r ei sm o r ea n dm o r ei m p o r t a n t t h ef o r m a lm e t h o d sa r es o m e p r e c i s es p e c i f i c a t i o na n dv e r i f i c a t i o nb a s e dt ot h em a t h e m a t i ca n dl o g i c a ll a n g u a g e a l s ot h e s ef o r m a lm e t h o d sa r ei m p o r t a n tt oe n s u r et h eh i g hr e l i a b i l i t yo fs o f t w a r e t h em o d e lc h e c k i n gi sav e r i f i c a t i o nt e c h n o l o g yo ft h ef o r m a lm e t h o d s t h er e s e a r c h o fm o d e lc h e c k i n gt h e o r i e sa n dt h ea p p l i c a t i o no ft h i st e c h n o l o g ya r eb e c o m i n gt h e h o tt o p i ci nt h el a s tf e wy e a r sb o ma th o m ea n da b r o a d s of a rt h e r ea r eg r e a t s u c c e s s e so ft h ea p p l i c a t i o no fm o d e lc h e c k i n gi nt h ec o m p u t e rh a r d w a r e ，s e c u r e p r o t o c o lv e r i f i c a t i o na n ds oo n i no r d e rt oi m p l e m e n tt h eh i g hr e l i a b i l i t yo fs o f t w a r e ，w es h o u l df i r s tl c a ma n d s t u d ys o f t w a r ev u l n e r a b i l i t i e s i nt h i sa r t i c l e ，n o to n l yt h ec a t e g o r i e so fs o f t w a r e v u l n e r a b i l i t i e sa r eg i v e nb u ta l s ot h ea n a l y s i sa n dd e f i n i t i o no fs p e c i a ls o f t w a r e v u l n e r a b i l i t ya r eg j v e n 1 1 1 el o 百c a ll a n g u a g e sa r et h eb a s i co fm o d e lc h e c k i n g i n o r d e rt om a s t e rt h em o d e lc h e c k i n gt e c h n o l o g y ，t h ec o m p u t a t i o nt r e el o 西c ( c t l ) a n dt h el i n e a rt e m p e r a ll o g i c ( l t l ) a r ed e s c r i b e d t h em o d e lc h e c k i n gt o o ls p i ni s s e l e c t e d t h e r e f o r e ，n o to n l yt h et h e o r yo fs p i ni sl e a r n e db u ta l s ot h ei n p u tl a n g u a g e p r o m e l ai si n t r o d u c e si nd e t a i l t h e r ea r et w om a i ni d e a sf o rt h ea p p l i c a t i o no f m o d e lc h e c k i n gi nv e r i f i c a t i o nt h e s o t l v a r ev u l n e r a b i l i t i e s o n ei st h em o d e lc h e c k i n gi nt h er e q u i r e m e n t sp h a s ea n dt h e o t h e ri st h em o d e lc h e c k i n gi nt h et e s t i n gt h et a r g e tc o d e sp h a s e t h i st o p i cs e l e c t st h e f o r m e ra n di m p l e m e n t st h ef o r m a lv e r i f i c a t i o no ft h es o f t w a r ed e s i g n i n gm o d e l sb a s e d o nt h eu m la c t i o nm o d e l s t h eu m lm o d e l i n gi st h em a i nv i s u a lm o d e l i n gm e t h o d s i nt h es o f t - w a r ed e v e l o p m e n t st o d a y t h em o d e li n gp r o c e s si no t h e rf o r m a lm e t h o d s h a sp r o b l e m ss u c ha st h ev i s u a lm o d e l i n ga n ds oo n t h u s t h ei n t e g r a t i o no ft h e s et w o m o d e l i n gm e t h o d sc a l le f f e c t i v e l yr e d u c et h ed i 伍c u l t i e so fv e r i f i c a t i o no nt h e s o f t w a r ev u l n e r a b i l i t i e s t h em a i ns t u d yi so nt h em o d e lc h e c k i n gt h eu m la c t i o nm o d e l si nt h e r e q u i r e m e n tp h a s e s f i r s t ，t h et r a n s f o r mr u l e sf r o mt h eu m l a c t i o nm o d e l st ot h e e x t e n d e dh i e r a r c h i c a la u t o m a t a ( e h a ) m o d e l sa r ed e s c r i b e d i n0 r d e rt oe x p l a i n t h e s er u l e sc l e a r l y , t h et r a n s f o r m a t i o np r o c e s s e si si m p l e m e n t e dw i t ht h ea t m e x a m p l e s e c o n d ，t h ef r a m e w o r kw i t hp r o m e l ai sg i y e nt od e s c r i b et h ee h am o d e l s o fs o m eu m la c t i v ed i a g r a me l e m e n t s a tt h es a m et i m e t h em o d e lc h e c k i n g 。p r o c e s s e sw i t hs p i nb a s e do nt h eu m la c t i v ed i a g r a mi n t e g r a t e d t h ed i n n i n g p h i l o s o p h e r sp r o b l e ma r ee x h i b i t e dp a r t i c u l a r l v a l s ot h ev e r i f i c a t i o nr e s u l t so f d e a d l o c ki nt h i sp r o b l e ma r ea l s od i s p l a y e d k e yw o r d s ：t h ef o r m a lm e t h o d s ； m o d e lc h e c k i n g ； s o f t w a r ev u l n e r a b i l i t i e s ； u m la c t i v em o d e l 9川9 8337川川1 洲y 目錄 第一章引言1 1 1 研究目的和意義1 1 2 國(guó)內(nèi)外研究動(dòng)態(tài)2 1 3 創(chuàng)新點(diǎn)和主要工作3 1 4 章節(jié)安排4 第二章軟件漏洞及其檢測(cè)理論7 2 1 軟件漏洞7 2 1 1 軟件漏洞概述7 2 1 2 典型的軟件漏洞8 2 2 軟件漏洞的檢測(cè)方法9 第三章模型檢測(cè)理論及s p i n 1 1 3 1 模型檢測(cè)概述1 1 3 2 模型檢測(cè)工具1 3 3 3s p i n 的輸入語(yǔ)言p r o m e l a 1 6 3 3 1p r o m e l a 概述1 6 3 3 2p r o m e l a 交互實(shí)例分析2 0 3 4s p i n 的輸入語(yǔ)言l t l 2 3 3 4 1 時(shí)序邏輯語(yǔ)言概述2 3 3 4 2 線性時(shí)序邏輯l t l 2 5 3 4 3 軟件漏洞的l t l 描述實(shí)例分析2 7 第四章基于e h a 的u m l 行為模型建模研究3 1 4 1 統(tǒng)一建模語(yǔ)言u(píng) m l 3 1 4 2 擴(kuò)展層次自動(dòng)機(jī)e h a 3 4 4 3u m l 行為模型到e h a 的轉(zhuǎn)換規(guī)則3 6 4 3 1 狀態(tài)圖的轉(zhuǎn)換規(guī)則3 6 4 3 2 活動(dòng)圖的轉(zhuǎn)換規(guī)則3 8 4 4e h a 模型到p r o m e l a 語(yǔ)言的轉(zhuǎn)換規(guī)則4 1 第一章引言 1 1 研究目的和意義 第一章引言 從2 0 世紀(jì)9 0 年代米期開(kāi)始，因特網(wǎng)r 臻成熟和計(jì)算機(jī)廣泛應(yīng)用，引發(fā)了一 場(chǎng)全球范圍內(nèi)的信息革命，全球信息化的步伐不斷加快，信息化社會(huì)正在形成并 走向成熟。 人們對(duì)計(jì)算機(jī)的依賴性與日俱增，這使得計(jì)算機(jī)的安全故障產(chǎn)生的各種危害 也是空前的增加。1 9 6 6 年歐洲航天局發(fā)射的火箭在升空后，緊緊3 7 秒鐘就爆炸 墜毀。人們?cè)趯?duì)這次慘劇進(jìn)行分析和研究時(shí)才發(fā)現(xiàn)了此次空難的原因，火箭的 慣性制導(dǎo)系統(tǒng)的軟件存在一個(gè)微小的規(guī)約和設(shè)計(jì)錯(cuò)誤。然而，如果在當(dāng)時(shí)采用了 模型檢測(cè)技術(shù)，就能夠很好的檢測(cè)出軟件在設(shè)計(jì)時(shí)存在的這類邏輯漏洞，這次耗 資8 0 億美元的航空計(jì)劃就不會(huì)失敗了。軟件的高可靠性要求成為軟件開(kāi)發(fā)的首 要問(wèn)題，尤其是在安全攸關(guān)領(lǐng)域更是如此。高可靠性軟件和系統(tǒng)受到了廣泛的重 視，成為計(jì)算機(jī)科學(xué)技術(shù)研究的重要熱點(diǎn)。美國(guó)國(guó)家宇航局( n a s a ) 于1 9 9 5 年 7 月和1 9 9 7 年5 月先后發(fā)布了形式化方法規(guī)范和驗(yàn)證指南；美國(guó)國(guó)家自然科 學(xué)基金會(huì)在2 0 0 0 年財(cái)政年度啟動(dòng)了至今為止規(guī)模最大的研究計(jì)劃，強(qiáng)調(diào)利用驗(yàn) 證和形式化方法來(lái)保證系統(tǒng)行為的正確可靠性等等。 應(yīng)用形式化方法的目的就是保證軟件的可靠性。上世紀(jì)6 0 年代，面對(duì)當(dāng)時(shí) 的軟件危機(jī)，f l o y d 、h o a r e 和m a n n a 等學(xué)者進(jìn)行了程序的正確性證明研究，他 們用數(shù)學(xué)方法來(lái)證明程序的正確性并發(fā)展了各種程序正確性驗(yàn)證方法。上世紀(jì)八 十年代，在硬件方面的形式化方法的應(yīng)用熱潮，使得很多學(xué)者不斷地研究將形式 化方法應(yīng)用在軟件領(lǐng)域。p n u e l i 提出了反應(yīng)式系統(tǒng)規(guī)格和驗(yàn)證的時(shí)態(tài)邏輯方法。 c l a r k e 和e m e r s o n 提出了對(duì)有窮狀態(tài)并發(fā)系統(tǒng)的模型檢測(cè)方法。上世紀(jì)9 0 年代 以來(lái)，形式化研究和在工業(yè)中的應(yīng)用得到了長(zhǎng)足的發(fā)展。 形式化方法可以定義為：“用于開(kāi)發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法是基于數(shù)學(xué)的 用于描述系統(tǒng)性質(zhì)的技術(shù)。這樣的形式化方法提供了一個(gè)框架，人們可以在該框 架中以系統(tǒng)的方式刻畫、開(kāi)發(fā)和驗(yàn)證系統(tǒng)”。 2 1 形式化方法可以分為形式化規(guī)格和形式化驗(yàn)證。其中，形式化規(guī)格方法有： 有限狀態(tài)機(jī)、s t a t e c h a r t s 、p e t r i 網(wǎng)、z ( z e d ) 、v d m ( v i e n n ad e v e l o p m e n tm e t h o d ) 、 l a r c h 、b 方法口1 、時(shí)段演算、x y z e 3 等基于時(shí)序邏輯的方法。形式化驗(yàn)證包括 模型檢測(cè)和定理證明。定理證明有b a n 邏輯、k a i l a r 邏輯等證明方法畸1 。 形式化方法從產(chǎn)生到現(xiàn)在，已經(jīng)開(kāi)發(fā)了一系列不同的方法和工具。因此，不 斷地學(xué)習(xí)和掌握網(wǎng)際上先進(jìn)的形式化方法，并且將形式化方法技術(shù)應(yīng)用于我國(guó)的 國(guó)防、科技、辦公、工業(yè)生產(chǎn)等各個(gè)方面，成為我國(guó)軟件領(lǐng)域的重要課題。 青島大學(xué)碩i ：學(xué)位論文 模型檢測(cè)技術(shù)是形式化方法的主要技術(shù)之一。模型檢測(cè)理論的研究與創(chuàng)新， 以及將模型檢測(cè)技術(shù)應(yīng)用于軟件領(lǐng)域也成為今年來(lái)研究的重要內(nèi)容。本文主要研 究了如何將模型檢測(cè)技術(shù)應(yīng)用到軟件漏洞檢測(cè)方面。傳統(tǒng)的軟件檢測(cè)技術(shù)，往往 是在軟件開(kāi)發(fā)后期，對(duì)軟件成品的檢測(cè)。在軟件開(kāi)發(fā)初期，對(duì)軟件進(jìn)行邏輯漏洞 的檢測(cè)可以大大的減少軟件開(kāi)發(fā)成本。目前，幾乎所有軟件開(kāi)發(fā)者，在開(kāi)發(fā)初期 使用統(tǒng)一建模語(yǔ)言( u m l ) 對(duì)軟件功能、框架、角色以及動(dòng)作序列等進(jìn)行描述。 因此，對(duì)軟件漏洞的檢測(cè)可以對(duì)軟件開(kāi)發(fā)初期的u m l 模型，使用模型檢測(cè)技術(shù)進(jìn) 行漏洞檢測(cè)。 1 2 國(guó)內(nèi)外研究動(dòng)態(tài) 軟件漏洞的形式化檢測(cè)方法的研究可以根據(jù)不同的標(biāo)準(zhǔn)分為不同的方面： ( 1 ) 按照軟件開(kāi)發(fā)階段，形式化檢測(cè)方法主要分為軟件開(kāi)發(fā)初期即需求分 析階段和設(shè)計(jì)階段的形式化檢測(cè)方法研究和軟件測(cè)試階段的形式化檢測(cè)方法的 研究。 ( 2 ) 按照軟件性質(zhì)的不同，形式化檢測(cè)方法主要分為安全協(xié)議的形式化檢 測(cè)方法研究和實(shí)時(shí)混成系統(tǒng)的形式化檢測(cè)方法研究。 ( 3 ) 按照軟件漏洞的性質(zhì)的不同，分為針對(duì)不同漏洞的形式化檢測(cè)方法。 基于軟件開(kāi)發(fā)階段的形式化檢測(cè)方法的研究，主要是對(duì)軟件開(kāi)發(fā)初期的需求 分析階段的設(shè)計(jì)模型進(jìn)行形式化規(guī)格與驗(yàn)證，很多學(xué)者在研究的過(guò)程基于u m l 視 圖模型進(jìn)行各種形式化研究。 u m l 雖然采用了四層體系結(jié)構(gòu)，但是它的語(yǔ)法結(jié)構(gòu)還不是形式化意義上的定 義，而是基于自然語(yǔ)言和u m l 子集元素的描述。在對(duì)其描述的模型進(jìn)行定量定性 分析和驗(yàn)證時(shí)，很難采用形式化的方法。因此，基于u m l 的形式化研究已經(jīng)成為 了國(guó)內(nèi)外學(xué)術(shù)界關(guān)注的熱點(diǎn)。 國(guó)外的學(xué)術(shù)界對(duì)u m l 語(yǔ)義進(jìn)行形式化研究的兩個(gè)主要思路是晦1 ： 一方面是對(duì)u m l 核心語(yǔ)法進(jìn)行形式化，使u m l 成為符合形式化規(guī)范的語(yǔ)言。 英國(guó)的p u m l ( p r e c i s eu m lg r o u p ) 運(yùn)用淺顯的數(shù)學(xué)知識(shí)描述元模型層次的元素， 從而建立u m l 模型層和用戶對(duì)象層的數(shù)學(xué)模型基礎(chǔ)。文獻(xiàn)u m l 和謂詞轉(zhuǎn)換入手， 可以建立一組和u m l 相對(duì)應(yīng)的數(shù)學(xué)模型。文獻(xiàn)對(duì)狀態(tài)圖中的各種狀態(tài)及遷移函數(shù) 進(jìn)行了形式化定義。文獻(xiàn)定義了一種包含對(duì)象流描述u m l 活動(dòng)圖的形式化語(yǔ)義。 另方面，利用形式化語(yǔ)言在不丟失或少丟失信息的前提下對(duì)u m l 進(jìn)行形式 化。該方法對(duì)每種u m l 圖形賦予形式化語(yǔ)言，然后利用已有的形式化語(yǔ)言和工具 對(duì)u m l 模型進(jìn)行推理驗(yàn)證。文獻(xiàn)口1 使用p e t r i 網(wǎng)元素，將u m l 的四個(gè)模型元素進(jìn) 行了描述，并且實(shí)現(xiàn)了從u m l 活動(dòng)圖模型到p e t r i 網(wǎng)的轉(zhuǎn)換算法。l a t e l l a 和 s t e f a n i a m l 等分析了u m l 的模型元素的語(yǔ)義，使用自動(dòng)機(jī)描述u m ls t a t e c h a r t s 2 第一章引言 中的模型元素，并且使用模型檢測(cè)工具s p i n 對(duì)實(shí)例進(jìn)行了驗(yàn)證，同時(shí)證明了自 動(dòng)機(jī)模型與u m ls t a t e c h a r t s 模型的一致性問(wèn)題。s t e f a n i ag n e s i 和f r a n c o m a z z a n t i 一1 將u m l 動(dòng)態(tài)行為模型看作是一組交互狀態(tài)自動(dòng)機(jī)，基于分支時(shí)間邏輯 一a c t l 和演算，使用模型檢測(cè)工具對(duì)u m l 模型進(jìn)行了驗(yàn)證。 國(guó)內(nèi)的研究主要在以下幾個(gè)方面： 國(guó)內(nèi)在軟件開(kāi)發(fā)初期的研究主要是對(duì)u m l 模型進(jìn)行形式化驗(yàn)證。文獻(xiàn)們提出 了基于自動(dòng)機(jī)理論的活動(dòng)圖模型檢測(cè)方法，該方法首先建立系統(tǒng)自動(dòng)機(jī)，然后將 系統(tǒng)的待測(cè)屬性使用l t l 公式描述，為性質(zhì)的否定命題建立b u c h i 自動(dòng)機(jī)。計(jì)算 兩個(gè)自動(dòng)機(jī)的乘積。最后檢查該乘積自動(dòng)機(jī)所能接受的語(yǔ)言是否為空。這種方法 雖然給我們提供了一種檢測(cè)u m l 活動(dòng)圖屬性檢測(cè)的方法，但是，這種方法需要有 自動(dòng)機(jī)理論基礎(chǔ)的人才能運(yùn)用。在實(shí)際應(yīng)用之中，這種方法難以被工作人員接受。 因此，能夠簡(jiǎn)單地應(yīng)用到實(shí)際工作中的模型檢測(cè)方法及工具，成為專家學(xué)者的主 要研發(fā)目標(biāo)。分析了u m l 狀態(tài)圖的結(jié)構(gòu)特點(diǎn)和語(yǔ)義特征，構(gòu)造了層次化著色p e t r i 網(wǎng)h c p n 。主要解決了使用p e t r i 網(wǎng)進(jìn)行形式化驗(yàn)證的問(wèn)題。文獻(xiàn)1 使用k r i p k e 結(jié)構(gòu)賦予了u m l 狀態(tài)圖形式化語(yǔ)義，提出并證明了u m l 狀態(tài)圖和k r i p k e 結(jié)構(gòu)語(yǔ) 義的雙映射關(guān)系。為了更好的研究u m l 類圖，從而適應(yīng)形式化描述方法時(shí)序 邏輯語(yǔ)言x y z e 來(lái)表示類圖形式化語(yǔ)義的方法。對(duì)順序圖的形式化研究方法主要 采用將順序圖轉(zhuǎn)換為元模型的描述語(yǔ)言0 c l ，然后將o c l 轉(zhuǎn)換為x y z 語(yǔ)言，進(jìn)行 形式化驗(yàn)證。對(duì)u m l 狀態(tài)圖的形式化研究主要引入了有線自動(dòng)機(jī)，作為u m l 狀態(tài) 圖和s p i n 之間的橋梁，將復(fù)雜的多層u m l 狀態(tài)圖分解為多個(gè)子自動(dòng)機(jī)，并且提 出了a t t p 算法，將自動(dòng)機(jī)描述為p r o m e l a 代碼。微軟的模型檢測(cè)工具m o p s ，并 且自己實(shí)現(xiàn)了工具m c s ，對(duì)l i n u x 系統(tǒng)進(jìn)行了安全屬性的分析與驗(yàn)證。將u m l 模 型轉(zhuǎn)換為p e t r i 網(wǎng)模型，再利用p e t r i 網(wǎng)的分析驗(yàn)證技術(shù)，可以實(shí)現(xiàn)對(duì)軟件模型 的正確性的驗(yàn)證。并且基于實(shí)例對(duì)u m l 模型轉(zhuǎn)換為x m i 格式，使用d o ma p i 實(shí)現(xiàn) 了u m l 模型向p e t r i 網(wǎng)標(biāo)識(shí)語(yǔ)言p n m l 的自動(dòng)轉(zhuǎn)換。將模型檢測(cè)技術(shù)應(yīng)用于安全 協(xié)議運(yùn)行模型的漏洞和缺陷分析，從而突破了安全協(xié)議的形式化檢測(cè)的傳統(tǒng)方 法：f s m 建模、p e t r i 網(wǎng)建模、t l 推理、通信進(jìn)程演算、e s t e l l e 描述、l o t o s 描述、s d l 描述，以及b a n 邏輯和k a i l a r 邏輯驗(yàn)證。 1 3 創(chuàng)新點(diǎn)和主要工作 本文在研究時(shí)序邏輯語(yǔ)言以及模型檢測(cè)這種形式化方法的基礎(chǔ)之上，創(chuàng)新點(diǎn) 主要有以下兩個(gè)方面： ( 1 ) 提出了基于部分u m l 行為模型的元素轉(zhuǎn)換為擴(kuò)展層次自動(dòng)機(jī)模型的 方法，然后使用模型檢測(cè)技術(shù)對(duì)該擴(kuò)展層次自動(dòng)機(jī)模型進(jìn)行驗(yàn)證。 ( 2 )提出了u m l 行為模型元素的擴(kuò)展層次自動(dòng)機(jī)模型到p r o m e l a 模型的描 青島人學(xué)碩上學(xué)位論文 述框架。 在本課題的研究過(guò)程中，首先主要研究了模型檢測(cè)工具s p i n ，s p i n 的輸入 語(yǔ)言p r o m e l a ，以及基于s p i n 的模型檢測(cè)過(guò)程。再次，對(duì)軟件漏洞和基于u m l 模型的模型檢測(cè)建模技術(shù)進(jìn)行了研究。最后，分析并實(shí)現(xiàn)了基于u m l 行為模型的 模型檢測(cè)實(shí)例。 本文主要的研究?jī)?nèi)容包括以下幾個(gè)方面，如圖0 1 所示。 圖1 1 研究?jī)?nèi)容示意圖 ( 1 ) 對(duì)u m l 狀態(tài)圖模型到e l l a 模型的轉(zhuǎn)換規(guī)則進(jìn)行了形式化定義，并且基 于該定義，對(duì)a t m 工作流程狀態(tài)圖模型到e h a 模型的轉(zhuǎn)換進(jìn)行了實(shí)現(xiàn)。 ( 2 ) 形式化定義了u m i 。行為模型的部分模型元素到e h a 模型的轉(zhuǎn)換艦則。 ( 3 ) 提出了u l d l 行為模型的部分模型元素對(duì)應(yīng)的e h a 模型到p r o m e l a 模型 的轉(zhuǎn)換框架。 ( 4 ) 對(duì)軟件漏洞中的資源競(jìng)爭(zhēng)性問(wèn)題和堆溢出問(wèn)題進(jìn)行了分析，使用l t l 公式對(duì)其進(jìn)行了定義。 ( 5 ) 在掌握模型檢測(cè)工具的基礎(chǔ)之上，對(duì)s e t 購(gòu)買過(guò)程協(xié)議進(jìn)行了s p i n 模 型檢測(cè)，將這種理論的應(yīng)用進(jìn)行了擴(kuò)展。 ( 6 ) 實(shí)現(xiàn)了哲學(xué)家問(wèn)題的u m l 活動(dòng)圖模型的s p i n 模型檢測(cè)。 1 4 章節(jié)安排 論文正文共分為五章。 4 第一章引言 第一章是軟件漏洞及其檢測(cè)理論的研究。本章主要介紹了軟件漏洞的分類， 并且對(duì)兩類典型的軟件漏洞進(jìn)行了分析。同時(shí)，對(duì)軟件檢測(cè)方法進(jìn)行了概括性介 紹，提出了本課題使用的軟件漏洞檢測(cè)方法一基于u m l 的模型檢測(cè)技術(shù)。 第二章是模型檢測(cè)。介紹了模型檢測(cè)的理論研究現(xiàn)狀及國(guó)內(nèi)外成果。對(duì)模型 檢測(cè)的基本原理、建模方法和搜索算法進(jìn)行了介紹。模型檢測(cè)在應(yīng)用過(guò)程中，很 多學(xué)者經(jīng)過(guò)研究，開(kāi)發(fā)了多種模型檢測(cè)工具，本章對(duì)其中的幾種工具進(jìn)行了介紹。 其中詳細(xì)地介紹了課題在研究過(guò)程中使用的模型檢測(cè)工具s p i n 。以及詳細(xì)地描 述了使用該工具對(duì)具體的一個(gè)安全協(xié)議模型進(jìn)行部分p r o m e l a 代碼實(shí)現(xiàn)。在本章 中還介紹了模型檢測(cè)的基礎(chǔ)時(shí)序邏輯。對(duì)線性時(shí)序邏輯( l t l ) 的語(yǔ)義與語(yǔ) 法規(guī)范進(jìn)行了詳述。 第三章是基于e l l a 的u m l 行為模型建模研究。本章主要介紹了介紹了u m l 以 及如何將u m l 各種建模機(jī)制，提出了使用轉(zhuǎn)換規(guī)則建立自動(dòng)機(jī)模型是模型檢測(cè)的 第一步，因此成為本章研究的重點(diǎn)問(wèn)題。擴(kuò)展層次自動(dòng)機(jī)( e h a ) 是廣泛使用的 一種建模工具。本章提出了u m l 行為模型的部分元素使用e h a 抽象建模的規(guī)則， 以及對(duì)u m l 的元素e h a 模型使用p r o m e l a 描述的語(yǔ)法框架。同時(shí)，基于實(shí)例，對(duì) u m l 狀態(tài)圖轉(zhuǎn)換為e h a 模型的基本過(guò)程，為模型檢測(cè)的下一步工作奠定了基礎(chǔ)。 第四章是基于u m l 行為模型的s p i n 檢測(cè)過(guò)程的實(shí)驗(yàn)過(guò)程描述。本章對(duì)哲學(xué) 家就餐問(wèn)題進(jìn)行了詳細(xì)地分析，對(duì)該問(wèn)題的u m l 活動(dòng)圖轉(zhuǎn)換為e h a 模型，同時(shí)根 據(jù)p r o m e l a 轉(zhuǎn)換框架，實(shí)現(xiàn)了對(duì)模型的描述。同時(shí)對(duì)部分系統(tǒng)屬性進(jìn)行了l t l 描 述，實(shí)現(xiàn)了對(duì)該問(wèn)題的s p i n 驗(yàn)證，并且對(duì)該驗(yàn)證結(jié)果進(jìn)行了描述。 第五章是總結(jié)與展望。 青島大學(xué)碩l 學(xué)位論文 6 第二章軟件漏洞及其檢測(cè)理論 第二章軟件漏洞及其檢測(cè)理論 隨著計(jì)算機(jī)的產(chǎn)生和廣泛應(yīng)用，人們對(duì)計(jì)算機(jī)安全領(lǐng)域的研究也隨之進(jìn)行并 不斷地成熟。追溯到上世紀(jì)7 0 年代中期，美國(guó)南加州大學(xué)針對(duì)操作系統(tǒng)的安全 缺陷進(jìn)行研究的p a ( p r o t e c t i o na n a l y s i sp r o j e c t ) 計(jì)劃，目的就是增強(qiáng)計(jì)算 機(jī)操作系統(tǒng)的安全性。后來(lái)又有很多學(xué)者參與這一領(lǐng)域的研究并不斷創(chuàng)新研究成 果，他們的研究分別是：r i s o s 計(jì)劃、s d c 的滲透分析方法、l a n d w h e r 的漏洞分 類、b r i a nm a r i c k 的軟件漏洞分析以及普渡大學(xué)c o a s t 實(shí)驗(yàn)室的計(jì)算機(jī)漏洞研 究。但是，對(duì)計(jì)算機(jī)安全漏洞的定義、分類、特征到目前為止還未形成統(tǒng)一和公 認(rèn)的結(jié)論。 2 1 軟件漏洞 2 0 0 9 年5 月1 9 日晚，受暴風(fēng)影音軟件存在的設(shè)計(jì)缺陷以及免費(fèi)智能d n s 軟 件d n s p o d 的不健壯性影響，黑客通過(guò)僵尸網(wǎng)絡(luò)控制下的d d o s 攻擊，致使我國(guó)江 蘇、安徽、廣西、海南、甘肅、浙江等省在內(nèi)的2 3 個(gè)省出現(xiàn)罕見(jiàn)的斷網(wǎng)故障， 即“5 1 9 斷網(wǎng)事件 。這次事件中，免費(fèi)軟件的后門是問(wèn)題產(chǎn)生的誘因，d n s 服 務(wù)的脆弱性是問(wèn)題產(chǎn)生的關(guān)鍵。雖然此次事件已經(jīng)平息，但是人們不得不對(duì)軟件 及服務(wù)的高可靠性要求再次提高了要求。類似該事件的大量安全性攻擊行為充分 利用了操作系統(tǒng)和應(yīng)用軟件存在的漏洞，人們對(duì)操作系統(tǒng)的漏洞和d n s 應(yīng)用軟件 的漏洞管理產(chǎn)生了質(zhì)疑n 別。 2 1 1 軟件漏洞概述 軟件漏洞研究是分析和研究軟件脆弱性的基礎(chǔ)。對(duì)產(chǎn)生軟件脆弱性的各種軟 件漏洞進(jìn)行研究，可以加深我們對(duì)軟件脆弱性的理解，同時(shí)基于軟件脆弱性的基 本理論，幫助人們更好的解決隱藏的安全隱患，設(shè)計(jì)和實(shí)現(xiàn)高可靠性的復(fù)雜軟件 系統(tǒng)。 要理解軟件脆弱性，就要明確脆弱性的相關(guān)術(shù)語(yǔ)。 錯(cuò)誤：錯(cuò)誤是指開(kāi)發(fā)人員在工作過(guò)程中的一個(gè)拼寫錯(cuò)誤，對(duì)需求說(shuō)明的誤讀， 對(duì)子程序的錯(cuò)誤理解等等n 3 1 。 故障：故障是指不正確的程序和正確的版本之間的差異n 制。 安全缺陷：軟件安全缺陷是指有意或是無(wú)意地引入系統(tǒng)中的，可能導(dǎo)致違背 系統(tǒng)安全需求的不正確行為的程序或數(shù)據(jù)n 耵。 漏洞( 脆弱性) ：軟件脆弱性是指由軟件缺陷的客觀存在所形成的一個(gè)可以 被攻擊者利用的實(shí)例6 。 基于刈+ 信息安全與隱私的分析和研究，r i s o s 項(xiàng)目 的研究人員提出了基于 青島人學(xué)碩士學(xué)位論文 操作系統(tǒng)的完整性缺陷的軟件脆弱性分類方法。 軟件脆弱性 l 二01 搡輯：戲操住數(shù)選 不m 確豹保護(hù)4 q f 確的駿涯不正確的陽(yáng)步 猙 摶潑 j r毒i ri ，、。 i 扔蝓稼護(hù)域 沒(méi)f i j e 確黼 i l 存消，j 絨 l 選抒錨淡 璃虹現(xiàn)環(huán)柱 變換鑄誒禽筆鐨誤 壤分魁鋤援 繇f 牲錯(cuò)誤顙膨鎊溪 l 圖2 1 軟件漏洞分類 p a 項(xiàng)目u 踟對(duì)g c o s 、m u l t i c s 、u n i x 等六個(gè)操作系統(tǒng)的1 0 0 多個(gè)缺陷進(jìn)行了 分析，最終將這些缺陷分為4 類( 圖2 1 ) 。美國(guó)海軍研究實(shí)驗(yàn)室的l a n d w e h r 等 人提出了基于缺陷的起因、引入的時(shí)間( 開(kāi)發(fā)階段、維護(hù)階段或運(yùn)行階段) 、分 布的位置( 軟件或硬件) 進(jìn)行了分類n 們。1 9 9 5 年，c o a s t 實(shí)驗(yàn)室的a s l a m 針對(duì) u n i x 操作系統(tǒng)，將引起軟件脆弱性的故障分為編碼故障和突發(fā)故障兩大類。對(duì) 軟件脆弱性的分類，還有很多方法，例如：b i s h o p 分類法、i b m 的軟件缺陷分類 法和t s i p e n y u k “7 + 1 分類法等等啪1 。 2 1 2 典型的軟件漏洞 ( 1 ) 競(jìng)爭(zhēng)條件漏洞。 競(jìng)爭(zhēng)狀態(tài)是一種異常行為，是由對(duì)事件相對(duì)節(jié)奏的依賴關(guān)系的破壞而引發(fā) 的。競(jìng)爭(zhēng)條件屬于t o c f o u ( t i m e - o f - c h e c k - t o - t i m e - o f - u s e ) 漏洞的一種，即 程序先檢查對(duì)象的某個(gè)特性，然后得動(dòng)作是在假設(shè)這些特性一直保持的情況下做 出的，但這時(shí)該特性可能不具備了。在有些研究中，該問(wèn)題稱為定時(shí)或同步漏洞。 競(jìng)爭(zhēng)條件漏洞是軟件設(shè)計(jì)過(guò)程中經(jīng)常遇到的問(wèn)題。通常可以分為兩類：在運(yùn) 行某一個(gè)程序過(guò)程中，由于程序進(jìn)程的非原子性，從而存在了非誠(chéng)實(shí)進(jìn)程插入運(yùn) 行，從而導(dǎo)致了非誠(chéng)實(shí)主體的非法行為的執(zhí)行。很多安全分類學(xué)稱這個(gè)問(wèn)題為“順 序 或“原子性問(wèn)題；很多進(jìn)程對(duì)同一共享資源擁有相同的優(yōu)先權(quán)，當(dāng)多個(gè)進(jìn) 程同時(shí)運(yùn)行相同的程序并且使用該共享資源時(shí)，就會(huì)造成誠(chéng)實(shí)進(jìn)程之間的沖突。 很多分類學(xué)叫這類問(wèn)題為“死鎖 、“活鎖”或“鎖失敗條件 。 一般來(lái)說(shuō)，進(jìn)程不是以原子方式運(yùn)行的，一個(gè)進(jìn)程p 1 的中斷可以在另一個(gè) 進(jìn)程p 2 正在執(zhí)行兩條指令之間進(jìn)行。如果進(jìn)程p 2 對(duì)進(jìn)程p 1 的中斷行為沒(méi)有適 當(dāng)?shù)奶幚泶胧?，那么程序的?zhí)行就會(huì)產(chǎn)生安全問(wèn)題。 競(jìng)爭(zhēng)條件漏洞的發(fā)生要具備兩個(gè)條件乜。第一，有兩個(gè)或更多的事件發(fā)生， 并且這些事件的發(fā)生存在一定的時(shí)間間隔。兩個(gè)事件問(wèn)有一定的關(guān)系，即：其它 第二章軟件漏洞及其檢測(cè)理論 的事件的執(zhí)行依賴于其中的一個(gè)或幾個(gè)事件。第二，攻擊者能夠改變這些事件執(zhí) 行所依賴的假設(shè)，也就是所依賴事件產(chǎn)生的結(jié)果。 ( 2 ) 堆溢出 由于c 語(yǔ)言不檢查邊界溢出問(wèn)題，使得很多程序存在設(shè)計(jì)漏洞。其中最典型 的是內(nèi)存溢出問(wèn)題。內(nèi)存區(qū)分為存放動(dòng)態(tài)數(shù)據(jù)的堆區(qū)、靜念數(shù)據(jù)的堆區(qū)和存放程 序調(diào)用的棧區(qū)。將堆區(qū)溢出問(wèn)題抽象為對(duì)兩個(gè)動(dòng)態(tài)數(shù)組變量進(jìn)行操作時(shí)造成的數(shù) 組長(zhǎng)度越界問(wèn)題。 2 2 軟件漏洞的檢測(cè)方法 正是由于軟件的漏洞會(huì)給人們帶來(lái)不可挽回的損失和后果，對(duì)于軟件生產(chǎn)商 和用戶來(lái)說(shuō)，都非常注重對(duì)軟件漏洞的檢測(cè)，這就使得軟件漏洞檢測(cè)方法有了長(zhǎng) 足的發(fā)展。軟件漏洞的檢測(cè)方法有很多，主流有基于數(shù)據(jù)流和控制流的分析方法； 有基于白盒測(cè)試和自動(dòng)化工具的代碼檢測(cè)堙刳；而對(duì)于商業(yè)軟件來(lái)說(shuō)，主要采取黑 盒測(cè)試的方法。 從檢測(cè)過(guò)程角度來(lái)看，可以分為靜態(tài)檢測(cè)和動(dòng)態(tài)檢測(cè)，兩者的區(qū)別主要在于 是否執(zhí)行待測(cè)試的軟件。靜態(tài)分析主要采用自動(dòng)化的檢測(cè)工具對(duì)源代碼進(jìn)行檢 測(cè)，使用一個(gè)“鉤子函數(shù)”調(diào)用用戶自定義的屬性函數(shù)，并通過(guò)分析函數(shù)來(lái)判斷 該屬性函數(shù)是否滿足特定的約束條件。這種方法的具有速度快，不需要實(shí)際運(yùn)行 軟件的優(yōu)點(diǎn)。但同時(shí)，由于“鉤子函數(shù)”的算法和效率直接影響到靜態(tài)測(cè)試的準(zhǔn) 確性，所以，往往也會(huì)帶來(lái)諸如不能發(fā)現(xiàn)漏洞的完整性、誤判以及對(duì)漏洞描述不 足等缺點(diǎn)。而對(duì)于動(dòng)態(tài)檢測(cè)方法，基本上都是通過(guò)在代碼中注入標(biāo)記，并在實(shí)際 運(yùn)行軟件時(shí)記錄這些標(biāo)記，從而發(fā)現(xiàn)軟件是否按照原定的路徑執(zhí)行。這種方法的 檢測(cè)準(zhǔn)確率非常高，但是大部分時(shí)間會(huì)用在處理這些標(biāo)記信息上，因此效率不高。 目前利用自動(dòng)化方法檢測(cè)軟件漏洞主要有兩類方法，類是基于黑盒測(cè)試原 理，另一類是使用編譯技術(shù)，對(duì)軟件的源代碼進(jìn)行掃描測(cè)試。 第一類方法主要是針對(duì)軟件接口而不是針對(duì)軟件的實(shí)現(xiàn)進(jìn)行的測(cè)試。在測(cè)試 過(guò)程中，測(cè)試者要給出大量的測(cè)試片j 例。如果針對(duì)某一類測(cè)試用例，該軟件出現(xiàn) 異常情況，例如軟件崩潰或者軟件：異常。就可以說(shuō)明，該軟件針對(duì)某類測(cè)試用例 可以觸發(fā)軟件漏洞。 第二類方法主要是對(duì)軟件的源代碼進(jìn)行掃描并且塒軟件函數(shù)的使用進(jìn)行檢 查。因此該類方法只能對(duì)丌源軟件進(jìn)行檢測(cè)，對(duì)非開(kāi)源的軟件就沒(méi)有辦法了。 模型檢測(cè)技術(shù)在硬件應(yīng)用領(lǐng)域的應(yīng)用已經(jīng)相當(dāng)成熟，然而在軟件領(lǐng)域該技術(shù) 正處在研究階段心3 兒2 4 1 。 9 青島大學(xué)碩十學(xué)位論文 二一j 圖2 2 針對(duì)源碼的模型檢測(cè) 模型檢測(cè)技術(shù)同樣可以應(yīng)用到對(duì)源代碼進(jìn)行檢測(cè)過(guò)程中。如圖2 2 所示，對(duì) 軟件產(chǎn)品的源碼進(jìn)行檢測(cè)時(shí)，首先要通過(guò)模型生成器將源碼轉(zhuǎn)換為有窮自動(dòng)機(jī)， 同時(shí)將要檢測(cè)的安全屬性描述并轉(zhuǎn)換為下推自動(dòng)機(jī)。其次，將這兩個(gè)自動(dòng)機(jī)模型 帶入模型檢測(cè)器中進(jìn)行檢測(cè)，模型檢測(cè)器會(huì)將檢測(cè)結(jié)果自動(dòng)輸出。 人們不能已知所有的軟件漏洞，然而可以利用現(xiàn)有的安全屬性庫(kù)中的安全屬 性模型對(duì)軟件產(chǎn)品進(jìn)行檢測(cè)。其中，對(duì)l i n u x 操作系統(tǒng)的開(kāi)源源碼進(jìn)行模型檢測(cè) 是現(xiàn)在學(xué)者研究的重點(diǎn)內(nèi)容。一些針對(duì)l i n u x 操作系統(tǒng)的安全屬性包括比印諸如系 統(tǒng)的訪問(wèn)控制；對(duì)文件進(jìn)行寫入操作時(shí)，調(diào)用f o p e n 函數(shù)打開(kāi)或新建一個(gè)文件后， 必須先上鎖才能進(jìn)行下一步的操作等等。 部分研究人員正在研究模型檢測(cè)技術(shù)應(yīng)用于軟件漏洞自動(dòng)挖掘。模型檢測(cè)技 術(shù)的漏洞挖掘方法具有很多優(yōu)點(diǎn)：不必運(yùn)行被測(cè)系統(tǒng)，速度很快；能做到完全自 動(dòng)化；無(wú)需用戶輸入；能夠保證漏洞發(fā)現(xiàn)的完全性。一般情況下，應(yīng)用于軟件的 模型檢測(cè)技術(shù)可以分為對(duì)軟件開(kāi)發(fā)初期的設(shè)計(jì)模型進(jìn)行的模型檢測(cè)和針對(duì)源代 碼的模型檢測(cè)。 目前，針對(duì)源代碼的模型檢測(cè)工具原型主要是m o p s 啪1 。該工具主要由加州 大學(xué)伯克利分校博士研究生h a oc h e n 完成，適用對(duì)象是采用c 語(yǔ)言編寫的程序 源代碼，它基于控制流分析，實(shí)現(xiàn)了對(duì)百萬(wàn)行c 代碼的分析，其中包括了對(duì)完整 版本的l i n u x 9 的代碼分析，找到了多個(gè)以前未知的安全漏洞。 、 針對(duì)軟件開(kāi)發(fā)初期的模型檢測(cè)技術(shù)主要是基于u m l 模型的檢測(cè)。很多學(xué)者將 u m i 模型轉(zhuǎn)化為p e t r i 網(wǎng)模型，再利用p e t r i 網(wǎng)的分析驗(yàn)證技術(shù)，實(shí)現(xiàn)對(duì)軟件模 型的正確性驗(yàn)證。還有學(xué)者的研究過(guò)程是將u m l 模型的x m i 格式進(jìn)行解析，然后 使用d o ma p i 實(shí)現(xiàn)了u m l 模型向p e t r i 網(wǎng)標(biāo)識(shí)語(yǔ)言p n m l 的自動(dòng)轉(zhuǎn)換。 本課題在經(jīng)過(guò)分析研究之后，選擇了將u m l 模型轉(zhuǎn)換為自動(dòng)機(jī)模型，然后使 用s p i n 工具對(duì)該自動(dòng)機(jī)模型進(jìn)行建模、規(guī)約和驗(yàn)證。從而實(shí)現(xiàn)了對(duì)軟件模型的 正確性驗(yàn)證。 l o 第三章模型榆測(cè)理論及s p i n 第三章模型檢測(cè)理論及s p i n 3 1 模型檢測(cè)概述 模型檢測(cè)是形式化驗(yàn)證方法之一。近幾十年中，模型檢測(cè)理論得到了不斷地 完善和發(fā)展，同時(shí)基于該理論的模型檢測(cè)技術(shù)也越來(lái)越多的在實(shí)際應(yīng)用中取得巨 大的成果。許多世界著名大公司如a t & t 、f u j i t s u 、i n t e l 、i b m 、m i c r o s o f t 、 l u c e n t 、m o t o r o l a 、s i e m e n s 等紛紛在其產(chǎn)品設(shè)計(jì)和開(kāi)發(fā)過(guò)程中使用模型檢測(cè)技 術(shù)，并在許多復(fù)雜的實(shí)例研究中發(fā)揮了重要的作用。 模型檢測(cè)是對(duì)實(shí)際系統(tǒng)抽象為有限狀態(tài)模型后，對(duì)其進(jìn)行窮盡搜索，判斷該 有窮狀態(tài)模型是否滿足待測(cè)屬性，如果不滿足則給出反例。當(dāng)系統(tǒng)的有限狀態(tài)模 型確定后，逐個(gè)或組合使用屬性集中的約束條件，驗(yàn)證系統(tǒng)描述的行為是否能夠 達(dá)到所預(yù)想的狀態(tài)。 區(qū)醒叵墮 # 一i j 、m 是否滿足v 一，7 7 l 二二一j v 否 l + ，j 圖3 1 模型檢測(cè)的基本原理 模型檢測(cè)過(guò)程也就是建模、規(guī)約和驗(yàn)證的過(guò)程。如圖3 1 所示。 建模：其中有限狀態(tài)模型m 使用自動(dòng)機(jī)( 包括擴(kuò)展自動(dòng)機(jī)e f a 、b u c h i 自動(dòng) 機(jī)、t 1 m e d 自動(dòng)機(jī)) 、p e t r i 網(wǎng)( 包括位置遷移p e t r i 嘲和高級(jí)p e t r i 網(wǎng)) 或者 s t a t e c h a r t s 等工具進(jìn)行描述。屬性集的公式使用時(shí)序邏輯語(yǔ)言描述，根據(jù)當(dāng) 前時(shí)刻的可能未來(lái)時(shí)刻是否足線性的，可分為線性時(shí)態(tài)邏輯i ，t i 。和計(jì)算樹時(shí)態(tài)邏 輯c t l 。 規(guī)約：一個(gè)時(shí)念邏輯公式可以轉(zhuǎn)換為一個(gè)等價(jià)的自動(dòng)機(jī)，v a r d i 和w o l p e r 于1 9 8 6 年實(shí)現(xiàn)了將時(shí)態(tài)邏輯檢測(cè)轉(zhuǎn)變?yōu)樽詣?dòng)機(jī)模型檢測(cè)，從而把這兩種方法關(guān) 聯(lián)起來(lái)。自動(dòng)機(jī)模型檢測(cè)分別將系統(tǒng)和屬性表示成自動(dòng)機(jī)，然后去檢測(cè)系統(tǒng)自動(dòng) 機(jī)所接受的語(yǔ)言足否包含丁屬性白動(dòng)機(jī)接受的語(yǔ)言。時(shí)態(tài)邏輯模型檢測(cè)則足將系 青島大學(xué)碩士學(xué)位論文 統(tǒng)抽象為位置遷移系統(tǒng)s ，表示系統(tǒng)的行為，鼠是初始狀態(tài)集( rcs ) ，用模 態(tài)時(shí)序邏輯公式f 刻畫系統(tǒng)的性質(zhì)，通過(guò)計(jì)算找到s 中所有滿足，的狀態(tài)組成 的集合s ，若r s ，則通過(guò)驗(yàn)證。 對(duì)于公式妙，它所包含的約束屬性可分為以下幾種：可達(dá)性( r e a c h a b i l i t y ) 、 安全性( s a f e t y ) 、活性( 1 i v e n e s s ) 、公平性( f a i r n e s s ) ，它們從不同的側(cè)面 去檢測(cè)模型的行為，從而比較全面地實(shí)現(xiàn)檢測(cè)的目的。 驗(yàn)證：驗(yàn)證過(guò)程是驗(yàn)證建模過(guò)程中得到的有窮狀態(tài)模型是否滿足規(guī)約階段得 到的屬性公式。該驗(yàn)證過(guò)程可以使用驗(yàn)證算法進(jìn)行窮盡搜索，也可以使用模型檢 測(cè)工具進(jìn)行自動(dòng)化驗(yàn)證。在模型檢測(cè)的驗(yàn)證算法中，較為成熟的是針對(duì)c t l 的標(biāo) 記算法，這個(gè)基礎(chǔ)算法在模型驗(yàn)證和模型檢測(cè)領(lǐng)域得到了廣泛的應(yīng)用，尤其是在 計(jì)算機(jī)硬件系統(tǒng)模型的驗(yàn)證和檢測(cè)方面。另一種基本的模型檢測(cè)算法是 f i x p o i n t 算法乜引。很多學(xué)者，結(jié)合模型檢測(cè)算法，實(shí)現(xiàn)了對(duì)多個(gè)問(wèn)題領(lǐng)域的自 動(dòng)模型檢測(cè)，并且研發(fā)了多種模型檢測(cè)工具。 模型檢測(cè)在建筑、工程、計(jì)算機(jī)硬件等領(lǐng)域應(yīng)用了很多年，但在軟件領(lǐng)域的 應(yīng)用卻是近幾年才有了突破，原因是存在狀態(tài)空間爆炸問(wèn)題，這個(gè)問(wèn)題成為制約 模型檢測(cè)的瓶頸，也是研究模型檢測(cè)的前沿問(wèn)題。近幾年來(lái)，針對(duì)狀態(tài)空間爆炸 問(wèn)題的研究，有了突破性進(jìn)展，主要的解決方法有：二叉決策圖( b d d ) 和符號(hào) 模型檢測(cè)( s m c ) 、o n - t h e - f l y 技術(shù)、抽象技術(shù)、偏序規(guī)約、組合推理和對(duì)稱檢 測(cè)等。論文只介紹其中幾種重要的技術(shù)。 二叉決策圖( b d d ) 是一種有根無(wú)環(huán)圖，它由b r y a n t 首先提出，用來(lái)存儲(chǔ)布 爾表達(dá)式，該技術(shù)極大地減少了存儲(chǔ)布爾公式所需要的空間，使模型檢測(cè)工業(yè)應(yīng) 用成為可能。它主要用于描述節(jié)點(diǎn)的偏序關(guān)系，并在此基礎(chǔ)之上，使用對(duì)圖的基 本操作來(lái)實(shí)現(xiàn)對(duì)布爾函數(shù)的操作。 符號(hào)模型檢測(cè)( s m c ) 由m c m i l l a n 提出，其主要思想是狀態(tài)集相關(guān)的屬性表 示成集合，也就是狀態(tài)的合并，使用布爾表達(dá)式刻畫這些屬性，再用b d d 在計(jì)算 機(jī)內(nèi)實(shí)現(xiàn)這些布爾公式及其運(yùn)算，該方法可以把驗(yàn)證規(guī)模提高到若干數(shù)量級(jí)，有 些情況設(shè)置可以達(dá)到l o “”，并丌發(fā)出工具s m v 。 o n - t h e - f l y 技術(shù)是在需要某些狀態(tài)時(shí)，才將其路徑展丌，從而避免了狀態(tài) 的預(yù)先生成。該方法很適合深度優(yōu)先遍歷搜索狀態(tài)空l(shuí) 日j 的模型檢測(cè)算法。 抽象技術(shù)是除符號(hào)模型外，解決空問(wèn)狀念爆炸問(wèn)題最有效的方法。抽象技術(shù) 是狀態(tài)合并，為了壓縮狀態(tài)空間，它通過(guò)消除一些不影響規(guī)范的變量狀態(tài)，得到 簡(jiǎn)化的自動(dòng)機(jī)模型，通過(guò)驗(yàn)證簡(jiǎn)化模型的性質(zhì)來(lái)降低模型檢測(cè)的復(fù)雜性。文獻(xiàn)瞳町 對(duì)抽象技術(shù)進(jìn)行了深入的研究，提出了多種抽象方法：數(shù)據(jù)抽象、基于抽象解釋 的抽象、謂詞抽象、基于反例的抽象求精。d 時(shí)將這些方法與t l e n z i n g e r 提出的 懶惰抽象技術(shù)做了比較。 1 2 第三章模型柃測(cè)理論及s p i n 對(duì)稱檢測(cè)技術(shù)最早應(yīng)用在高級(jí)p e t r i 網(wǎng)，主要是用在有色p e t r i 網(wǎng)中。它和 標(biāo)記算法相同都是用來(lái)創(chuàng)建有限狀態(tài)的可達(dá)樹。這種思想被擴(kuò)展應(yīng)用在了位置 遷移系統(tǒng)中，用于對(duì)模型進(jìn)行死鎖偵測(cè)和活性的檢測(cè)。文獻(xiàn)啪，中提出該技術(shù)采用 了離散數(shù)學(xué)的群論知識(shí)，在自同構(gòu)的群中，通過(guò)求解商集獲得o u o t i e n tk r i p l e 結(jié)構(gòu)，并且可以結(jié)合o n - t h e - f l y 等多種關(guān)鍵技術(shù)相結(jié)合，同時(shí)文中提出了怎樣 在弱對(duì)稱系統(tǒng)中使用了對(duì)稱技術(shù)。該技術(shù)成為研究狀態(tài)爆炸問(wèn)題的有效方法。 3 2 模型檢測(cè)工具 模型檢測(cè)理論的不斷成熟，依賴于國(guó)內(nèi)外學(xué)者的深入研究。同時(shí)，模型檢測(cè) 工具使得該理論與實(shí)際相結(jié)合，在不斷解決實(shí)際應(yīng)用問(wèn)題中完善和解決該理論中 存在的問(wèn)題。模型檢測(cè)工具主要有以下幾種： ( 1 ) 符號(hào)化模型檢測(cè)工具s m v ，可以解決狀態(tài)空間爆炸問(wèn)題。s m v 的輸入時(shí) k r i p k e 結(jié)構(gòu)，并且使用c t l 語(yǔ)言對(duì)系統(tǒng)屬性進(jìn)行定義。它成功地發(fā)現(xiàn)了i e e e f u t u r e b u s + s t a n d a r d ( i e e e 標(biāo)準(zhǔn)8 9 6 卜1 9 9 1 ) 中描述的c a c h e 一致性協(xié)議中的 錯(cuò)誤，這也是使用自動(dòng)驗(yàn)證工具首次發(fā)現(xiàn)i e e e 標(biāo)準(zhǔn)的錯(cuò)誤。國(guó)際上符號(hào)化模型 檢測(cè)工具還有c o n c u r r e n t f a c t o r y ，x m l ，c w b 等。 ( 2 ) s l a m 是微軟開(kāi)發(fā)的基于c 語(yǔ)言的模型檢測(cè)工具包，已經(jīng)成功應(yīng)用于驗(yàn) 證w i n d o w s x p 中的一些驅(qū)動(dòng)程序的接口的正確性。 ( 3 ) j a v a p a t h f i n d e r ( j p f ) 是美國(guó)國(guó)家航空航天局開(kāi)發(fā)的針對(duì)j a v a 語(yǔ)言的 驗(yàn)證工具。j p f 已經(jīng)應(yīng)用于多個(gè)實(shí)際系統(tǒng)，取得了很好的效果。 ( 4 ) 還有幾種基于抽象技術(shù)解決狀態(tài)爆炸問(wèn)題的模型檢測(cè)工具。b l a s t 是 加州大學(xué)伯克萊分校丌發(fā)的針對(duì)c 程序的軟件模型檢測(cè)工具。m a g i c 是卡內(nèi)基梅 隆大學(xué)開(kāi)發(fā)的針