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