（計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)論文）面向c程序驗(yàn)證的切片執(zhí)行方法.pdf

國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 摘要 隨著計(jì)算機(jī)系統(tǒng)的廣泛應(yīng)用，計(jì)算機(jī)軟件的高可信性質(zhì)受到了越來(lái)越多的關(guān) 注。面向軟件源程序的形式驗(yàn)證是保障軟件高可信性質(zhì)的一種有效方法，受到了 大量的關(guān)注和廣泛的研究。但是，由于軟件程序邏輯復(fù)雜、規(guī)模龐大，如何提高 軟件源程序驗(yàn)證的精度特別是可擴(kuò)展性仍是當(dāng)前研究所面臨的主要問(wèn)題。 本文提出了一種面向c 程序的時(shí)序安全性質(zhì)驗(yàn)證方法，即切片執(zhí)行方法。它 本質(zhì)上是一種輕量級(jí)的符號(hào)執(zhí)行，能夠自動(dòng)抽象出順序和并發(fā)c 程序的有限狀態(tài) 模型，并基于模型檢驗(yàn)方法進(jìn)行驗(yàn)證。切片執(zhí)行融合了程序切片，程序語(yǔ)義抽象、 符號(hào)化狀態(tài)表示、反例制導(dǎo)的抽象精化、偏序縮減等多種有效的狀態(tài)空間縮減技 術(shù)，大大縮減了抽象模型的狀態(tài)空間，從而提高了軟件源程序形式驗(yàn)證的可擴(kuò)展 性。切片執(zhí)行的主要特點(diǎn)是面向時(shí)序安全性質(zhì)的驗(yàn)證，能夠以接近標(biāo)準(zhǔn)流敏感數(shù) 據(jù)流分析的代價(jià)，達(dá)到路徑敏感程序模擬的驗(yàn)證精度；同時(shí)切片執(zhí)行支持包括循 環(huán)在內(nèi)的程序結(jié)構(gòu)，支持全自動(dòng)的模型抽象和性質(zhì)驗(yàn)證。 切片執(zhí)行構(gòu)建在基于變量抽象的程序保守近似語(yǔ)義的基礎(chǔ)上，它符號(hào)化地執(zhí) 行變量抽象下的相關(guān)語(yǔ)句計(jì)算用于描述程序保守近似語(yǔ)義的部分最強(qiáng)后置條件 和部分最弱前置條件，抽象出c 程序的有限狀態(tài)模型，并基于模型檢驗(yàn)方法驗(yàn)證 抽象模型是否滿足給定的時(shí)序安全性質(zhì)?；诒疚奶岢龅乃阉鲝?fù)用框架，切片執(zhí) 行不斷根據(jù)產(chǎn)生的偽反例路徑精化變量抽象的抽象準(zhǔn)則，直到性質(zhì)被驗(yàn)證或找到 真實(shí)反例路徑面向并發(fā)c 程序驗(yàn)證，切片執(zhí)行集成了本文提出的有狀態(tài)動(dòng)態(tài)偏 序縮減方法，大大縮減搜索的狀態(tài)空間切片執(zhí)行還集成了一種輕量級(jí)判定過(guò)程， 用于對(duì)c 程序驗(yàn)證過(guò)程中的驗(yàn)證公式進(jìn)行高效判定具體地，本文的創(chuàng)新點(diǎn)包括 如下五個(gè)方面： l 、提出了切片執(zhí)行的基本概念和方法基于對(duì)程序驗(yàn)證基本規(guī)律的分析，我 們提出了變量抽象方法，只考慮程序中與待驗(yàn)證性質(zhì)相關(guān)的變量和語(yǔ)句基于變 量抽象，我們定義了部分最強(qiáng)后置條件，進(jìn)而定義了程序的保守近似語(yǔ)義?；?這兩個(gè)概念，我們提出了切片執(zhí)行的概念，它是一種輕量級(jí)的符號(hào)執(zhí)行過(guò)程 2 、提出了面向時(shí)序安全性質(zhì)驗(yàn)證的搜索復(fù)用框架并將其應(yīng)用于切片執(zhí)行。搜 索復(fù)用框架也是一種反例路徑制導(dǎo)的抽象精化( c e g a r ) 框架，基于偽反例路徑 進(jìn)行模型精化。相比傳統(tǒng)的c e g a r 框架，搜索復(fù)用框架的最大特點(diǎn)是能夠在不同 精度的抽象模型之間進(jìn)行充分的信息復(fù)用，從而避免了大量不必要的重復(fù)搜索， 有效降低了驗(yàn)證開(kāi)銷。 3 、提出了部分最弱前置條件的概念并將其應(yīng)用于切片執(zhí)行部分最弱前置條 第i 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 件是程序保守近似語(yǔ)義的另一種表示方法，同樣基于變量抽象定義在切片執(zhí)行 過(guò)程中，可以用部分最弱前置條件部分地取代部分最強(qiáng)后置條件，以生成更弱的 一階邏輯公式來(lái)描述抽象模型的同一個(gè)狀態(tài)，從而在不影響模型精度的前提下有 效縮減生成模型的狀態(tài)空間。 4 、提出了面向有狀態(tài)模型檢驗(yàn)的有狀態(tài)動(dòng)態(tài)偏序縮減方法，并將其集成到切 片執(zhí)行過(guò)程中。我們將切片執(zhí)行方法擴(kuò)展到了對(duì)并發(fā)c 程序的驗(yàn)證。為了進(jìn)一步 進(jìn)行狀態(tài)空問(wèn)縮減，我們提出了有狀態(tài)動(dòng)態(tài)偏序縮減方法，并將其自然地集成到 切片執(zhí)行框架中，用于指導(dǎo)切片執(zhí)行，使其避免搜索多條具有相同偏序關(guān)系的并 發(fā)進(jìn)線程交迭執(zhí)行路徑。我們進(jìn)行了多個(gè)實(shí)驗(yàn)，包括兩個(gè)實(shí)用并發(fā)程序片段和一 個(gè)并發(fā)s s l 程序?qū)嶒?yàn)結(jié)果表明，切片執(zhí)行和有狀態(tài)動(dòng)態(tài)偏序縮減這兩種正交的 狀態(tài)空問(wèn)縮減方法的集成，大大縮減了并發(fā)程序抽象模型的狀態(tài)空問(wèn)，特別是降 低了驗(yàn)證的空間開(kāi)銷。 5 、提出了面向切片執(zhí)行驗(yàn)證公式的輕量級(jí)判定過(guò)程。我們定義了一類整數(shù)線 性一階邏輯判定公式，此類判定公式支持c 程序中常用的整數(shù)線性運(yùn)算。我們優(yōu) 化了判定過(guò)程，并擴(kuò)充了對(duì)整數(shù)除法、取余和位運(yùn)算的支持實(shí)驗(yàn)表明，擴(kuò)充后 的判定過(guò)程能夠?qū)γ嫦騝 程序的切片執(zhí)行所產(chǎn)生的絕大多數(shù)驗(yàn)證公式進(jìn)行高效判 定。在基于s s l 程序的切片執(zhí)行實(shí)驗(yàn)中我們發(fā)現(xiàn)，采用該判定方法后，驗(yàn)證效率 比使用定理證明工具s i m p l i 匆提高了1 0 5 倍 我們還基于開(kāi)放源代碼的m a g i c 項(xiàng)目，實(shí)現(xiàn)了基于切片執(zhí)行的c 程序驗(yàn)證 工具原型，并基于o p e n s s l * 0 9 6 c 等實(shí)用程序針對(duì)上述每個(gè)創(chuàng)新點(diǎn)都進(jìn)行了實(shí)驗(yàn)。 我們?cè)趯?shí)驗(yàn)時(shí)采用了與b l a s t 和m a g i c 相同的硬件平臺(tái)，并針對(duì)相同的驗(yàn)證用 例，驗(yàn)證了相同的性質(zhì)集合。經(jīng)過(guò)充分的實(shí)驗(yàn)數(shù)據(jù)對(duì)比，我們發(fā)現(xiàn)切片執(zhí)行在驗(yàn) 證效率上具有一定的優(yōu)勢(shì)。 主題詞：切片執(zhí)行，模型檢驗(yàn)，時(shí)序安全性質(zhì)，c 程序驗(yàn)證，變量抽象，部分 最強(qiáng)后置條件，部分最弱前置條件，有狀態(tài)動(dòng)態(tài)偏序縮減 第i i 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 a b s t r a c t w i t ht h ew i d eu s i n go fc o m p u t e rs y s t e m s , t h et r u s t w o r t h yp r o p e r t i e so ft h e s o f t w a r ea r er e c e i v i n gm o t ea n dm o t a t t e n t i o n s t h ef o r m a lv e r i f i c a t i o no f t h es o f b , v a r e p r o g r a mi so n eo ft h ee f f e c t i v em e t h o d st op r o m i s em l s 陽(yáng)，o n l l y t h e r e f o r e ，m o r ea n d m o r er e s e a r c h e r sa r ea t t r a c t e dt ot h i sa f e a h o w e v e r , t h es o f t w a r ep r o g r a m su s u a l l y h a v ec o m p l e xl o g i ca n dl a r g es c a l e s oh o wt oi n c r e a s et h ea c c u r a c ya n dt h es c a h b i l i t y o f t h ep r o g r a mv e r i f i c a t i o ni st h em a i nr e s e a r c ht o p i c t h ed i s s e r t a t i o np r e s e n t san o v e lm e t h o d , n a m e l ys l i c i n ge x e c u t i o n ，t ov e r i f yc p r o g r a m sw i t hr e s p e c tt ot e m p o r a ls a f e t yp r o p e r t i e s i ti sb a s i c a l l yal i g h t w e i g h t s y m b o l ce x e c u t i o nt e c h n i c a la n dm a ya u t o m a t i c a l l ye x t r a c tf i n i t e m o d e l s f r o m s e q u e n t i a la n dc o n c u r r e n tcp r o g r a m s s l i c i n ge x e c u t i o ni n t e g r a t e ss e v e r a ls t a t es p a c e r e d u c t i o nt e c h n i q u e s ，i n c l u d i n gp r o g r a ms l i c i n g , a b s u a c t i o no fp r o g r a ms e m a n t i c s , s y m b o l i c a lr e p r e s e n t a t i o n , c o u n t e r e x a m p l eg u i d e d a b s t r a c t i o nr e f i n e m e n ta n d p a r t i a l - o r d e rr e d u c t i o n , e t c 。t h e r e f o r e ，t h es t a t es p a c e so ft h ea b s t r a c t e dm o d e l sc a nb e g r e a t l y r e d u c e d , a n d t h es c a l a b i l i t y o f t h e v e r i f i c a t i o nc a n b e i m p r o v e dc o r r e s p o n d i n g l y t h ed i s t i n g u i s h e df e a t u r eo fs l i c i n ge x e c u t i o ni st h a ti tm a ya c h i e v et h ea c c u r a c yo f p a t h - s e n s i t i v es i m u l a t i o nf o rv e r i f y i n gt e m p o r a ls a f e t yp r o p e r t i e s , o n l yw i t ht h ec o s t c l o s et os t a n d a r df l o w - s e n s i t i v ed a t a f l o wa n a l y s i s m o r et h a nt h a l - i ts u p p o r t sa r b i w a r y p r o g r a m 鰣n 地t l l r ei n c l u d i n ga l lk i n d so fp r o g r a ml o o p s i t 湖a l s of u u - a n t o m a t i c a l l y a b s t r a c tm o d e l sa n dv e r i f yp r o p e r t i e sw i t h o u t a n ya i do f p e o p l e s l i c i n ge x e c u t i o ni sf o u n d e do nt h eo v e r - a p p r o x i m a t e dp r o g r a ms e m a n t i c so fc p r o g r a m sb yv a r i a b l ea b s t r a c t i o n i to n l ys y m b o l i c a l l ye x e c u t e st h er e l e v a n ts t a t e m e n t s u n d e rv a r i a b l ea b s t r a c t o n , a n dc a l c u l a t e st h ep a r t i a ls t r o n g e s tp o s t - c o n d i t i o n sa n dt h e p a r t i a lw e a k e s tp r e c o n d i t i o n st oc o n s t r u c tf i n i t ea b s t r a c tm o d e l s ，w h i c hm a yb em o d e l c h e c k e dw i t hr e s p e c tt ot e m p o r a ls a f e t yp r o p e r t i e s b a s e do nt h ev e r i f i c a t i o nr e u s i n g f i a m e w o r kp r e s e n t e di nt h ed i s s e r t a t i o n , s l i c i n ge x e c u t i o nk e e p sr e f i n i n gt h ev a r i a b l e a b s t r a c t i o nc r i t e r i aa c c o r d i n gt ot h es p u r i o u sc o u n t e r e x a m p l ep a t h su n t i lt h ep r o p e r t yi s p r o v e no raf e a s i b l ec o u n t e r e x a m p l ep a t hi sf o u n d t ov e r i f yc o n c u r r e n tcp r o g r a m s ，a n o v e ls t a t e f u d y n a m i cp a r t i a l - o r d e rr e d u c t i o nm e t h o di s i n t e g r a t e di n t os l i c i n g e x e c u t i o n , w h i c hg r e a t l yr e d u c e st h es e a r c h i n gs 詛鈀s p a c e al i g h t w e i g h td e c i s i o n p r o c e d u r ei sa l s oi n t e g r a t e dt oe f f i c i e n t l yd e c i d et h ef o r m u l a sg e n e r a t e dd u r i n gt h e v e r i f i c a t i o no fcp r o g r a t m m o r et h o r o u g h l y , t h ei n n o v a t i o n so ft h ed i s s e r t a t i o na r e s u m m a r i z e di n t of o l l o w i n gf i v ea s p e c t s ： 第j i i 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 l ，t h eb a s i cd c f m i t i o ma n dt e c h n i q u e sf o rs l i c i n ge x e c u t i o n b a s e do nt h ea n a l y s i s o fp r a c t i c a lp r o g r a mv e r i f i c a t i o n , w ep r e s e n tv a r i a b l ea b s t r a c t i o nt oo n l yc o n s i d e rt h e v a r i a b l e sa n ds t a t e m e n t st h a ta r er e l e v a n tt ot h eg i v e np r o p e r t y w et h e np r e s e n tt h e p a r t i a ls t r o n g e s tp o s t - c o n d i t i o n , w h i c hr e p r e s e n t s t h e o v e r - a p p r o x i m a t e dp r o g r a m s e m a n t i c s f i n a l l y , w ep r e s e n ts l i c i n ge x e c u t i o na sal i g h t w e i g h ts y m b o l i ce x e c u t i o n 2 t h et e m p o r a ls a f e t yp r o p e r t yo r i e n t e ds e a r c h i n gr e u s i n gf r a m e w o r ka n di t s a p p l i c a t i o ni ns l i c i n ge x e c u t i o n l i k ec o u n t e r e x a m p l eg u i d e da b s t r a c t i o nr e f i n e m e n t ( c e g a r ) ，t h es e a r c h i n gr e u s i n gf r a m e w o r ka l s or e f i n e st h ea b s t r a c t e dm o d e lu n d e rt h e g u i d a n c eo fs p u r i o u sc o u n t e r e x a m p l e s h o w e v e r , i tm a k e s t h es e a r c h i n gi n f o r m a t i o nb e r e u s e da m o n gt h em o d e l so fd i f f e r e n tp r e c i s i o n , a n dt h u sag r e a td e a lo fr e d u n d a n t s e a r c h i n gm a yb ea v o i d e d 3 ，t h ed e f i n i t i o no fp a r t i a lw e a k e s tp r e c o n d i t i o na n di t sa p p l i c a t i o ni ns l i c i n g e x e c u t i o n t h c p a r t i a l w e a k e s t p r e c o n d i t i o n i sa n o t h e rw a yt o r e p r e s e n t t h e o v e r - a p p r o x h n a t e dp r o g r a ms e m a n t i c s ，a n di t sd e f i n i t i o ni sa l s ob a s e d0 1 1v a r i a b l e a b s t r a c t i o n i ns l i c i n ge x e c u t i o n , w em a yu s ep a r t i a lw e a k e s tp r e c o n d i t i o n st or e p l a c e p a r to fp a r t i a ls t r o n g e s tp o s t - c o n d i t i o n st og e n e r a t em u c hw e a k e rs t a t ef o r m u l a s a sa r e s u l lw em a yg r e a t l yr e d u c et h es t a t es p a c eo ft h ea b s t r a c t e dm o d e lw i t h o u tl o s so f a c c u r a c y 4 ，朝1 es t a t e f o ld y n a m i cp a r t i a l - o r d e rr e d u c t i o nt e c h n i q u ea n di t sa p p l i c a t i o ni n s l i c i n ge x e c u t i o n a & re x t e n d i n gs l i c i n ge x e c u t i o nt oc o n c u r r e n tcp r o g r a m s w e p r e s e n tt h es t a t e f o ld y n a m i cp a r t i a l - o r d e rr e d u c t i o nt e c h n i q u et og u i d ei tn o tt os e a r c h m u l t i p l ei n t e r l e a v i n gt r a n s i t i o ns e q u e n c e st h a th a st h es a m ep a r t i a l - o r d e r w es e l e c t s e v e r a le x p e r i m e n t si n c l u d i n gt w op r a c t i c a lp r o g r a mf r a g m e n t sa n dac o n c u r r e n ts s l s y s t e m 1 1 1 ce x p e r i m e n t si l l u s t r a t et h a tt h ei n t e g r a t i o no fs l i c i n ge x e c u t i o na n ds t a t e f i t l d y m i cp a r t i a l - o r d e rr e d u c t i o nl e a d st ot h er e d u c t i o no ft h es t a t es p a c e ，a sw e l la st h e r e d u c t i o no f t h es p a c ec o s to f t h ev e r i f i c a t i o n 5 t h el i g h t w e i g h td e c i s i o np r o c e d u r ef o rt h ev e r i f i c a t i o nf o r m u l a so fs l i c i n g e x e c u t i o n w ed e f i n ea ne x t e n d e dc l a s so fi n t e g e rl i n e a rf i r s t - o r d e rl o g i cf o r m u l a , w h i c h s u p p o r t sm o s ti n t e g e rl i n e a ra n db i t - w i s ee x p r e s s i o n si ncp r o g r a m si n c l u d i n gi n t e g e r d i v i s i o n , i n t e g e rm o d u l a ra n db i t - w i s eo p e r a t i o n e x p e r i m e n tr e s u l t ss h o wt h a tt h e e x t e n d e dd e c i s i o np r o c e d u r es u p p o r t sm o s tv e r i f i c a t i o nf o r m u l a sm e ti n s l i c i n g e x e c u t i o n b a s e do nt h ee x p e r i m e n to v e rt h ep r a c t i c a lp r o g r a mo p e n s s l - o 9 6 e ，w ef i n d t h a tt h ed e c i s i o nc o s ti s1 0 5t i m e sl e s st h a nt h et h e o r e mp r o v e rs i m p l i f y o u rs l i c i n ge x e c u t i o nt o o lp r o t o t y p ei si m p l e m e n t e do l lt h eo p e n - s o u r c ep r o j e c t 第i v 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 “舊i c e a c hi n n o v a t i o ni sd e m o n s t r a t e db ya l le x p e r i m e n to nt h ep r a c t i c a lp r o g r a m o p e n s s l - o 9 6 c w ea l s oc o m p a l oo u re x p e r m e n tr e s u l t sw i t hb l a s t a n dm a g i c a l l e x p e r i m e n t sa p e r f o r m e do i lm a c h i n e so fs a m eh a r d w a r e ，u s i n gs a l l l op r a c t i c a l p r o g r a ma n dv e r i f y i n gs a m ep r o p e r t i e s t h cc o m p a r i n gr e s u l t ss h o wt h a ts l i c i n g e x e c u t i o ni se v e nab i tf f l o r ee f f e c t i v et h a nt h eo t h e rt w o k e yw o r d s ：s c m ge x e c u t i o n , m o d e lc h e c k i n g , t e m p o r a ls a f e t yp r o p e r t y , c p r o g r a mv e r i f i c a t i o n , v a r i a b l ea b s t r a c t i o n , p a r t i a ls m ) n g e s tp o s t - c o n d i t i o n , p a r t i a l w e a k e s tp r e c o n d i t i o n , s t a t e f u ld y l n m i cp a r t i a l - o r d e rr e d u c t i o n 第v 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 表目錄 表2 1 表3 ，1 表4 1 表5 1 表5 2 表5 3 表6 1 表6 2 表7 1 s s l 協(xié)議的初始握手過(guò)程驗(yàn)證的實(shí)驗(yàn)結(jié)果 基于o p e n s s l 程序的切片執(zhí)行實(shí)驗(yàn)結(jié)果 集成部分最弱前置條件的切片執(zhí)行的實(shí)驗(yàn)結(jié)果比較。 兩條示例遷移序列的交迭信息總結(jié) 4 0 5 4 7 2 8 9 i n d e x e r 程序的實(shí)驗(yàn)結(jié)果比較9 5 f i l es y s t e m 程序的實(shí)驗(yàn)結(jié)果比較 示例并發(fā)程序的實(shí)驗(yàn)結(jié)果1 1 3 基于并發(fā)程序o p e n s s l 0 9 6 c 的s s l 協(xié)議初始握手過(guò)程驗(yàn)證。11 4 輕量級(jí)判定過(guò)程與定理證明工具s h n p u f y 的實(shí)驗(yàn)結(jié)果對(duì)比1 2 7 第頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 圖 目錄 圖1 1 圈2 1 圖2 2 圖2 3 圖2 4 圖2 5 圖2 6 圖3 1 圖3 2 圖3 3 圖3 a 圖3 5 圖4 1 圖4 2 圖4 3 圖4 4 圖5 1 圖5 2 圖5 3 圖5 4 圈5 5 圖5 6 圖5 7 圖5 8 圖6 1 圖6 2 圖6 3 圈6 4 圖6 5 圖6 6 圖7 1 圖7 2 切片執(zhí)行的技術(shù)體系組成 基于切片執(zhí)行的c 程序驗(yàn)證框架。 產(chǎn)生切片執(zhí)行圖的切片執(zhí)行過(guò)程 描述加解鎖用法的性質(zhì)自動(dòng)機(jī)示例。 基于切片執(zhí)行的加鎖時(shí)序安全性質(zhì)的驗(yàn)證示例 s s l 程序的代碼結(jié)構(gòu) 性質(zhì)s s l - c i n t - 1 描述的性質(zhì)自動(dòng)機(jī) 面向切片執(zhí)行的搜索復(fù)用框架 基于搜索復(fù)用框架的切片執(zhí)行過(guò)程偽代碼 帶圈的切片執(zhí)行圖示例 2 9 3 5 3 9 4 0 面向搜索復(fù)用框架的深度優(yōu)先切片執(zhí)行過(guò)程 船f ，九例程中的一段代碼 部分最弱前置條件示例程序代碼 4 7 5 l 5 5 集成了部分最弱前置條件的切片執(zhí)行過(guò)程 具有變量依賴關(guān)系的賦值語(yǔ)句組成的執(zhí)行路徑 轉(zhuǎn)換后被動(dòng)化形式的執(zhí)行路徑 基于動(dòng)態(tài)偏序縮減的無(wú)圈狀態(tài)空間遍歷過(guò)程 6 l 6 5 6 5 面向無(wú)圈狀態(tài)空間的回溯點(diǎn)和回溯進(jìn)程鑒別過(guò)程 基于有狀態(tài)動(dòng)態(tài)偏序縮減的含圈狀態(tài)空間遍歷過(guò)程 r e f i n e b a c k t r a c k s h 過(guò)程的實(shí)現(xiàn) 交迭信息總結(jié)的更新過(guò)程u p d a t e s i i 8 l 。8 3 9 2 9 3 交迭信息總結(jié)的合并過(guò)程m e r g e s l i f i l es y s t e m 示例程序 并發(fā)c 程序的基本切片執(zhí)行過(guò)程 集成無(wú)狀態(tài)動(dòng)態(tài)偏序縮減的切片執(zhí)行過(guò)程 無(wú)狀態(tài)動(dòng)態(tài)偏序縮減的回溯點(diǎn)和回溯進(jìn)程鑒別過(guò)程 基于時(shí)鐘向量的有狀態(tài)動(dòng)態(tài)偏序縮減方法的實(shí)現(xiàn) 集成有狀態(tài)動(dòng)態(tài)偏序縮減的切片執(zhí)行過(guò)程 1 0 3 1 0 6 1 0 7 1 0 9 基于并發(fā)c 程序建模環(huán)境改寫后的i n d e x e r 程序 整數(shù)線性判定問(wèn)題的一階邏輯公式定義 擴(kuò)充整數(shù)除法、取余和位運(yùn)算的c 程序判定公式 1 1 2 。1 1 7 1 2 1 第v 頁(yè) 獨(dú)創(chuàng)性聲明 本人聲明所呈交的學(xué)位論文是我本人在導(dǎo)師指導(dǎo)下進(jìn)行的研究工作及取得的研 究成果盡我所知，除了文中特別加以標(biāo)注和致謝的地方外，論文中不包含其他入已 經(jīng)發(fā)表和撰寫過(guò)的研究成果，也不包含為獲得國(guó)防科學(xué)技術(shù)大學(xué)或其它教育機(jī)構(gòu)的學(xué) 位或證書而使用過(guò)的材料與我一同工作的同志對(duì)本研究所做的任何貢獻(xiàn)均已在論文 中作了明確的說(shuō)明并表示謝意 學(xué)位論文題目：魚鯉魚毖墮絲塹翌星塹塑墮 學(xué)位論文作者搟：易址魄塒年7 月彳日 學(xué)位論文版權(quán)使用授權(quán)書 本人完全了解國(guó)防科學(xué)技術(shù)大學(xué)有關(guān)保留，使用學(xué)位論文的規(guī)定本人授權(quán)國(guó) 防科學(xué)技術(shù)大學(xué)可以保留并向國(guó)家有關(guān)部門或機(jī)構(gòu)送交論文的復(fù)印件和電子文檔，允 許論文被查閱和借閱；可以將學(xué)位論文的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫(kù)進(jìn)行檢索， 可以采用影印縮印或掃描等復(fù)制手段保存，匯編學(xué)位論文 ( 保密學(xué)位論文在解密后適用本授權(quán)書) 學(xué)位論文題目：量魚壘礁摩壘墾塑鯉烏毖查島 學(xué)位論文作者簽名：壺囊 作者指導(dǎo)教師簽名：跟呀勇9 1 一。， 日期：砌年羅月日 醐：翮年尸嘣日 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 第一章緒論 1 1 課題研究背景 1 1 1 軟件的可信性質(zhì) 隨著科技的高速發(fā)展和計(jì)算機(jī)技術(shù)的廣泛普及，人類社會(huì)的信息化，智能化 程度越來(lái)越高，作為其核心的計(jì)算機(jī)軟件已經(jīng)融入到人們生活的方方面面，從飛 機(jī)汽車到家用電器，都離不開(kāi)軟件的自動(dòng)控制。另一方面，由軟件控制的各種各 樣的機(jī)器和設(shè)備大量替代了以前必須由人工完成的低級(jí)勞動(dòng)，不僅極大地減輕了 人們工作量、減小了對(duì)工人可能造成的傷害，還大大地提高了工作的效率和質(zhì)量。 因此，如果說(shuō)計(jì)算機(jī)技術(shù)的應(yīng)用開(kāi)創(chuàng)了一種新的生活和工作方式的話。那么軟件 就是這種新方式的靈瑰和主導(dǎo)。 隨著軟件承擔(dān)了越來(lái)越重要的功能和作用，軟件失效所帶來(lái)的代價(jià)越來(lái)越不 能容忍。例如，海灣戰(zhàn)爭(zhēng)中由于軟件失效曾導(dǎo)致美國(guó)愛(ài)國(guó)者導(dǎo)彈未能及時(shí)攔截伊 拉克的飛毛腿導(dǎo)彈攻擊；軟件失效還導(dǎo)致1 9 9 6 年6 月歐_ i i la r i a n e 五型火箭首發(fā)失 敗，造成高達(dá)2 5 億美元的直接經(jīng)濟(jì)損失。 因此，作為信息化核心的軟件，必須滿足包括可靠性，安全性( 包括可靠安 全性和保密安全性) 、可用性、可生存性等性質(zhì)在內(nèi)的高可信性質(zhì)。其中，可靠 性是指在規(guī)定的環(huán)境下和規(guī)定的時(shí)間內(nèi)軟件無(wú)失效運(yùn)行的能力，可靠安全性是指 軟件運(yùn)行不引起危險(xiǎn)和災(zāi)難的能力，保密安全性是指軟件系統(tǒng)對(duì)數(shù)據(jù)和信息提供 保密性、完整性、可用性、真實(shí)性保障的能力，等等。 然而，軟件作為人類連續(xù)的高度復(fù)雜的智力產(chǎn)品，其科學(xué)原理和工程規(guī)律遠(yuǎn) 未得到充分的認(rèn)識(shí)，缺乏有效地生產(chǎn)滿足高可信軟件的軟件技術(shù)。導(dǎo)致的結(jié)果是： 一方面，人們的生產(chǎn)生活越來(lái)越依賴于各種各樣的軟件；另方面，隨著軟件功 能的日益復(fù)雜和強(qiáng)大，軟件的高可信性質(zhì)越來(lái)越不能保證例如，僅從軍事方面 來(lái)看，美國(guó)國(guó)防部認(rèn)為嵌入式軟件開(kāi)發(fā)成為美武器項(xiàng)目研制的瓶頸：面在國(guó)內(nèi)， 根據(jù)當(dāng)前總裝備部的調(diào)查結(jié)果可以看到，軟件失效已成為武器裝備系統(tǒng)不能正常 運(yùn)轉(zhuǎn)的主要原因，甚至已經(jīng)超過(guò)硬件出現(xiàn)的問(wèn)題。因此，如何有效的保證軟件的 安全性、提高可靠性成為軟件研究領(lǐng)域亟需解決的重大課題，并受到各國(guó)政府、 軍方和軟件公司的高度重視。 軟件的高可信性質(zhì)受到了國(guó)內(nèi)外政府、軍隊(duì)和企業(yè)的廣泛關(guān)注。作為1 9 9 9 年 著名的p i t a c 報(bào)告信息技術(shù)研究：為未來(lái)投資k i n f o r m a t i o nt e c h n o l o g yr e s e a r c h ： i n v e s t i n gi no u r f u t u r e ) 認(rèn)為美國(guó)“依賴于脆弱的軟件”，“缺乏構(gòu)造可靠安全軟 第1 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 件的技術(shù)”，明確指出將軟件基礎(chǔ)研究放在絕對(duì)優(yōu)先的位置上。2 0 0 1 年1 月，美 國(guó)n i t r d 信息技術(shù)研究與發(fā)展聯(lián)合工作組( i n t e r a g e n c yw o r k i n gg r o u po n i n f o r m a t i o n r e s e a r c ha n dd e v e l o p m e n t ) 發(fā)布了高可信軟件與系統(tǒng)研究需求( h i g h c o n f i d e n c es o m v a r ea n ds y s t e m sr e s e a r c hn e e 出) 報(bào)告提出了h c s s ( 高可信軟 件與系統(tǒng)) 的國(guó)家研究計(jì)劃。2 0 0 3 年9 月，n i t r d 在2 0 0 4 財(cái)年藍(lán)皮書美國(guó)創(chuàng) 新的先進(jìn)基礎(chǔ)( a d v a n c e df o u n d a t i o n sf o ra m e r i c a ni n n o v a t i o n ) 中，設(shè)計(jì)高可靠 軟件的有效方法，復(fù)雜軟件中高可信的科學(xué)和工程方法都成為了最優(yōu)先研究的內(nèi) 容。歐盟的第五框架計(jì)劃和第六框架計(jì)劃都把高可信軟件作為軟件技術(shù)發(fā)展的重 點(diǎn)，i n f o r m a t i o ns o c i e t yt e c h n o l o g i e s 支持了s a f e a i r i i ( 安全攸關(guān)系統(tǒng)的先進(jìn)設(shè) 計(jì)工具) 、o m e g a ( 實(shí)時(shí)嵌入式系統(tǒng)的正確開(kāi)發(fā)) 、a r t i s t ( 先進(jìn)實(shí)時(shí)系統(tǒng)) 等項(xiàng)目。為了應(yīng)對(duì)軟件安全性問(wèn)題，我國(guó)也采取了一些針對(duì)性措施，如制定了g j b z 1 0 2 - 9 7 軟件可靠性和安全性設(shè)計(jì)準(zhǔn)則等軟件開(kāi)發(fā)標(biāo)準(zhǔn)，并進(jìn)行了一些實(shí)踐。 1 1 2 基于軟件源代碼的可靠安全性質(zhì)保證 軟件可信性質(zhì)的保證是貫穿整個(gè)軟件生命周期的。在軟件的設(shè)計(jì)、實(shí)現(xiàn)、測(cè) 試、維護(hù)等階段進(jìn)行的可信性質(zhì)保證是相互依賴、缺一不可的。從保證方法上來(lái) 看。形式化方法對(duì)軟件可信性質(zhì)的保證有著不可替代的作用。然而，形式化方法 在實(shí)用軟件的可信性質(zhì)保證中仍不多見(jiàn)，基本處于實(shí)驗(yàn)室的試驗(yàn)階段，并且，其 使用者多是專家型用戶。因此，將形式化方法以工程化的途徑自動(dòng)化、可擴(kuò)展她 實(shí)施軟件安全性保證是一個(gè)重要趨勢(shì) 從當(dāng)前軟件的可信需求來(lái)看，可靠安全性( s a f e t y ) 需求占據(jù)了重要的地位， 它反應(yīng)了人們對(duì)軟件運(yùn)行不會(huì)引起災(zāi)難和危害的根本要求。從對(duì)軟件可靠安全性 質(zhì)的保證方法上來(lái)看，面向可靠安全性質(zhì)的軟件驗(yàn)證是一種重要且行之有效的手 段，從而得到了長(zhǎng)期和廣泛的研究和應(yīng)用。它通過(guò)檢驗(yàn)軟件是否滿足所關(guān)心的可 靠安全性質(zhì)，來(lái)最終保證軟件的可靠安全性。下文中，除非特別指明，否則我們 討論的安全性都是指可靠安全性。 本論文主要研究面向軟件源代碼驗(yàn)證的軟件安全性質(zhì)保證，它是軟件安全性 保證的一個(gè)重要組成部分，其意義主要表現(xiàn)在三個(gè)方面：首先，軟件源代碼包含 了軟件的所有細(xì)節(jié)，從而源代碼級(jí)的驗(yàn)證能夠準(zhǔn)確地回答所關(guān)心的安全性質(zhì)是否 得到保證：其次，軟件所關(guān)心的大量安全性質(zhì)本身就是針對(duì)軟件源代碼的，例如 不能有空指針、數(shù)組越界等安全性質(zhì)，從而只能在源代碼級(jí)進(jìn)行驗(yàn)證和保證，同 時(shí)軟件編碼又是最容易引入錯(cuò)誤的階段之一，因此源代碼級(jí)的安全性質(zhì)的驗(yàn)證能 夠確實(shí)提高軟件可信性：最后，從目前軟件工程方法的應(yīng)用現(xiàn)狀來(lái)看，軟件安全 性保證的主要矛盾尚處在軟件代碼層面上，在軟件開(kāi)發(fā)中，開(kāi)發(fā)者把大量的時(shí)間 第2 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 和精力花費(fèi)在尋找軟件錯(cuò)誤的調(diào)試和測(cè)試中，而結(jié)果依然是不完全的。同時(shí)，目 前使用的軟件開(kāi)發(fā)平臺(tái)中對(duì)安全性保證的技術(shù)支持十分薄弱，主要通過(guò)軟件過(guò)程 控制進(jìn)行保障，人為因素占了主導(dǎo)地位，從而帶來(lái)了很大的不確定性。 當(dāng)前面向源代碼的安全性質(zhì)保證主要依靠軟件開(kāi)發(fā)人員來(lái)手工發(fā)現(xiàn)軟件中的 錯(cuò)誤，開(kāi)發(fā)人員通過(guò)對(duì)軟件執(zhí)行步驟、變量和數(shù)據(jù)結(jié)構(gòu)狀態(tài)的變化、斷言的違反 等進(jìn)行跟蹤和判斷，以確定程序中是否存在錯(cuò)誤。一般情況下，這只能發(fā)現(xiàn)一些 簡(jiǎn)單、明顯的錯(cuò)誤。當(dāng)軟件稍微復(fù)雜一些，由于龐大的可能運(yùn)行路徑集合，即使 調(diào)試中不出現(xiàn)錯(cuò)誤，也不能說(shuō)明軟件中就不存在錯(cuò)誤。對(duì)于高可信軟件，其失效 并不僅僅是一些簡(jiǎn)單的計(jì)算錯(cuò)誤，可能存在的進(jìn)程同步時(shí)序錯(cuò)誤、死鎖、接口綁 定錯(cuò)誤、訪問(wèn)越界、棧溢出、空指針等，都會(huì)導(dǎo)致軟件運(yùn)行失效，而這些是僅僅 通過(guò)傳統(tǒng)調(diào)試手段無(wú)法完全發(fā)現(xiàn)的。已有斷言方法主要對(duì)一些布爾表達(dá)式進(jìn)行判 斷，也不能有效解決這些闖題。例如，g j b z1 0 2 - 9 7 軟件可靠性和安全性設(shè)計(jì)準(zhǔn) 則中所列出的大量安全性要求都是傳統(tǒng)調(diào)試和編譯環(huán)境難以發(fā)現(xiàn)的，因而在實(shí) 際軟件開(kāi)發(fā)中出現(xiàn)了可操作性差等問(wèn)題。 體現(xiàn)源代碼級(jí)驗(yàn)證這種安全性保障技術(shù)的發(fā)展趨勢(shì)的一個(gè)值得關(guān)注的動(dòng)向是 由圖靈獎(jiǎng)獲得者t o n y h o a r e ( 現(xiàn)任職微軟劍橋研究院) 于2 0 0 2 年提出的程序驗(yàn)證 器( v e r i f y i n gc o m p i l e r ，后改稱p r o g r a mv e r i f i e r ) 設(shè)想他希望程序驗(yàn)證器通過(guò) 自動(dòng)化的數(shù)學(xué)和邏輯推理方法檢測(cè)其所編譯的程序的正確性，而該正確性是通過(guò) 程序中的類型、斷言，規(guī)范或其它一些標(biāo)注進(jìn)行聲明的。該設(shè)想正是我們的研究 目標(biāo)和研究?jī)?nèi)容。事實(shí)上。微軟在其軟件開(kāi)發(fā)中廣泛使用各類斷言以提高程序可 調(diào)試的能力，并開(kāi)發(fā)出程序分析工具p r e f i x 供其內(nèi)部各開(kāi)發(fā)小組在調(diào)試中使用。 以檢查程序中每條路徑可能出現(xiàn)的空指針、訪問(wèn)越界等高可信軟件所關(guān)注的錯(cuò)誤 中的一些較為簡(jiǎn)單的部分( 但其面臨的一個(gè)問(wèn)題是找到的很多錯(cuò)誤路徑實(shí)際是不 可行的，需要人工排除這些不可行路徑) 工業(yè)界2 0 0 2 年統(tǒng)計(jì)結(jié)果認(rèn)為，若程序 驗(yàn)證器當(dāng)時(shí)能夠投入實(shí)用，美國(guó)當(dāng)年因?yàn)槌绦蝈e(cuò)誤引起的損失可以減少2 2 0 6 0 0 億美元。目前，驗(yàn)證編譯器被國(guó)際計(jì)算機(jī)軟件領(lǐng)域認(rèn)為是甚至可以和人類登月， 人類基因組圖譜等相提并論的巨大挑戰(zhàn)之一。 1 2 相關(guān)研究工作 面向軟件源程序的形式化分析與驗(yàn)證方法可以分為動(dòng)態(tài)與靜態(tài)兩大類方法， 動(dòng)態(tài)方法是指運(yùn)行待檢驗(yàn)的程序，并根據(jù)程序的動(dòng)態(tài)運(yùn)行情況判斷待驗(yàn)證的性質(zhì) 1 最近，該設(shè)想又被改名為v e r i f i e ds o f t w a r e ，并包含了軟件需求分析、設(shè)計(jì)、實(shí)現(xiàn)等不同軟 件開(kāi)發(fā)階段的安全性保障需求。但面向程序的驗(yàn)證仍是該設(shè)想的主要內(nèi)容之一。 第3 頁(yè) 國(guó)防科學(xué)技術(shù)大學(xué)研究生院博士學(xué)位論文 是否被滿足，例如測(cè)試方法；而靜態(tài)方法則是指通過(guò)對(duì)程序源代碼進(jìn)行靜態(tài)分析 來(lái)分析和驗(yàn)證其是否滿足某種性質(zhì)。兩類方法各有優(yōu)缺點(diǎn)：動(dòng)態(tài)方法往往不能保 證對(duì)程序進(jìn)行完全的分析和驗(yàn)證，即不能保證性質(zhì)一定被程序滿足，而靜態(tài)方法 所花費(fèi)的時(shí)間與空間的代價(jià)往往比動(dòng)態(tài)方法大得多。本文的研究是圍繞靜態(tài)方法 展開(kāi)的，研究的重點(diǎn)集中在如何盡量減小靜態(tài)分析和驗(yàn)證方法的時(shí)間和空間開(kāi)銷， 從而提高靜態(tài)方法的可擴(kuò)展性。 根據(jù)特性的不同，我們將靜態(tài)方法分為以下五類進(jìn)行介紹，即靜態(tài)分析方法， 定理證明方法、抽象解釋方法、模型檢驗(yàn)方法和謂詞抽象方法，下面我們結(jié)合實(shí) 例介紹這五類方法的研究進(jìn)展 1 - 2 1 靜態(tài)分析方法 靜態(tài)分析( s t a t i ca n a l y s i s ) 是指直接對(duì)程序進(jìn)行分析，以檢查程序源代碼是 否滿足某種性質(zhì)。靜態(tài)分析方法的思想比較直接，它往往較少涉及程序語(yǔ)義，因 此一般來(lái)說(shuō)不能保證可靠性和完備性。 使用靜態(tài)分析方法的一個(gè)成功的例子來(lái)自于m mt - j w a s t o n 研究中心的 x i a o l a nz h a n g 和a n t o n ye d w a r d s 的工作，他們使用一種基于類型的靜態(tài)檢查工具 c q u a l 1 】對(duì)l i n u x 操作系統(tǒng)的l s m ( l i n u xs e c u r i t ym o d e l s ) 框架在內(nèi)核中鉤子函 數(shù)的放置進(jìn)行了驗(yàn)證并找到了一個(gè)b u 毋