（计算机软件与理论专业论文）基于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 国内外研究动态2 1 3 创新点和主要工作3 1 4 章节安排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 统一建模语言u m l 3 1 4 2 扩展层次自动机e h a 3 4 4 3u m l 行为模型到e h a 的转换规则3 6 4 3 1 状态图的转换规则3 6 4 3 2 活动图的转换规则3 8 4 4e h a 模型到p r o m e l a 语言的转换规则4 1 第一章引言 1 1 研究目的和意义 第一章引言 从2 0 世纪9 0 年代米期开始，因特网r 臻成熟和计算机广泛应用，引发了一 场全球范围内的信息革命，全球信息化的步伐不断加快，信息化社会正在形成并 走向成熟。 人们对计算机的依赖性与日俱增，这使得计算机的安全故障产生的各种危害 也是空前的增加。1 9 6 6 年欧洲航天局发射的火箭在升空后，紧紧3 7 秒钟就爆炸 坠毁。人们在对这次惨剧进行分析和研究时才发现了此次空难的原因，火箭的 惯性制导系统的软件存在一个微小的规约和设计错误。然而，如果在当时采用了 模型检测技术，就能够很好的检测出软件在设计时存在的这类逻辑漏洞，这次耗 资8 0 亿美元的航空计划就不会失败了。软件的高可靠性要求成为软件开发的首 要问题，尤其是在安全攸关领域更是如此。高可靠性软件和系统受到了广泛的重 视，成为计算机科学技术研究的重要热点。美国国家宇航局( n a s a ) 于1 9 9 5 年 7 月和1 9 9 7 年5 月先后发布了形式化方法规范和验证指南；美国国家自然科 学基金会在2 0 0 0 年财政年度启动了至今为止规模最大的研究计划，强调利用验 证和形式化方法来保证系统行为的正确可靠性等等。 应用形式化方法的目的就是保证软件的可靠性。上世纪6 0 年代，面对当时 的软件危机，f l o y d 、h o a r e 和m a n n a 等学者进行了程序的正确性证明研究，他 们用数学方法来证明程序的正确性并发展了各种程序正确性验证方法。上世纪八 十年代，在硬件方面的形式化方法的应用热潮，使得很多学者不断地研究将形式 化方法应用在软件领域。p n u e l i 提出了反应式系统规格和验证的时态逻辑方法。 c l a r k e 和e m e r s o n 提出了对有穷状态并发系统的模型检测方法。上世纪9 0 年代 以来，形式化研究和在工业中的应用得到了长足的发展。 形式化方法可以定义为：“用于开发计算机系统的形式化方法是基于数学的 用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框 架中以系统的方式刻画、开发和验证系统”。 2 1 形式化方法可以分为形式化规格和形式化验证。其中，形式化规格方法有： 有限状态机、s t a t e c h a r t s 、p e t r i 网、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 。 形式化方法从产生到现在，已经开发了一系列不同的方法和工具。因此，不 断地学习和掌握网际上先进的形式化方法，并且将形式化方法技术应用于我国的 国防、科技、办公、工业生产等各个方面，成为我国软件领域的重要课题。 青岛大学硕i ：学位论文 模型检测技术是形式化方法的主要技术之一。模型检测理论的研究与创新， 以及将模型检测技术应用于软件领域也成为今年来研究的重要内容。本文主要研 究了如何将模型检测技术应用到软件漏洞检测方面。传统的软件检测技术，往往 是在软件开发后期，对软件成品的检测。在软件开发初期，对软件进行逻辑漏洞 的检测可以大大的减少软件开发成本。目前，几乎所有软件开发者，在开发初期 使用统一建模语言( u m l ) 对软件功能、框架、角色以及动作序列等进行描述。 因此，对软件漏洞的检测可以对软件开发初期的u m l 模型，使用模型检测技术进 行漏洞检测。 1 2 国内外研究动态 软件漏洞的形式化检测方法的研究可以根据不同的标准分为不同的方面： ( 1 ) 按照软件开发阶段，形式化检测方法主要分为软件开发初期即需求分 析阶段和设计阶段的形式化检测方法研究和软件测试阶段的形式化检测方法的 研究。 ( 2 ) 按照软件性质的不同，形式化检测方法主要分为安全协议的形式化检 测方法研究和实时混成系统的形式化检测方法研究。 ( 3 ) 按照软件漏洞的性质的不同，分为针对不同漏洞的形式化检测方法。 基于软件开发阶段的形式化检测方法的研究，主要是对软件开发初期的需求 分析阶段的设计模型进行形式化规格与验证，很多学者在研究的过程基于u m l 视 图模型进行各种形式化研究。 u m l 虽然采用了四层体系结构，但是它的语法结构还不是形式化意义上的定 义，而是基于自然语言和u m l 子集元素的描述。在对其描述的模型进行定量定性 分析和验证时，很难采用形式化的方法。因此，基于u m l 的形式化研究已经成为 了国内外学术界关注的热点。 国外的学术界对u m l 语义进行形式化研究的两个主要思路是晦1 ： 一方面是对u m l 核心语法进行形式化，使u m l 成为符合形式化规范的语言。 英国的p u m l ( p r e c i s eu m lg r o u p ) 运用浅显的数学知识描述元模型层次的元素， 从而建立u m l 模型层和用户对象层的数学模型基础。文献u m l 和谓词转换入手， 可以建立一组和u m l 相对应的数学模型。文献对状态图中的各种状态及迁移函数 进行了形式化定义。文献定义了一种包含对象流描述u m l 活动图的形式化语义。 另方面，利用形式化语言在不丢失或少丢失信息的前提下对u m l 进行形式 化。该方法对每种u m l 图形赋予形式化语言，然后利用已有的形式化语言和工具 对u m l 模型进行推理验证。文献口1 使用p e t r i 网元素，将u m l 的四个模型元素进 行了描述，并且实现了从u m l 活动图模型到p e t r i 网的转换算法。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 动态行为模型看作是一组交互状态自动机，基于分支时间逻辑 一a c t l 和演算，使用模型检测工具对u m l 模型进行了验证。 国内的研究主要在以下几个方面： 国内在软件开发初期的研究主要是对u m l 模型进行形式化验证。文献们提出 了基于自动机理论的活动图模型检测方法，该方法首先建立系统自动机，然后将 系统的待测属性使用l t l 公式描述，为性质的否定命题建立b u c h i 自动机。计算 两个自动机的乘积。最后检查该乘积自动机所能接受的语言是否为空。这种方法 虽然给我们提供了一种检测u m l 活动图属性检测的方法，但是，这种方法需要有 自动机理论基础的人才能运用。在实际应用之中，这种方法难以被工作人员接受。 因此，能够简单地应用到实际工作中的模型检测方法及工具，成为专家学者的主 要研发目标。分析了u m l 状态图的结构特点和语义特征，构造了层次化着色p e t r i 网h c p n 。主要解决了使用p e t r i 网进行形式化验证的问题。文献1 使用k r i p k e 结构赋予了u m l 状态图形式化语义，提出并证明了u m l 状态图和k r i p k e 结构语 义的双映射关系。为了更好的研究u m l 类图，从而适应形式化描述方法时序 逻辑语言x y z e 来表示类图形式化语义的方法。对顺序图的形式化研究方法主要 采用将顺序图转换为元模型的描述语言0 c l ，然后将o c l 转换为x y z 语言，进行 形式化验证。对u m l 状态图的形式化研究主要引入了有线自动机，作为u m l 状态 图和s p i n 之间的桥梁，将复杂的多层u m l 状态图分解为多个子自动机，并且提 出了a t t p 算法，将自动机描述为p r o m e l a 代码。微软的模型检测工具m o p s ，并 且自己实现了工具m c s ，对l i n u x 系统进行了安全属性的分析与验证。将u m l 模 型转换为p e t r i 网模型，再利用p e t r i 网的分析验证技术，可以实现对软件模型 的正确性的验证。并且基于实例对u m l 模型转换为x m i 格式，使用d o ma p i 实现 了u m l 模型向p e t r i 网标识语言p n m l 的自动转换。将模型检测技术应用于安全 协议运行模型的漏洞和缺陷分析，从而突破了安全协议的形式化检测的传统方 法：f s m 建模、p e t r i 网建模、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 创新点和主要工作 本文在研究时序逻辑语言以及模型检测这种形式化方法的基础之上，创新点 主要有以下两个方面： ( 1 ) 提出了基于部分u m l 行为模型的元素转换为扩展层次自动机模型的 方法，然后使用模型检测技术对该扩展层次自动机模型进行验证。 ( 2 )提出了u m l 行为模型元素的扩展层次自动机模型到p r o m e l a 模型的描 青岛人学硕上学位论文 述框架。 在本课题的研究过程中，首先主要研究了模型检测工具s p i n ，s p i n 的输入 语言p r o m e l a ，以及基于s p i n 的模型检测过程。再次，对软件漏洞和基于u m l 模型的模型检测建模技术进行了研究。最后，分析并实现了基于u m l 行为模型的 模型检测实例。 本文主要的研究内容包括以下几个方面，如图0 1 所示。 图1 1 研究内容示意图 ( 1 ) 对u m l 状态图模型到e l l a 模型的转换规则进行了形式化定义，并且基 于该定义，对a t m 工作流程状态图模型到e h a 模型的转换进行了实现。 ( 2 ) 形式化定义了u m i 。行为模型的部分模型元素到e h a 模型的转换舰则。 ( 3 ) 提出了u l d l 行为模型的部分模型元素对应的e h a 模型到p r o m e l a 模型 的转换框架。 ( 4 ) 对软件漏洞中的资源竞争性问题和堆溢出问题进行了分析，使用l t l 公式对其进行了定义。 ( 5 ) 在掌握模型检测工具的基础之上，对s e t 购买过程协议进行了s p i n 模 型检测，将这种理论的应用进行了扩展。 ( 6 ) 实现了哲学家问题的u m l 活动图模型的s p i n 模型检测。 1 4 章节安排 论文正文共分为五章。 4 第一章引言 第一章是软件漏洞及其检测理论的研究。本章主要介绍了软件漏洞的分类， 并且对两类典型的软件漏洞进行了分析。同时，对软件检测方法进行了概括性介 绍，提出了本课题使用的软件漏洞检测方法一基于u m l 的模型检测技术。 第二章是模型检测。介绍了模型检测的理论研究现状及国内外成果。对模型 检测的基本原理、建模方法和搜索算法进行了介绍。模型检测在应用过程中，很 多学者经过研究，开发了多种模型检测工具，本章对其中的几种工具进行了介绍。 其中详细地介绍了课题在研究过程中使用的模型检测工具s p i n 。以及详细地描 述了使用该工具对具体的一个安全协议模型进行部分p r o m e l a 代码实现。在本章 中还介绍了模型检测的基础时序逻辑。对线性时序逻辑( l t l ) 的语义与语 法规范进行了详述。 第三章是基于e l l a 的u m l 行为模型建模研究。本章主要介绍了介绍了u m l 以 及如何将u m l 各种建模机制，提出了使用转换规则建立自动机模型是模型检测的 第一步，因此成为本章研究的重点问题。扩展层次自动机( e h a ) 是广泛使用的 一种建模工具。本章提出了u m l 行为模型的部分元素使用e h a 抽象建模的规则， 以及对u m l 的元素e h a 模型使用p r o m e l a 描述的语法框架。同时，基于实例，对 u m l 状态图转换为e h a 模型的基本过程，为模型检测的下一步工作奠定了基础。 第四章是基于u m l 行为模型的s p i n 检测过程的实验过程描述。本章对哲学 家就餐问题进行了详细地分析，对该问题的u m l 活动图转换为e h a 模型，同时根 据p r o m e l a 转换框架，实现了对模型的描述。同时对部分系统属性进行了l t l 描 述，实现了对该问题的s p i n 验证，并且对该验证结果进行了描述。 第五章是总结与展望。 青岛大学硕l 学位论文 6 第二章软件漏洞及其检测理论 第二章软件漏洞及其检测理论 随着计算机的产生和广泛应用，人们对计算机安全领域的研究也随之进行并 不断地成熟。追溯到上世纪7 0 年代中期，美国南加州大学针对操作系统的安全 缺陷进行研究的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 ) 计划，目的就是增强计算 机操作系统的安全性。后来又有很多学者参与这一领域的研究并不断创新研究成 果，他们的研究分别是：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 的软件漏洞分析以及普渡大学c o a s t 实验室的计算机漏洞研 究。但是，对计算机安全漏洞的定义、分类、特征到目前为止还未形成统一和公 认的结论。 2 1 软件漏洞 2 0 0 9 年5 月1 9 日晚，受暴风影音软件存在的设计缺陷以及免费智能d n s 软 件d n s p o d 的不健壮性影响，黑客通过僵尸网络控制下的d d o s 攻击，致使我国江 苏、安徽、广西、海南、甘肃、浙江等省在内的2 3 个省出现罕见的断网故障， 即“5 1 9 断网事件 。这次事件中，免费软件的后门是问题产生的诱因，d n s 服 务的脆弱性是问题产生的关键。虽然此次事件已经平息，但是人们不得不对软件 及服务的高可靠性要求再次提高了要求。类似该事件的大量安全性攻击行为充分 利用了操作系统和应用软件存在的漏洞，人们对操作系统的漏洞和d n s 应用软件 的漏洞管理产生了质疑n 别。 2 1 1 软件漏洞概述 软件漏洞研究是分析和研究软件脆弱性的基础。对产生软件脆弱性的各种软 件漏洞进行研究，可以加深我们对软件脆弱性的理解，同时基于软件脆弱性的基 本理论，帮助人们更好的解决隐藏的安全隐患，设计和实现高可靠性的复杂软件 系统。 要理解软件脆弱性，就要明确脆弱性的相关术语。 错误：错误是指开发人员在工作过程中的一个拼写错误，对需求说明的误读， 对子程序的错误理解等等n 3 1 。 故障：故障是指不正确的程序和正确的版本之间的差异n 制。 安全缺陷：软件安全缺陷是指有意或是无意地引入系统中的，可能导致违背 系统安全需求的不正确行为的程序或数据n 耵。 漏洞( 脆弱性) ：软件脆弱性是指由软件缺陷的客观存在所形成的一个可以 被攻击者利用的实例6 。 基于刈+ 信息安全与隐私的分析和研究，r i s o s 项目 的研究人员提出了基于 青岛人学硕士学位论文 操作系统的完整性缺陷的软件脆弱性分类方法。 软件脆弱性 l 二01 搡辑：戏操住数选 不m 确豹保护4 q f 确的骏涯不正确的阳步 狰 抟泼 j r毒i ri ，、。 i 扔蝓稼护域 没f i j e 确黼 i l 存消，j 绒 l 选抒锚淡 璃虹现环柱 变换铸诶禽笔镄误 壤分魁锄援 繇f 牲错误颡膨镑溪 l 图2 1 软件漏洞分类 p a 项目u 踟对g c o s 、m u l t i c s 、u n i x 等六个操作系统的1 0 0 多个缺陷进行了 分析，最终将这些缺陷分为4 类( 图2 1 ) 。美国海军研究实验室的l a n d w e h r 等 人提出了基于缺陷的起因、引入的时间( 开发阶段、维护阶段或运行阶段) 、分 布的位置( 软件或硬件) 进行了分类n 们。1 9 9 5 年，c o a s t 实验室的a s l a m 针对 u n i x 操作系统，将引起软件脆弱性的故障分为编码故障和突发故障两大类。对 软件脆弱性的分类，还有很多方法，例如：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 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 ) 漏洞的一种，即 程序先检查对象的某个特性，然后得动作是在假设这些特性一直保持的情况下做 出的，但这时该特性可能不具备了。在有些研究中，该问题称为定时或同步漏洞。 竞争条件漏洞是软件设计过程中经常遇到的问题。通常可以分为两类：在运 行某一个程序过程中，由于程序进程的非原子性，从而存在了非诚实进程插入运 行，从而导致了非诚实主体的非法行为的执行。很多安全分类学称这个问题为“顺 序 或“原子性问题；很多进程对同一共享资源拥有相同的优先权，当多个进 程同时运行相同的程序并且使用该共享资源时，就会造成诚实进程之间的冲突。 很多分类学叫这类问题为“死锁 、“活锁”或“锁失败条件 。 一般来说，进程不是以原子方式运行的，一个进程p 1 的中断可以在另一个 进程p 2 正在执行两条指令之间进行。如果进程p 2 对进程p 1 的中断行为没有适 当的处理措施，那么程序的执行就会产生安全问题。 竞争条件漏洞的发生要具备两个条件乜。第一，有两个或更多的事件发生， 并且这些事件的发生存在一定的时间间隔。两个事件问有一定的关系，即：其它 第二章软件漏洞及其检测理论 的事件的执行依赖于其中的一个或几个事件。第二，攻击者能够改变这些事件执 行所依赖的假设，也就是所依赖事件产生的结果。 ( 2 ) 堆溢出 由于c 语言不检查边界溢出问题，使得很多程序存在设计漏洞。其中最典型 的是内存溢出问题。内存区分为存放动态数据的堆区、静念数据的堆区和存放程 序调用的栈区。将堆区溢出问题抽象为对两个动态数组变量进行操作时造成的数 组长度越界问题。 2 2 软件漏洞的检测方法 正是由于软件的漏洞会给人们带来不可挽回的损失和后果，对于软件生产商 和用户来说，都非常注重对软件漏洞的检测，这就使得软件漏洞检测方法有了长 足的发展。软件漏洞的检测方法有很多，主流有基于数据流和控制流的分析方法； 有基于白盒测试和自动化工具的代码检测堙刳；而对于商业软件来说，主要采取黑 盒测试的方法。 从检测过程角度来看，可以分为静态检测和动态检测，两者的区别主要在于 是否执行待测试的软件。静态分析主要采用自动化的检测工具对源代码进行检 测，使用一个“钩子函数”调用用户自定义的属性函数，并通过分析函数来判断 该属性函数是否满足特定的约束条件。这种方法的具有速度快，不需要实际运行 软件的优点。但同时，由于“钩子函数”的算法和效率直接影响到静态测试的准 确性，所以，往往也会带来诸如不能发现漏洞的完整性、误判以及对漏洞描述不 足等缺点。而对于动态检测方法，基本上都是通过在代码中注入标记，并在实际 运行软件时记录这些标记，从而发现软件是否按照原定的路径执行。这种方法的 检测准确率非常高，但是大部分时间会用在处理这些标记信息上，因此效率不高。 目前利用自动化方法检测软件漏洞主要有两类方法，类是基于黑盒测试原 理，另一类是使用编译技术，对软件的源代码进行扫描测试。 第一类方法主要是针对软件接口而不是针对软件的实现进行的测试。在测试 过程中，测试者要给出大量的测试片j 例。如果针对某一类测试用例，该软件出现 异常情况，例如软件崩溃或者软件：异常。就可以说明，该软件针对某类测试用例 可以触发软件漏洞。 第二类方法主要是对软件的源代码进行扫描并且埘软件函数的使用进行检 查。因此该类方法只能对丌源软件进行检测，对非开源的软件就没有办法了。 模型检测技术在硬件应用领域的应用已经相当成熟，然而在软件领域该技术 正处在研究阶段心3 儿2 4 1 。 9 青岛大学硕十学位论文 二一j 图2 2 针对源码的模型检测 模型检测技术同样可以应用到对源代码进行检测过程中。如图2 2 所示，对 软件产品的源码进行检测时，首先要通过模型生成器将源码转换为有穷自动机， 同时将要检测的安全属性描述并转换为下推自动机。其次，将这两个自动机模型 带入模型检测器中进行检测，模型检测器会将检测结果自动输出。 人们不能已知所有的软件漏洞，然而可以利用现有的安全属性库中的安全属 性模型对软件产品进行检测。其中，对l i n u x 操作系统的开源源码进行模型检测 是现在学者研究的重点内容。一些针对l i n u x 操作系统的安全属性包括比印诸如系 统的访问控制；对文件进行写入操作时，调用f o p e n 函数打开或新建一个文件后， 必须先上锁才能进行下一步的操作等等。 部分研究人员正在研究模型检测技术应用于软件漏洞自动挖掘。模型检测技 术的漏洞挖掘方法具有很多优点：不必运行被测系统，速度很快；能做到完全自 动化；无需用户输入；能够保证漏洞发现的完全性。一般情况下，应用于软件的 模型检测技术可以分为对软件开发初期的设计模型进行的模型检测和针对源代 码的模型检测。 目前，针对源代码的模型检测工具原型主要是m o p s 啪1 。该工具主要由加州 大学伯克利分校博士研究生h a oc h e n 完成，适用对象是采用c 语言编写的程序 源代码，它基于控制流分析，实现了对百万行c 代码的分析，其中包括了对完整 版本的l i n u x 9 的代码分析，找到了多个以前未知的安全漏洞。 、 针对软件开发初期的模型检测技术主要是基于u m l 模型的检测。很多学者将 u m i 模型转化为p e t r i 网模型，再利用p e t r i 网的分析验证技术，实现对软件模 型的正确性验证。还有学者的研究过程是将u m l 模型的x m i 格式进行解析，然后 使用d o ma p i 实现了u m l 模型向p e t r i 网标识语言p n m l 的自动转换。 本课题在经过分析研究之后，选择了将u m l 模型转换为自动机模型，然后使 用s p i n 工具对该自动机模型进行建模、规约和验证。从而实现了对软件模型的 正确性验证。 l o 第三章模型榆测理论及s p i n 第三章模型检测理论及s p i n 3 1 模型检测概述 模型检测是形式化验证方法之一。近几十年中，模型检测理论得到了不断地 完善和发展，同时基于该理论的模型检测技术也越来越多的在实际应用中取得巨 大的成果。许多世界著名大公司如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 等纷纷在其产品设计和开发过程中使用模型检测技 术，并在许多复杂的实例研究中发挥了重要的作用。 模型检测是对实际系统抽象为有限状态模型后，对其进行穷尽搜索，判断该 有穷状态模型是否满足待测属性，如果不满足则给出反例。当系统的有限状态模 型确定后，逐个或组合使用属性集中的约束条件，验证系统描述的行为是否能够 达到所预想的状态。 区醒叵堕 # 一i j 、m 是否满足v 一，7 7 l 二二一j v 否 l + ，j 图3 1 模型检测的基本原理 模型检测过程也就是建模、规约和验证的过程。如图3 1 所示。 建模：其中有限状态模型m 使用自动机( 包括扩展自动机e f a 、b u c h i 自动 机、t 1 m e d 自动机) 、p e t r i 网( 包括位置迁移p e t r i 嘲和高级p e t r i 网) 或者 s t a t e c h a r t s 等工具进行描述。属性集的公式使用时序逻辑语言描述，根据当 前时刻的可能未来时刻是否足线性的，可分为线性时态逻辑i ，t i 。和计算树时态逻 辑c t l 。 规约：一个时念逻辑公式可以转换为一个等价的自动机，v a r d i 和w o l p e r 于1 9 8 6 年实现了将时态逻辑检测转变为自动机模型检测，从而把这两种方法关 联起来。自动机模型检测分别将系统和属性表示成自动机，然后去检测系统自动 机所接受的语言足否包含丁属性白动机接受的语言。时态逻辑模型检测则足将系 青岛大学硕士学位论文 统抽象为位置迁移系统s ，表示系统的行为，鼠是初始状态集( rcs ) ，用模 态时序逻辑公式f 刻画系统的性质，通过计算找到s 中所有满足，的状态组成 的集合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 t l 的标 记算法，这个基础算法在模型验证和模型检测领域得到了广泛的应用，尤其是在 计算机硬件系统模型的验证和检测方面。另一种基本的模型检测算法是 f i x p o i n t 算法乜引。很多学者，结合模型检测算法，实现了对多个问题领域的自 动模型检测，并且研发了多种模型检测工具。 模型检测在建筑、工程、计算机硬件等领域应用了很多年，但在软件领域的 应用却是近几年才有了突破，原因是存在状态空间爆炸问题，这个问题成为制约 模型检测的瓶颈，也是研究模型检测的前沿问题。近几年来，针对状态空间爆炸 问题的研究，有了突破性进展，主要的解决方法有：二叉决策图( b d d ) 和符号 模型检测( s m c ) 、o n - t h e - f l y 技术、抽象技术、偏序规约、组合推理和对称检 测等。论文只介绍其中几种重要的技术。 二叉决策图( b d d ) 是一种有根无环图，它由b r y a n t 首先提出，用来存储布 尔表达式，该技术极大地减少了存储布尔公式所需要的空间，使模型检测工业应 用成为可能。它主要用于描述节点的偏序关系，并在此基础之上，使用对图的基 本操作来实现对布尔函数的操作。 符号模型检测( s m c ) 由m c m i l l a n 提出，其主要思想是状态集相关的属性表 示成集合，也就是状态的合并，使用布尔表达式刻画这些属性，再用b d d 在计算 机内实现这些布尔公式及其运算，该方法可以把验证规模提高到若干数量级，有 些情况设置可以达到l o “”，并丌发出工具s m v 。 o n - t h e - f l y 技术是在需要某些状态时，才将其路径展丌，从而避免了状态 的预先生成。该方法很适合深度优先遍历搜索状态空l 日j 的模型检测算法。 抽象技术是除符号模型外，解决空问状念爆炸问题最有效的方法。抽象技术 是状态合并，为了压缩状态空间，它通过消除一些不影响规范的变量状态，得到 简化的自动机模型，通过验证简化模型的性质来降低模型检测的复杂性。文献瞳町 对抽象技术进行了深入的研究，提出了多种抽象方法：数据抽象、基于抽象解释 的抽象、谓词抽象、基于反例的抽象求精。d 时将这些方法与t l e n z i n g e r 提出的 懒惰抽象技术做了比较。 1 2 第三章模型柃测理论及s p i n 对称检测技术最早应用在高级p e t r i 网，主要是用在有色p e t r i 网中。它和 标记算法相同都是用来创建有限状态的可达树。这种思想被扩展应用在了位置 迁移系统中，用于对模型进行死锁侦测和活性的检测。文献啪，中提出该技术采用 了离散数学的群论知识，在自同构的群中，通过求解商集获得o u o t i e n tk r i p l e 结构，并且可以结合o n - t h e - f l y 等多种关键技术相结合，同时文中提出了怎样 在弱对称系统中使用了对称技术。该技术成为研究状态爆炸问题的有效方法。 3 2 模型检测工具 模型检测理论的不断成熟，依赖于国内外学者的深入研究。同时，模型检测 工具使得该理论与实际相结合，在不断解决实际应用问题中完善和解决该理论中 存在的问题。模型检测工具主要有以下几种： ( 1 ) 符号化模型检测工具s m v ，可以解决状态空间爆炸问题。s m v 的输入时 k r i p k e 结构，并且使用c t l 语言对系统属性进行定义。它成功地发现了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 标准8 9 6 卜1 9 9 1 ) 中描述的c a c h e 一致性协议中的 错误，这也是使用自动验证工具首次发现i e e e 标准的错误。国际上符号化模型 检测工具还有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 是微软开发的基于c 语言的模型检测工具包，已经成功应用于验 证w i n d o w s x p 中的一些驱动程序的接口的正确性。 ( 3 ) j a v a p a t h f i n d e r ( j p f ) 是美国国家航空航天局开发的针对j a v a 语言的 验证工具。j p f 已经应用于多个实际系统，取得了很好的效果。 ( 4 ) 还有几种基于抽象技术解决状态爆炸问题的模型检测工具。b l a s t 是 加州大学伯克莱分校丌发的针对c 程序的软件模型检测工具。m a g i c 是卡内基梅 隆大学开发的针