（计算机科学与技术专业论文）面向c程序验证的切片执行方法.pdf

国防科学技术大学研究生院博士学位论文 摘要 随着计算机系统的广泛应用，计算机软件的高可信性质受到了越来越多的关 注。面向软件源程序的形式验证是保障软件高可信性质的一种有效方法，受到了 大量的关注和广泛的研究。但是，由于软件程序逻辑复杂、规模庞大，如何提高 软件源程序验证的精度特别是可扩展性仍是当前研究所面临的主要问题。 本文提出了一种面向c 程序的时序安全性质验证方法，即切片执行方法。它 本质上是一种轻量级的符号执行，能够自动抽象出顺序和并发c 程序的有限状态 模型，并基于模型检验方法进行验证。切片执行融合了程序切片，程序语义抽象、 符号化状态表示、反例制导的抽象精化、偏序缩减等多种有效的状态空间缩减技 术，大大缩减了抽象模型的状态空间，从而提高了软件源程序形式验证的可扩展 性。切片执行的主要特点是面向时序安全性质的验证，能够以接近标准流敏感数 据流分析的代价，达到路径敏感程序模拟的验证精度；同时切片执行支持包括循 环在内的程序结构，支持全自动的模型抽象和性质验证。 切片执行构建在基于变量抽象的程序保守近似语义的基础上，它符号化地执 行变量抽象下的相关语句计算用于描述程序保守近似语义的部分最强后置条件 和部分最弱前置条件，抽象出c 程序的有限状态模型，并基于模型检验方法验证 抽象模型是否满足给定的时序安全性质。基于本文提出的搜索复用框架，切片执 行不断根据产生的伪反例路径精化变量抽象的抽象准则，直到性质被验证或找到 真实反例路径面向并发c 程序验证，切片执行集成了本文提出的有状态动态偏 序缩减方法，大大缩减搜索的状态空间切片执行还集成了一种轻量级判定过程， 用于对c 程序验证过程中的验证公式进行高效判定具体地，本文的创新点包括 如下五个方面： l 、提出了切片执行的基本概念和方法基于对程序验证基本规律的分析，我 们提出了变量抽象方法，只考虑程序中与待验证性质相关的变量和语句基于变 量抽象，我们定义了部分最强后置条件，进而定义了程序的保守近似语义。基于 这两个概念，我们提出了切片执行的概念，它是一种轻量级的符号执行过程 2 、提出了面向时序安全性质验证的搜索复用框架并将其应用于切片执行。搜 索复用框架也是一种反例路径制导的抽象精化( c e g a r ) 框架，基于伪反例路径 进行模型精化。相比传统的c e g a r 框架，搜索复用框架的最大特点是能够在不同 精度的抽象模型之间进行充分的信息复用，从而避免了大量不必要的重复搜索， 有效降低了验证开销。 3 、提出了部分最弱前置条件的概念并将其应用于切片执行部分最弱前置条 第i 页 国防科学技术大学研究生院博士学位论文 件是程序保守近似语义的另一种表示方法，同样基于变量抽象定义在切片执行 过程中，可以用部分最弱前置条件部分地取代部分最强后置条件，以生成更弱的 一阶逻辑公式来描述抽象模型的同一个状态，从而在不影响模型精度的前提下有 效缩减生成模型的状态空间。 4 、提出了面向有状态模型检验的有状态动态偏序缩减方法，并将其集成到切 片执行过程中。我们将切片执行方法扩展到了对并发c 程序的验证。为了进一步 进行状态空问缩减，我们提出了有状态动态偏序缩减方法，并将其自然地集成到 切片执行框架中，用于指导切片执行，使其避免搜索多条具有相同偏序关系的并 发进线程交迭执行路径。我们进行了多个实验，包括两个实用并发程序片段和一 个并发s s l 程序实验结果表明，切片执行和有状态动态偏序缩减这两种正交的 状态空问缩减方法的集成，大大缩减了并发程序抽象模型的状态空问，特别是降 低了验证的空间开销。 5 、提出了面向切片执行验证公式的轻量级判定过程。我们定义了一类整数线 性一阶逻辑判定公式，此类判定公式支持c 程序中常用的整数线性运算。我们优 化了判定过程，并扩充了对整数除法、取余和位运算的支持实验表明，扩充后 的判定过程能够对面向c 程序的切片执行所产生的绝大多数验证公式进行高效判 定。在基于s s l 程序的切片执行实验中我们发现，采用该判定方法后，验证效率 比使用定理证明工具s i m p l i 匆提高了1 0 5 倍 我们还基于开放源代码的m a g i c 项目，实现了基于切片执行的c 程序验证 工具原型，并基于o p e n s s l * 0 9 6 c 等实用程序针对上述每个创新点都进行了实验。 我们在实验时采用了与b l a s t 和m a g i c 相同的硬件平台，并针对相同的验证用 例，验证了相同的性质集合。经过充分的实验数据对比，我们发现切片执行在验 证效率上具有一定的优势。 主题词：切片执行，模型检验，时序安全性质，c 程序验证，变量抽象，部分 最强后置条件，部分最弱前置条件，有状态动态偏序缩减 第i i 页 国防科学技术大学研究生院博士学位论文 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 阳，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 页 国防科学技术大学研究生院博士学位论文 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 页 国防科学技术大学研究生院博士学位论文 “旧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 页 国防科学技术大学研究生院博士学位论文 表目录 表2 1 表3 ，1 表4 1 表5 1 表5 2 表5 3 表6 1 表6 2 表7 1 s s l 协议的初始握手过程验证的实验结果 基于o p e n s s l 程序的切片执行实验结果 集成部分最弱前置条件的切片执行的实验结果比较。 两条示例迁移序列的交迭信息总结 4 0 5 4 7 2 8 9 i n d e x e r 程序的实验结果比较9 5 f i l es y s t e m 程序的实验结果比较 示例并发程序的实验结果1 1 3 基于并发程序o p e n s s l 0 9 6 c 的s s l 协议初始握手过程验证。11 4 轻量级判定过程与定理证明工具s h n p u f y 的实验结果对比1 2 7 第页 国防科学技术大学研究生院博士学位论文 图 目录 图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 切片执行的技术体系组成 基于切片执行的c 程序验证框架。 产生切片执行图的切片执行过程 描述加解锁用法的性质自动机示例。 基于切片执行的加锁时序安全性质的验证示例 s s l 程序的代码结构 性质s s l - c i n t - 1 描述的性质自动机 面向切片执行的搜索复用框架 基于搜索复用框架的切片执行过程伪代码 带圈的切片执行图示例 2 9 3 5 3 9 4 0 面向搜索复用框架的深度优先切片执行过程 船f ，九例程中的一段代码 部分最弱前置条件示例程序代码 4 7 5 l 5 5 集成了部分最弱前置条件的切片执行过程 具有变量依赖关系的赋值语句组成的执行路径 转换后被动化形式的执行路径 基于动态偏序缩减的无圈状态空间遍历过程 6 l 6 5 6 5 面向无圈状态空间的回溯点和回溯进程鉴别过程 基于有状态动态偏序缩减的含圈状态空间遍历过程 r e f i n e b a c k t r a c k s h 过程的实现 交迭信息总结的更新过程u p d a t e s i i 8 l 。8 3 9 2 9 3 交迭信息总结的合并过程m e r g e s l i f i l es y s t e m 示例程序 并发c 程序的基本切片执行过程 集成无状态动态偏序缩减的切片执行过程 无状态动态偏序缩减的回溯点和回溯进程鉴别过程 基于时钟向量的有状态动态偏序缩减方法的实现 集成有状态动态偏序缩减的切片执行过程 1 0 3 1 0 6 1 0 7 1 0 9 基于并发c 程序建模环境改写后的i n d e x e r 程序 整数线性判定问题的一阶逻辑公式定义 扩充整数除法、取余和位运算的c 程序判定公式 1 1 2 。1 1 7 1 2 1 第v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研 究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他入已 经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它教育机构的学 位或证书而使用过的材料与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意 学位论文题目：鱼鲤鱼毖堕丝堑翌星堑塑堕 学位论文作者擀：易址魄埘年7 月彳日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留，使用学位论文的规定本人授权国 防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允 许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印缩印或扫描等复制手段保存，汇编学位论文 ( 保密学位论文在解密后适用本授权书) 学位论文题目：量鱼垒礁摩垒垦塑鲤乌毖查岛 学位论文作者签名：壶囊 作者指导教师签名：跟呀勇9 1 一。， 日期：砌年罗月日 醐：翮年尸嘣日 国防科学技术大学研究生院博士学位论文 第一章绪论 1 1 课题研究背景 1 1 1 软件的可信性质 随着科技的高速发展和计算机技术的广泛普及，人类社会的信息化，智能化 程度越来越高，作为其核心的计算机软件已经融入到人们生活的方方面面，从飞 机汽车到家用电器，都离不开软件的自动控制。另一方面，由软件控制的各种各 样的机器和设备大量替代了以前必须由人工完成的低级劳动，不仅极大地减轻了 人们工作量、减小了对工人可能造成的伤害，还大大地提高了工作的效率和质量。 因此，如果说计算机技术的应用开创了一种新的生活和工作方式的话。那么软件 就是这种新方式的灵瑰和主导。 随着软件承担了越来越重要的功能和作用，软件失效所带来的代价越来越不 能容忍。例如，海湾战争中由于软件失效曾导致美国爱国者导弹未能及时拦截伊 拉克的飞毛腿导弹攻击；软件失效还导致1 9 9 6 年6 月欧_ i i la r i a n e 五型火箭首发失 败，造成高达2 5 亿美元的直接经济损失。 因此，作为信息化核心的软件，必须满足包括可靠性，安全性( 包括可靠安 全性和保密安全性) 、可用性、可生存性等性质在内的高可信性质。其中，可靠 性是指在规定的环境下和规定的时间内软件无失效运行的能力，可靠安全性是指 软件运行不引起危险和灾难的能力，保密安全性是指软件系统对数据和信息提供 保密性、完整性、可用性、真实性保障的能力，等等。 然而，软件作为人类连续的高度复杂的智力产品，其科学原理和工程规律远 未得到充分的认识，缺乏有效地生产满足高可信软件的软件技术。导致的结果是： 一方面，人们的生产生活越来越依赖于各种各样的软件；另方面，随着软件功 能的日益复杂和强大，软件的高可信性质越来越不能保证例如，仅从军事方面 来看，美国国防部认为嵌入式软件开发成为美武器项目研制的瓶颈：面在国内， 根据当前总装备部的调查结果可以看到，软件失效已成为武器装备系统不能正常 运转的主要原因，甚至已经超过硬件出现的问题。因此，如何有效的保证软件的 安全性、提高可靠性成为软件研究领域亟需解决的重大课题，并受到各国政府、 军方和软件公司的高度重视。 软件的高可信性质受到了国内外政府、军队和企业的广泛关注。作为1 9 9 9 年 著名的p i t a c 报告信息技术研究：为未来投资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 ) 认为美国“依赖于脆弱的软件”，“缺乏构造可靠安全软 第1 页 国防科学技术大学研究生院博士学位论文 件的技术”，明确指出将软件基础研究放在绝对优先的位置上。2 0 0 1 年1 月，美 国n i t r d 信息技术研究与发展联合工作组( 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 ) 发布了高可信软件与系统研究需求( 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 出) 报告提出了h c s s ( 高可信软 件与系统) 的国家研究计划。2 0 0 3 年9 月，n i t r d 在2 0 0 4 财年蓝皮书美国创 新的先进基础( 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 ) 中，设计高可靠 软件的有效方法，复杂软件中高可信的科学和工程方法都成为了最优先研究的内 容。欧盟的第五框架计划和第六框架计划都把高可信软件作为软件技术发展的重 点，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 ( 安全攸关系统的先进设 计工具) 、o m e g a ( 实时嵌入式系统的正确开发) 、a r t i s t ( 先进实时系统) 等项目。为了应对软件安全性问题，我国也采取了一些针对性措施，如制定了g j b z 1 0 2 - 9 7 软件可靠性和安全性设计准则等软件开发标准，并进行了一些实践。 1 1 2 基于软件源代码的可靠安全性质保证 软件可信性质的保证是贯穿整个软件生命周期的。在软件的设计、实现、测 试、维护等阶段进行的可信性质保证是相互依赖、缺一不可的。从保证方法上来 看。形式化方法对软件可信性质的保证有着不可替代的作用。然而，形式化方法 在实用软件的可信性质保证中仍不多见，基本处于实验室的试验阶段，并且，其 使用者多是专家型用户。因此，将形式化方法以工程化的途径自动化、可扩展她 实施软件安全性保证是一个重要趋势 从当前软件的可信需求来看，可靠安全性( s a f e t y ) 需求占据了重要的地位， 它反应了人们对软件运行不会引起灾难和危害的根本要求。从对软件可靠安全性 质的保证方法上来看，面向可靠安全性质的软件验证是一种重要且行之有效的手 段，从而得到了长期和广泛的研究和应用。它通过检验软件是否满足所关心的可 靠安全性质，来最终保证软件的可靠安全性。下文中，除非特别指明，否则我们 讨论的安全性都是指可靠安全性。 本论文主要研究面向软件源代码验证的软件安全性质保证，它是软件安全性 保证的一个重要组成部分，其意义主要表现在三个方面：首先，软件源代码包含 了软件的所有细节，从而源代码级的验证能够准确地回答所关心的安全性质是否 得到保证：其次，软件所关心的大量安全性质本身就是针对软件源代码的，例如 不能有空指针、数组越界等安全性质，从而只能在源代码级进行验证和保证，同 时软件编码又是最容易引入错误的阶段之一，因此源代码级的安全性质的验证能 够确实提高软件可信性：最后，从目前软件工程方法的应用现状来看，软件安全 性保证的主要矛盾尚处在软件代码层面上，在软件开发中，开发者把大量的时间 第2 页 国防科学技术大学研究生院博士学位论文 和精力花费在寻找软件错误的调试和测试中，而结果依然是不完全的。同时，目 前使用的软件开发平台中对安全性保证的技术支持十分薄弱，主要通过软件过程 控制进行保障，人为因素占了主导地位，从而带来了很大的不确定性。 当前面向源代码的安全性质保证主要依靠软件开发人员来手工发现软件中的 错误，开发人员通过对软件执行步骤、变量和数据结构状态的变化、断言的违反 等进行跟踪和判断，以确定程序中是否存在错误。一般情况下，这只能发现一些 简单、明显的错误。当软件稍微复杂一些，由于庞大的可能运行路径集合，即使 调试中不出现错误，也不能说明软件中就不存在错误。对于高可信软件，其失效 并不仅仅是一些简单的计算错误，可能存在的进程同步时序错误、死锁、接口绑 定错误、访问越界、栈溢出、空指针等，都会导致软件运行失效，而这些是仅仅 通过传统调试手段无法完全发现的。已有断言方法主要对一些布尔表达式进行判 断，也不能有效解决这些闯题。例如，g j b z1 0 2 - 9 7 软件可靠性和安全性设计准 则中所列出的大量安全性要求都是传统调试和编译环境难以发现的，因而在实 际软件开发中出现了可操作性差等问题。 体现源代码级验证这种安全性保障技术的发展趋势的一个值得关注的动向是 由图灵奖获得者t o n y h o a r e ( 现任职微软剑桥研究院) 于2 0 0 2 年提出的程序验证 器( 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 ) 设想他希望程序验证器通过 自动化的数学和逻辑推理方法检测其所编译的程序的正确性，而该正确性是通过 程序中的类型、断言，规范或其它一些标注进行声明的。该设想正是我们的研究 目标和研究内容。事实上。微软在其软件开发中广泛使用各类断言以提高程序可 调试的能力，并开发出程序分析工具p r e f i x 供其内部各开发小组在调试中使用。 以检查程序中每条路径可能出现的空指针、访问越界等高可信软件所关注的错误 中的一些较为简单的部分( 但其面临的一个问题是找到的很多错误路径实际是不 可行的，需要人工排除这些不可行路径) 工业界2 0 0 2 年统计结果认为，若程序 验证器当时能够投入实用，美国当年因为程序错误引起的损失可以减少2 2 0 6 0 0 亿美元。目前，验证编译器被国际计算机软件领域认为是甚至可以和人类登月， 人类基因组图谱等相提并论的巨大挑战之一。 1 2 相关研究工作 面向软件源程序的形式化分析与验证方法可以分为动态与静态两大类方法， 动态方法是指运行待检验的程序，并根据程序的动态运行情况判断待验证的性质 1 最近，该设想又被改名为v e r i f i e ds o f t w a r e ，并包含了软件需求分析、设计、实现等不同软 件开发阶段的安全性保障需求。但面向程序的验证仍是该设想的主要内容之一。 第3 页 国防科学技术大学研究生院博士学位论文 是否被满足，例如测试方法；而静态方法则是指通过对程序源代码进行静态分析 来分析和验证其是否满足某种性质。两类方法各有优缺点：动态方法往往不能保 证对程序进行完全的分析和验证，即不能保证性质一定被程序满足，而静态方法 所花费的时间与空间的代价往往比动态方法大得多。本文的研究是围绕静态方法 展开的，研究的重点集中在如何尽量减小静态分析和验证方法的时间和空间开销， 从而提高静态方法的可扩展性。 根据特性的不同，我们将静态方法分为以下五类进行介绍，即静态分析方法， 定理证明方法、抽象解释方法、模型检验方法和谓词抽象方法，下面我们结合实 例介绍这五类方法的研究进展 1 - 2 1 静态分析方法 静态分析( s t a t i ca n a l y s i s ) 是指直接对程序进行分析，以检查程序源代码是 否满足某种性质。静态分析方法的思想比较直接，它往往较少涉及程序语义，因 此一般来说不能保证可靠性和完备性。 使用静态分析方法的一个成功的例子来自于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 的工作，他们使用一种基于类型的静态检查工具 c q u a l 1 】对l i n u x 操作系统的l s m ( l i n u xs e c u r i t ym o d e l s ) 框架在内核中钩子函 数的放置进行了验证并找到了一个b u 毋