没有合适的资源?快使用搜索试试~ 我知道了~
DeSpec:Windows NT内核驱动程序环境的模型检查与验证研究
理论计算机科学电子笔记203(2009)55-69www.elsevier.com/locate/entcsDeSpec:建模Windows驱动程序环境1Tomas Matousek2布拉格查尔斯大学分布式系统研究小组布拉格,捷克共和国Pavel Jezek3布拉格查尔斯大学分布式系统研究小组布拉格,捷克共和国摘要本文介绍了一种新的面向对象的规范和建模语言DeSpec。该语言主要针对Windows NT内核驱动程序环境中的模型检查。它集成了Zing建模语言的大部分功能,并增加了在不同细节级别定义环境的参数化抽象的方法。DeSpec语言还能够以量化的时序逻辑模式的形式捕获Windows内核对驱动程序施加的约束-保留字:规范语言,验证,模型检查,Windows内核驱动程序1介绍近年来,验证Windows内核驱动程序正确性的工作已经出现,因为它对整个操作系统的稳定性至关重要。微软自己已经开发了几个驱动程序验证工具,包括最新的静态驱动程序验证器模型检查器。模型检测方法在这一领域成功应用的关键是环境模型的合理选择然而,当前工具中使用的环境模型太(1)不确定性,降低了模型检查器报告的精确性,以及(2)过度简化,失去了1这项工作得到捷克科学院项目1 ET 400300504和捷克共和国赠款机构项目GD 201/05/H 014的部分支持。2电子邮件地址:matousek@nenya.ms.mff.cuni.cz3电子邮件地址:jezek@nenya.ms.mff.cuni.cz1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2009.03.02656T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55检查驱动程序的更具体的属性。另一方面,这些模型既没有提供可用于文档目的的正式或可读的规范。本文通过引入一种新的语言来对内核驱动程序及其环境进行形式化规范和建模,从而请注意,由于篇幅限制,本文仅摘录了语言功能的一小完整的语言规范,其功能的详细阐述以及Windows环境的大样本规范可以在[15]中找到。1.1模型检测模型检测技术是一种基于对程序模型状态空间进行彻底检查的形式化验证方法。该模型反映与被验证的属性相关的程序行为。理想情况下,它应该保留软件中可能影响财产的任何部分,以便验证是合理和完整的。另一方面,模型应该尽可能简单,因为模型检查器必须探索所有可能的状态。验证的时间和空间需求随着模型中使用的操作、线程和变量的数量呈指数级增长(状态爆炸问题[17])。通常,目标不是对整个系统进行模型检查。相反,系统被分成两部分环境被认为是正确的,其提供和要求的接口由规范定义。验证工具预计将从模块的源代码中提取部分模型,并根据规范通过包括环境的行为模型来传递给模型检查器的结果模型捕获模块与环境的交互,该环境从程序源代码中提取模型的过程是一项艰巨的任务,因为源代码语言本身可能会引发重大问题。一个C语言提取器需要理解指针、数组、联合、重新解释类型转换等构造从C源代码中提取模型的所有问题已经在不同的论文中提出[16]。本文重点介绍了环境的形式化描述,结合了对模块的要求和环境提供的功能建模。时间逻辑(E。G. 线性时序逻辑(Linear Temporal Logic,LTL)[14]通常用于前者。它们定义了系统的属性如何使用随时间变量量化的谓词随时间变化然而,通过简单的时态逻辑来指定实际应用程序的属性有一个明显的缺点。对于大多数驱动程序员来说,这种规范并不容易理解,如果公式变得更复杂,时序逻辑专家也不容易理解。普通逻辑的不可读性驱使人们开发更高级的语言,T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)5557Bandera时序逻辑模式 [9].用这种语言表达的属性被翻译成许多现有验证工具所使用的时态逻辑公式该模式允许在非常简单的英语句子中编写经常使用的时态逻辑公式,例如。G. “P is absent between Q and R” isQ((Q<$R<$QR)<$[P U R])公式。 虽然不完整的模式是足以指定广泛使用的属性。此外,如果需要的话,可以将额外的模式添加到库中在我们的工作中,我们使用Zing建模语言[1,24]作为环境行为规范的基础Zing语言和Zing模型检查器是由微软研究小组开发的。之所以选择Zing,是因为它然而,这项工作背后的大多数想法并不依赖于目标建模语言,并且可以应用于至少提供类、方法、异常、非确定性选择和线程的任何其他建模语言。满足这些标准的另一种建模语言应该是Bandera中间表示(BIR)的新版本1.2检查Windows驱动程序Windows内核驱动程序是相对较小的库,通常用C语言编写。它们以特权模式运行,使它们能够直接与硬件一起工作。如果驱动程序包含错误,这会带来损坏内核其他部分的高风险。因此,驱动程序的正确性对于操作系统的安全性和稳定性至关重要,驱动程序是软件验证的常见主题。驱动程序可以被看作是放入由内核和其他驱动程序组成的环境中的组件由于驱动程序通常只通过内核函数调用相互通信,因此将其他驱动程序包含到环境中是一种可以接受的简化。由于Windows内核的源代码通常不可用,因此验证器负责开放系统验证。即使它是,由于其固有的复杂性,提取和验证内核模型几乎是不可能的。此外,驱动程序应该只依赖公共文档功能。因此,模型提取器应该只与内核规范一起工作然而,这种规范目前还没有以一种可行的形式来驱动模型提取器我们工作的目标是提供一种编写规范的语言,并将其应用于内核API的重要部分。几个工具,验证驱动程序的正确性已经开发了自己的microsoft。其中包括Driver Verifier[18]用于运行时驱动程序验证的工具58T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55Tion,PREfast[19]静态分析工具,基于驱动程序函数的本地分析,最后是静态驱动程序验证器(SDV)[20](仍在开发中),基于整个驱动程序的静态分析和模型检查技术。静态驱动程序验证器(SDV)用C语言对内核环境进行建模,其中包含特殊的函数和宏,这些函数和宏处理模拟各种执行路径所需的非确定性驱动程序可以被验证的规则是用接口检查规范语言(SLIC)编写的[2]。在SLIC语言中表达规则需要编写C伪代码片段,并定义环境模型应该如何被它们插装。将得到的插装代码转换为抽象布尔程序,并将其传递给模型检查器。从插装代码中提取的第一个布尔程序从所有局部变量中抽象出来,并用非确定性选择替换所有条件。然后,模型检查器会发现错误跟踪,并通过符号执行与原始程序进行比较。如果错误跟踪描述了实际上不可行的执行,则布尔程序在执行跟踪时被细化为更具体的变量。细化后的程序被传递回模型检查器。这个错误搜索和模型专门化的过程会环境模型和SLIC语言允许针对在单个设备对象(表示驱动程序中的设备的对象)上顺序执行的操作来SLIC规则仅限于安全属性,因此不可能对DDK中定义的所有规则进行编码。这些规则是从内核环境中单独指定的,这使得它们不那么重要。无法对多线程环境进行建模以及同时在多个设备对象上工作,在这项工作中,我们介绍了一个解决方案,没有这些缺点。1.3论文投稿这项工作的目的是使以正式但可理解的形式指定和建模内核环境成为可能,这不仅可以用于内核API的精确文档,而且首先可以作为模型提取器的输入,该模型提取器可以产生Windows驱动程序的可验证并发模型。为此,本文介绍了一种新的驱动程 序 环 境 规 范 语 言 ( Driver Environment Specification Language , 简 称DeSpec)。如[15]所示,该语言能够捕获DDK强加给驱动程序的规则的重要子集,包括那些难以或不可能用SLIC语言表达的规则,因此目前无法通过SDV验证论文的其余部分安排如下。第2节从驱动程序验证的角度简要描述了Win-10内核环境。第3节介绍了DeSpec语言,解释了它在一个例子中的部分,并描述了模型提取器应该如何与DeSpec规范一起工作。第4节讨论了相关工作,第5节结束。T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55592Windows内核环境Windows内核执行程序由几个管理各种系统资源的组件组成管理者为执行者的其他部分和司机提供服务。I/O管理器、即插即用管理器和电源管理器是驱动程序验证中最有趣的,请注意,这项工作仅限于遵循Windows驱动程序模型(WDM)的驱动程序[26]。这些驱动程序必须实现即插即用和电源管理功能。I/O管理器加载和卸载驱动程序,并对它们发出I/O请求。驱动程序由I/O管理器直接控制,I/O管理器以I/O请求数据包(IRP)的形式发出I/O请求。如果驱动程序可以完成请求,它将填充为输出参数保留的数据包中的一个位置,并将数据包传递回管理器。如果它其他管理器通过I/O管理器向驱动程序发出请求和通知。例如,即插即用管理器跟踪设备状态转换(设备移除、停止、启动等)。电源管理器监视机器的电源状态(是否进入睡眠、唤醒等)。这两个管理器通过向驱动程序发送各自的IRP来适当地通知驱动程序。每个驱动程序都必须正确响应任意请求和数据包的内容。它可以返回一个指示错误的结果,但它绝不能崩溃或损坏内核的其他部分。驱动程序不能对层次结构中高于或低于它的驱动程序做出任何假设。此要求允许验证工具隔离驱动程序,并在I/O Manager和更高/更低级别驱动程序的任意输入和输出上对其进行测试。3驱动程序环境规范语言3.1概述驱动程序环境规范语言(DeSpec)是一种面向对象的规范和建模语言,结合了Zing建模语言[1]的大部分功能,并结合了受Spec#语言[3]和Bandera时序逻辑模式[9]启发的契约式设计元素它旨在指导从Windows内核驱动程序源代码中提取Zing模型DeSpec语言允许对I/O管理器的行为进行建模,对内核函数的行为进行建模,并指定驱动程序在调用这些函数时应遵守的约束和规则。模型和抽象可以在不同的细节层次上定义,作为对抗状态空间爆炸问题的解决方案之一,这使得模型提取器能够推断出足以验证特定规则的最小DeSpec语言提供了捕获驱动程序与其环境之间交互的基本元素的方法(即,e.全局变量、函数和数据结构60T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55tures)。它被设计为C语言的构造和Zing语言中特别是指针、函数指针、联合和其他在Zing语言中不能直接表达的结构的模型隐藏在DeSpec语言的语法后面。这允许调整这些特征的模型,而无需重写规范。显然,一些利用内存布局的构造(如重新解释强制转换或联合)无法以可行的方式进行建模因此,它们不能直接用DeSpec语言表达。幸运的是,驱动程序和环境接口应该尽可能独立于平台,因此这些结构应该很少使用。3.2质量标准结构DeSpec语言在语法结构上类似于C#语言。每个源文件都包含一个按名称空间分组的声明列表声明包括类、整数枚举、整数范围、方法委托和方法组。类声明由其成员组成。除了标准面向对象语言中常见的字段和方法之外,DeSpec类还可以包含规则。规则通过时序逻辑模式指定对字段和方法的约束。本节简要介绍DeSpec名称空间、类和规则。3.2.1命名空间命名空间定义了内核函数和结构的抽象范围。当模型提取器搜索驱动程序源代码中使用的内核函数或结构的抽象命名空间的选择取决于要验证的约束。默认(全局)命名空间描述了内核函数和结构的最小模型。其他命名空间通常会细化默认模型-使得验证无法通过默认模型表达的约束变得更加复杂。约束作为方法前提、后置条件、类型约束、规则等嵌入到规范中。通过选择要验证的约束,指定包含的名称空间供提取器搜索。通过细节级别区分规格的能力对于减小最终模型的大小很重要。3.2.2类虽然Windows内核是用C语言编写的,但它的设计是面向对象的。通常,表示内核中对象的结构(例如,G.信号量、互斥量或设备)与使用它的函数一起提供。这些函数的行为类似于结构(对象)的方法,因为它们都将指向结构的指针作为它们的参数之一(“this”引用)。继承的概念也出现在几个地方。继承用于在表示不同但相关的对象的结构这种共享在技术上是在相关结构中声明共同的初始场T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)5561这些观察结果证明引入类作为规范的主要元素是合理的-提供给驱动程序的内核结构在DeSpec中被建模为类。绑定到这些结构的函数被声明为类实例方法。未绑定到任何实例的函数映射到静态方法。引用该方法正在处理的实例的形参由instance关键字指定。抽象内核函数的方法(无论是静态还是实例)必须与内核函数同名,并且同一命名空间中的其他方法不能同名(即使在另一个类中声明)。此规则允许模型提取器找到其调用已在源代码中观察到的函数的规范。下面是一个类规范的示例例1.classDEVICE_OBLOG {NTSTATUSIoAttachDevice(instance,_,outDEVICE_OBSTANDARD attachedTo)需要!驱动程序。最低;{NTSTATUS状态 =选择{NTSTATUS.STATUS_SUCCESS,NTSTATUS.STATUS_INVALID_PARAMETER,NTSTATUS.STATUS_OBSERVED_TYPE_MISMATCH,NTSTATUS.STATUS_OBSERVED_NAME_INVALID,NTSTATUS.STATUS_INSUFICIENT_RESOURCES};attachedTo= IsSuccessful(status)?Driver.LowerDevice: null;返回状态;}DEVICE_OBSTANDARD IoAttachDeviceToDeviceStack(instance,_)需要!驱动程序。最低;{return(choose(bool))?Driver.LowerDevice: null;}void setPoint();/* 更多成员关注 */}在示例1中,DEVICE OBSIDE类抽象了同名的结构。结构的图表示驱动程序正在使用的设备。IoAttachDevice和IoAttachDeviceToDeviceStack内核函数都将设备对象附加到设备对象链的顶部直接下部装置62T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55对 象 ( 实 例 附 加 到 的 对 象 ) 分 别 在 attachedTo 输 出 参 数 和 返 回 值 中IoDetachDevice简单地从该设备对象实例4分离直接的更高级别设备。抽象内核函数的方法的签名定义了如何在规范中处理函数的参数占位符标记(单个下划线)用于对指定不重要的参数。IoAttach-函数的模型不关心第二个参数。当指定引用IoAttachDevice方法时,在实际参数列表中仅声明一个参数。实例参数是从参数列表中选取的,位于方法之前,使用点表示法表示目标实例。占位符位置上的参数在实际参数列表中也被省略在示例1中声明的方法如下:device.IoAttachDevice(out lower_device)device.IoAttachDeviceToDeviceStack()lower_device.IoDetachDevice()out关键字指定该参数是一个输出参数,并且必须在方法体中赋值。输出参数通过附加的间接层映射到C语言。因此,参数的C类型是DEVICE OBJECT**。ref关键字还支持标记通过引用传入和传出的参数签名后面可能有一个空的前置条件和后置条件列表。语法类似于Spec#语言中使用的语法-条件分别由requires和ensure关键字引入。该条件是一个布尔表达式,对术语有一些限制。例1中所述的条件要求最低级别的驱动程序不调用IoAttach-函数。在生成方法主体使用Zing语法定义方法行为的模型,该语法富含额外的构造,当生成结果模型时,这些构造被转换为Zing。在示例1中,使用了Zing选择运算符的扩展形式类型NTSTATUS是一个整数枚举,抽象了同名的内核类型。运算符IsSuccessful确定值是否为成功值它的类型由内核识别。如果建模的函数在当前抽象级别上不做任何影响驱动程序的事情,并且只有它的调用是重要的,那么主体也可以完全省略。如果一个内核函数向调用者返回一些值(通过返回值或输出参数),抛出一个异常或有一些副作用,那么指定方法应该有一个对这些操作进行建模的主体。由于DeSpec类通常是公共内核结构的抽象,它可能包含与结构的字段相对应的字段。存储辅助数据可能需要与实际字段不对应的附加字段4注意设备对象的相反角色--较高级别的设备对象正在连接,而较低级别的设备对象正在连接级别设备对象正在分离。T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)5563仅用于建模的唯一目的这些字段由synthetic关键字标记类似地,合成方法和合成类也可以在规范中定义。一般来说,DeSpec将合成语言元素与非合成语言元素区分开来。请注意,第一个例子中使用的所有元素都是非合成的。合成类不包含抽象,特别是没有内核函数映射到合成类的方法。包含合成属性的类示例如下:实施例2.static class Driver {syntheticDEVICE_OBSERVED LowerDevice = new DEVICE_OBSERVED;[ModelParam]const bool IsLowest= false;/* 更多成员关注 */}在示例2中,在静态类中定义了两个合成字段。 第一个一个是LowerDevice,用作当前驱动程序的所有设备都连接到的虚拟设备对象。该模型可以从精确的设备对象链中抽象出来类似的简化是必要的,以减少生成的模型的大小。名为IsLowest的第二个字段是一个字面常量字段,用于定义驱动程序是否是驱动程序链中的最低级别驱动程序。字段由ModelParam属性注释,这意味着其初始值应由用户在模型提取之前设置。当模型依赖于难以从驱动程序的源代码自动推断的属性时,使用模型参数化它也可以用于模型大小调整。3.2.3规则另一个可以出现在类中的成员是规则。该规则是一个量化的时序逻辑模式列表[9],模式参数用布尔表达式填充。实施例3.classDEVICE_OBLOG {/* 省略了示例1中的方法声明 */所有静态规则(DEVICE_OBSIDATE设备){_.IoAttachDevice(out device)::成功||64T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55(装置===_.IoAttachDeviceToDeviceStack())&&设备!= null}对应于{device.IoDetachDevice()}全球范围内;}例3中的规则是一个单一的模式,但是,一般来说,规则是一个列表由逗号分隔并以分号结尾的量化时态逻辑模式。所呈现的规则具有以下含义:本节的其余部分将更详细地解释这些模式每个时态逻辑模式由模式关键字和模式表达式组成。示例3中使用的模式可以被推广为{P}全局对应于{Q},其中P和Q是布尔表达式。每个模式都可以分为两部分:属性和作用域。在这种情况下,属性{P}对应于{Q},范围是全局的。 可用的阵列属性列表如下:(i) {Q}是通用的(ii) {Q}不存在(iii) {Q}存在(iv) {Q}在{R}(v) {Q}导致{R}(vi) {R}响应{Q}(vii) {Q}对应于{R}[9][10][11][12][13] [14][15][16][17][19]性质(v)和(vi)是等价的,这取决于哪一个更适合使用的情况性质(vii)等同于性质(v)和性质(iv)的结合,即,e.到{Q}导致{R}{Q}在{R}之前。它是在组合在内核环境中经常使用,单独编写这两种模式会很不方便。可用范围包括:(i) 全球(ii) {S}之前(iii) {P}之后(iv) 在{P}之后直到{S}(v) 在{P}和{S}之间每个属性和范围的含义是显而易见的。详细的定义可以在[9]中找到,以及等价的LTL公式。LTL公式T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)5565方法事件操作符E. E.M(args)::已输入在输入指定参数M后返回true,直到M返回。返回值被忽略。M(args)M(args)::已返回在使用指定参数d调用M并返回任意值后变为true,直到再次输入M并返回 同样的论点。M(args)::成功在M被指定参数d调用并成功返回值后变为true,直到M再次输入相同的参数。M(args)::失败在使用指定参数d调用M后变为true,返回值不成功,直到输入M同样的论点。expr = M(args)expr!== M(args)在使用指定参数nd调用M后变为true,返回值(un)等于expr直到M再次输入相同的参数。表1方法的源代码事件操作符。M代表非合成方法,args代表参数列表(可能为空),expr表示表达式。具有全局作用域的Q对应于R模式是Q(Q<$QR)<$[R W Q] 5.时间模式可以通过值类型或引用类型进行量化。实例规则的概率由声明类型的变量隐式量化。实例规则可以使用此关键字引用该变量。当引用类型的实例成员时,可 以 省 略 此 关 键 字 。 与 Bandera [8] 不 同 , DeSpec 允 许 量 化 值 类 型 ( 即 。 e.integers、Boolean、布尔运算)。Zing符号值类型可用于实现。引用类型量化可以以与Bandera中相同的方式实现,但是使用Zing符号引用类型可以实现更大的可扩展性,这应该在Zing的下一个版本中可用。包括模式参数的布尔表达式应该通过源代码事件操作符来引用所谓的源代码事件。源代码事件是指特定代码段的执行。DeSpec允许指定对应于函数调用的事件和字段上的操作(读和写),5Q是普适的时间量化器(总是在未来),Q是存在的时间量化器(在未来的某个时候),[W W]是弱的直到算子(要么是“W”永远不成立,“W”总是成立,要么是“W”在未来的某个时候成立,“W”直到那一刻才成立)。66T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)55场事件运算符E. E.F::read从F读取后返回true。F:书面在F被写入后返回trueexpr= F::getexpr!F::get在读取F并且读取的值等于expr的值之后返回true。expr = F::setexpr!F::set在F被写入且写入的值(不)等于expr的值后返回true。表2场的源代码事件操作符。 F代表非合成域,expr表示表达式。司机的源代码因此,源代码事件操作符仅适用于非合成方法和场。表1和表2列出了可用的源代码事件操作符。在示例3中,由方法(args)::succeededoperator定义的源代码事件为内核函数IoAt- tachDevice的成功返回建立了一个看门狗。它仅由这样的函数返回触发,即第三个参数可以与设备量化变量统一,并且函数返回值意味着成功调用。前两个参数在函数被调用时可以是任意的。每个源代码事件操作符都被相应的谓词替换,以进行规则验证。在模式表达式中使用源代码事件操作符意味着将全局状态变量添加到结果Zing模型中,并使用Zing代码片段对模型进行插装,以进行状态转换。运算符状态变量的值确定LTL公式谓词的值。虽然Zing3.3DeSpec驱动的模型提取模型提取过程的输入是被验证的驱动程序的源代码、内核头文件以及用DeSpec编写的内核函数和数据结构的规范。在开始时,用户应该选择一组他或她想要验证的约束。用户还可以选择用于验证的顶级模型。这个模型也是用DeSpec编写的,作为一个实现预定义方法的类。它的任务是模拟内核对驱动程序的行为,包括驱动程序加载和初始化以及发出I/O请求(IRP)。默认顶层模型是最复杂的模型。它模拟多处理器环境、多设备对象和并发IRP。然而,对于某些规则的验证,一个更简单的模型可能就足够了。DeSpec允许编写和使用这样的模型。的选择T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)5567更简单的模型可以从根本上减少状态空间的大小,并使验证更快,有时甚至允许在实际时间内完成验证。然而,一些错误可能仍未被发现。一旦选择了顶层模型,模型提取器就会生成驱动程序的Zing模型(使用其C源代码和内核头文件),并将其与环境模型相结合。由于生成的模型太大而无法验证,因此切片[13,10]应该只保留顶层模型传递引用的部分和正在验证的约束。作为最终结果,输出驱动程序的Zing模型以及相关的内核函数和结构4相关工作这项工作结合或依赖于模型检查[6,17],模型提取[7,30],时态逻辑[27,14,5],源代码静态分析和切片[13,10]以及Windows内核驱动程序环境[31,26]的思想和方法。特别是,Zing模型检查器[1],Bandera工具集(特别是Bogor模型检查框架[28,29]),Java Path Checklist[25]和SPIN模型检查器 [12,4]是专门用于模型检查的相关工具。SLAM项目[23]致力于C程序的静态分析和验证,特别是Windows内核驱动程序。Microsoft Static Driver Verifier(SDV)工具[20]的测试版最近已经发布,这是该领域的成果由于本文的研究对象是Windows内核驱动程序验证,因此SDV是与之最密切相关的工作。该工具中规则的指定方式将其验证能力限制在安全属性上。SDV使用的环境模型是单线程的,防止了一些竞争条件的验证,并且非常不确定,引入了额外的错误报告。它也没有提供可能用作文档的内核函数的另一方面,SDV是一个功能性工具,其在实践中的应用已经导致在Microsoft自己的驱动程序中发现了几个错误发现驱动程序中的错误并不局限于模型检查技术。MicrosoftPREfast驱动程序工具[19]对源代码进行静态分析,并搜索常见的错误模式。例如,它可以发现由于缺少函数调用、空指针的解引用、缓冲器溢出、在不正确的IRQL级别上调用的内核函数等引起的内存泄漏。分析是函数范围的,因此它引入了假阴性,也限制了它能够检测到的一组错误。Windows操作系统还允许检查驱动程序在压力条件下的工作情况,如内存不足,丢失资源,丢失数据包等。在与内核的合作中,驱动程序验证工具[18]模拟这些条件并对指定的驱动程序运行测试。 该工具能够检测到许多错误,但它68T. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)555结论和今后的工作本文介绍了DeSpec语言-一种语言的表达性和适用性在[15]的内核功能中得到了证明这项工作还表明,如果没有对Windows内核更深入的理解,内核环境的可用文档[21]对于其正式规范是不够由于DeSpec语言旨在由模型检查工具使用,因此它解决了这种验证方法的主要问题-状态爆炸问题。根据所验证的属性,抽象的详细程度可能会有所不同。模型的复杂性可以通过用户指定的模型参数进一步调整。通过设置这些参数,用户可以了解提取的模型有多用户还可以通过选择适当的顶层模型来选择测试的驱动程序功能的子集。仅使用断言来验证具有有限迹语义的LTL公式的可能性(参见[11])引起了一个问题,即使用时态规则是否带来了显式断言之外的新东西。虽然许多规则可以等效地手动验证,但i. e.通过在函数的模型代码中的正确位置添加断言(或方法契约),使用规则具有一些优势。这一地理位置暗示了几个优势。如果规则的整个“业务逻辑”都写在一个地方,那么它更容易维护,可读性更强,并且规则的验证可以更容易地选择(取消)进行验证。此外,当规则更复杂时,手动跟踪代码中影响已验证属性的所有操作并不容易。另一方面,有些规则过于复杂,难以编写或理解,因此最好通过显式断言手动实现它们。本文提出的设想目前正在实施。该实现包括DeSpec语言分析器和模型提取器,该模型提取器消耗C源代码并产生由DeSpec规范驱动的Zing模型。引用[1] Andrews,T.,Qadeer,S.,Rajamani,S. K.,J.,谢燕:一种并行软件的模型检测器,技术报告,微软研究院,2004年。[2] 鲍尔·T Rajamani,S. K.: SLIC:接口检查的规范语言,技术报告,MSR-TR-2001-21,Microsoft Research,2002年[3] Barnett,M.,Leino,K. R. M.,Schulte,W.:Spec# Programming System - An Overview,MicrosoftResearch,2004年[4] 贝尔实验室:SPIN模型检查器,http://spinroot.comT. Matousek,P.Jezek/Electronic Notes in Theoretical Computer Science 203(2009)5569[5] Clarke,E. M.,Emerson,E.一、Sistla,A. P.:使用时序逻辑规范自动验证有限状态并发系统,ACM编程语言系统汇刊,244-263,1986年[6] Clarke,E. M.,Grumberg,O.,Peled,D.答:模型检验,MIT出版社,2000年。[7] Corbett,J. C.,Dwyer,M. B、Hatterygal,J.,Laubach,S.,帕萨雷亚努角美国,Robby,Zheng,H.:Bandera:Extracting Java Source Code,Proceedings of the International Conference on SoftwareEngineering,2000[8] Corbett,J.C.的方法,Dwyer,M.B、Hatterygal,J.,Robby:表示动态系统的可检查性质Bandera Specification Language,2001年[9] Dwyer, M. B 、 阿 夫 鲁 宁 湾 美 国 , Corbett , J. C.: Patterns in property specifications for finite-stateverification,第21届软件工程国际会议论文集,411-420,1999年[10] Dwyer,M.B、哈特茅斯·J.:模型构造的切片软件,高阶与符号计算杂志,2000年[11]Giannakopoulou D.,Havelund K.:线性时序逻辑规范的分析,RIACS技术报告01.21,2001[12] Holzmann,G. J.:SPIN模型测试:入门和参考手册,Addison-Wesley Professional,2003年[13] Krinke,J.:顺序与并发程序的高级切片,博士论文,Fakultt Fr Mathematik und Informatik,UniversittPassau,2003[14] 兰波特湖:“Sometime” is sometimes “not never” – on the temporal logic of programs, in Proceedings of7th ACM Symposium on Principles of Programming Languages, pages 174-185,[15] Matousek,T.:Windows驱动程 序 环 境 模 型 , 布 拉 格 查 尔 斯 大 学 软 件 工 程 系 硕 士 论 文 , 2005 年 ,http://nenya.ms.mff.cuni.cz/publications/Matousek-thesis.pdf[16] Matousek,T.,Zavoral,F.:从C源代码中提取Zing模型,SOFSEM 2007[17] McMillan,K. L.:符号模型检验1992年,卡内基梅隆[18] 微软:司机验证员,http://www.microsoft.com/whdc/DevTools/tools/DrvVerifier.mspx[19] 微软:Prefast,http://www.microsoft.com/whdc/devtools/tools/PREfast.mspx[20] 微软:静态驾驶员验证器-找到司机虫子在牺牲时间, WHDC,http://www.microsoft.com/whdc/devtools/tools/sdv.mspx[21] 微软:Windows驱动程序开发工具包,WHDC,http://www.microsoft.com/whdc/devtools/d ddk/default. mspx[22] 微软:Windows驱动程序基金会,WHDC,http://www.microsoft.com/whdc/driver/wdf/default.mspx[23] 微软研究院:SLAM项目,http://research.microsoft.com/slam[24] 微软研究院:Zing模型库,http://research.microsoft.com/zing[25] NASA智能系统部:Java路径搜索,http://ase.arc.nasa.gov/havelund/jpf.html[26] Oney,W.:Programming the Microsoft Windows Driver Model,1999,Microsoft Press[27] Pnueli,A.:程序的时序逻辑,第18届IEEE计算机科学基础研讨会,第46-57页,1977年。[28] Robby,Dwyer,M. B、Hatterygal,J.:Bogor:一个可扩展的高度模块化的软件模型检测框架。工程注释28,5,267-276,2003[29] Robby,Dwyer,M. B、Hatterygal,J.:茂物,http://bogor.projects.cis.ksu.edu[30] SAnToS实验室:Bandera项目,http://bandera.projects.cis.ksu.edu[31] Solomon,D.一、Russinovich,M. E.:Inside Microsoft Windows 2000第三版,Microsoft Press,2000年[32] Vardi,M.是的,开放系统的验证,计算机科学讲义,卷1346/1997,Springer。
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功