（计算机应用技术专业论文）虚拟化平台支持的目标码验证技术研究.pdf

浙江大学硕士学位论文 摘要 摘要 当前，随着计算机软件快速发展、软件规模不断扩大，软件的质量越来越得 到重视。为此，人们提出了软件可靠性、软件验证、软件质量保证、软件测试等 一系列概念和理论。如何提高软件的可靠性成为目前软件系统设计与开发的主要 问题之一。软件验证，是软件可靠性的一部分。它对软件功能行为进行验证和确 认，通过一定的合理的行为来观察软件的表现。在高可靠性软件的开发过程中， 软件验证是一个非常重要的组成部分。没有经过验证的高可靠性软件，将会导致 灾难性的后果。 虚拟化技术和虚拟化平台的出现，给软件验证特别是目标码验证带来了方便。 虚拟化平台上软件运行的各种行为，都能被捕捉分析。虚拟化平台下的软件验证， 将成为软件验证新的发展方向。 本文主要针对高可靠性软件的目标码验证技术的研究，例如d o 1 7 8 b 标准中 的目标码验证研究。在分析当前目标码验证面临的困难的基础上，提出了一种在 虚拟化平台上实现目标码验证的方法。 本文对当前的软件验证和目标码验证技术的特点和方法做了介绍和分析，通 过对虚拟化平台的体系结构扩展，将目标码验证技术和虚拟化平台结合在一起。 针对目标码的正确性验证和鲁棒性验证两个方面，在特定的虚拟化平台上，讨论 了在其上面实现目标码验证的难点和设计要点。 最后，在虚拟化平台上实现了一个目标码验证工具b s v v t ( b o c h sb a s e d s o f t w a r ev e r i f i c a t i o na n dv a l i d a t i o nt o o l s ) 。该工具在扩展虚拟化平台体系结构的基 础上，在损失大约4 0 性能的情况下，实现了目标码覆盖检测、分支图生成、分 支反转与提示、故障条件注入和轨迹导出等功能，覆盖了目标码验证的两个方面。 同时，b s v v t 保证了目标码验证中代码的完整性和无侵入性。 关键词：软件验证，目标码验证，虚拟化平台，故障注入 浙江大学硕士学位论文 a b s t r a c t n o w a d a y s w i t ht h er a p i dd e v e l o p m e n to fs o f t w a r ea n dc o n t i n u o u se x p a n s i o no f s o t t w a r es c a l e ，t h eq u a l i t yo fs o t t w a r ei sb e i n gp a i da t t e n t i o nm o r ea n dm o r e t ot h i s e n d ，p e o p l er a i s eas e r i e so fc o n c e p t sa n dt h e o r i e sl i k es o f t w a r er e l i a b i l i t y , s o f t w a r e v e r i f i c a t i o n , s o f t w a r eq u a l i t ya s s u r a n c e ，s o f t w a r et e s t i n ga n de t c h o wt oi m p r o v et h e r e l i a b i l i t yo fs o f t w a r eb e c o m e st h em a j o rp r o b l e mo fs o f t w a r es y s t e md e s i g na n d d e v e l o p m e n t s o f t w a r ev e r i f i c a t i o ni sac o m p o n e n to fs o t t w a r er e l i a b i l i t yw h i c hi sa l l a c t i o no f v e r i f y i n ga n dv a l i d a t i n gf u n c t i o n sa n db e h a v i o r so fs o f t w a r e i to b s e r v e st h e p e r f o r m a n c eo fs o f t w a r et h r o u g hac e r t a i nr e a s o n a b l eb e h a v i o r i nt h ed e v e l o p m e n t p r o c e s so fh i g h - r e l i a b i l i t ys o f t w a r e ，s o f t w a r e v e r i f i c a t i o ni sav e r yi m p o r t a n t c o m p o n e n t h i g h - r e l i a b i l i t ys o f t w a r ew i t h o u tv e r i f i c a t i o nw i l lr e s u l t i nd i s a s t r o u s c o n s e q u e n c e s t h ee m e r g e n c eo ft h ev i r t u a l i z a t i o nt e c h n o l o g ya n dv i r t u a lp l a t f o r m sb r i n gg r e a t c o n v e n i e n c et os o f t w a r ev e r i f i c a t i o n e s p e c i a l l yt h ev e r i f i c a t i o no fo b j e c t c o d e v a r i o u ss o f t w a r er u n t i m eb e h a v i o r so nv i r t u a lp l a t f o r mc a nb ec a u g h tf o ra n a l y z i n g s o f t w a r ev e r i f i c a t i o no nv i r t u a lp l a t f o r mw i l lb et h en e wd i r e c t i o no fs o f t w a r e v e r i f i c a t i o na n dv a l i d a t i o n t h i sp a p e rm a i n l yf o c u s e so nt h er e s e a r c ho fo b j e c tc o d ev e r i f i c a t i o na n d v a l i d a t i o nt e c h n o l o g yi nh i 曲- r e l i a b i l i t ys o f t w a r e ，f o ri n s t a n c e ，t h er e s e a r c ho no b j e c t c o d ev e r i f i c a t i o ni nt h ed o 一17 8 bs t a n d a r d o nt h eb a s i so fa n a l y z i n gt h ed i f f i c u l t i e s w h i c ho b j e c tc o d ev e r i f i c a t i o nm e e t sc u r r e n t l y , am e t h o dw h i c hr e a l i z e so b j e c tc o d e v e r i f i c a t i o no nv i r t u a lp l a t f o r mi sr a i s e d t h i sp a p e rm a k e sa ni n t r o d u c t i o na n da n a l y s i so nt h ec h a r a c t e r sa n dm e t h o d so f c u r r e n tt e c h n o l o g yo fs o f t w a r ev e r i f i c a t i o na n do b j e c tc o d ev e r i f i c a t i o n b ye x p a n d i n g t h ea r c h i t e c t u r eo fv i r t u a lp l a t f o r m ，o b j e c tc o d ev e r i f i c a t i o na n dv i r t u a lp l a t f o r ma r e i n t e g r a t e d a i m i n ga tc o r r e c t n e s sv e r i f i c a t i o na n dr o b u s t n e s sv e r i f i c a t i o no fo b j e c t c o d e ，t h e d i f f i c u l t i e so fr e a l i z i n ga n dt h e k e yp o i n t s o fd e s i g n i n go b j e c tc o d e v e r i f i c a t i o no ns p e c i f i cv i r t u a lp l a t f o r ma r ed i s c u s s e d 浙江大学硕士学位论文 a b s t r a c t a tl a s t , a l lo b j e c tc o d ev e r i f i c a t i o nt o o l b s v v t ( b o c h sb a s e ds o f t w a r e v e r i f i c a t i o na n dv a l i d a t i o nt o o l s ) i si m p l e m e n t e do nv i r t u a lp l a t f o r m o nt h eb a s i so f e x p a n d i n gv i r t u a lp l a t f o r ma r c h i t e c t u r ea n do nt h ec o n d i t i o no fa b o u t4 0 p e r f o r m a n c el o s s ，t h i st o o lr e a l i z e st h et e s to fo b j e c tc o d ec o v e r a g e ，t h eg e n e r a t i o no f b r a n c hg r a p h ，t h er e v e r s ea n dp r o m p to fb r a n c h ，f a u l ti n j e c t i o n ，t r a c ee x p o r ta n de t c w h i c hc o v e r st h et w os i d e so fo b j e c tc o d ev e r i f i c a t i o n m e a n w h i l e ，b s v v tg u a r a n t e e t h ei n t e g r a l i t ya n dn o n - i n c u r s i o no fc o d ew h e nv e r i f y i n go b j e c tc o d e k e y w o r d s ：s o f t w a r ev e r i f i c a t i o n , o b j e c tc o d ev e r i f i c a t i o n , v i r t u a lp l a t f o r m ，f a u l t i 琦e c a o n 浙江大学硕士学位论文图目录 图目录 图2 1b o c h s 体系结构2 2 图2 3b o c h s 调试器断点检查和设置流程2 5 图3 1 验证工具总体框架2 6 图3 2 典型的分支图2 8 图3 3 监控区域形成多跳转地址。3 0 图3 4 函数调用形成多跳转地址。3 l 图4 1 目标码覆盖流程图3 6 图4 2 分支图生成流程。3 7 图4 3 分支反转、分支提示和分支条件修改流程图4 0 图4 - 4 故障注入和轨迹导出流程图4 4 图5 1s r i d e 、b o c h s 和b s v v t 的交互5 1 图5 2 目标码覆盖开销时间5 8 图5 3 分支图和分支反转时间开销5 9 图5 - 4 故障注入时间开销6 0 i v 浙江大学硕士学位论文表目录 表目录 表2 1i e e e 关于软件完整度的4 个级别1 2 表2 2d o 1 7 8 b 对于软件等级的描述1 3 表3 1 基本分支跳转结构图和它对应的代码形式一2 9 表4 1 目标码覆盖实现相关结构。3 7 表4 2 分支图实现相关结构3 8 表4 3 条件跳转指令的修改与新分支添加。3 9 表4 4 分支反转实现相关结构一4 l 表4 5 分支比较内容存储结构4 l 表4 6 分支反转改造一4 3 表4 7 比较指令的改造4 3 表4 8 故障注入相关结构4 5 表4 9 轨迹导出相关结构4 5 表4 1 0 新增指令4 8 表5 1 目标码覆盖输出结果5 2 表5 2 目标码分支图输出结果5 3 表5 3 分支反转后的目标码分支图5 4 表5 - 4 分支反转提示与注入信息5 5 表5 5 故障注入输入和输出结果5 5 表5 - 6 轨迹导出输出内容。5 6 表5 7 目标码验证工具的性能开销比6 1 v 浙江大学研究生学位论文独创性声明 本人声明所呈交的学位论文是本人在导师指导_ i 进行的研究工作及取得的 研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果，也不包含为获得澎姿态堂或其他教育机构的学位或 证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意。 学位论文作者签名：龆壬c 2 签字日期：知舒年多月善日 学位论文版权使用授权书 本学位论文作者完全了解逝姿态堂有权保留并向国家有关部门或机 构送交本论文的复印件和磁盘，允许论文被查阅和借阅。本人授权逝至三盘堂 可以将学位论文的全部或部分内容编入有关数据库进行检索和传播，可以采用影 印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：物孑l z ， 签字日期：扒耐年6 月妒日 导师签名：1 签字日期：o 丫年k 月髫日 浙江大学硕士学位论文第1 章绪论 第1 章绪论 1 1 引言 自从计算机诞生以来，特别是软件工程出现以后，软件作为计算机系统的一 个重要组成部分，越来越变得重要。但是随着软件规模的扩大，软件的“双重效 应 【l 】开始显现。 为此，人们提出了软件可靠性、软件验证、软件质量保证、软件测试等一系 列概念和理论，并将其用于软件工程的各个阶段。然而，计算机硬件的高速发展， 计算机软件的规模扩大，远远超出了理论的发展速度。软件的质量问题，随着时 间的推移，越来越变得重要。 因此在9 0 年代后，国外对软件错误检测、排错技术、故障恢复等可靠性保障 技术研究的投入明显加大。特别是2 0 0 0 年以后，一系列的检测定位b u g 的理论 和工具开始涌现，比如s o b e r t 2 1 、a r g u s t 3 】等。对于一般软件的检测，这些工具取 得了比较好的效果，但是对于高可靠软件，依然不足。 软件验证，作为软件可靠性的一部分，随着高可靠软件的发展越来越得到重 视。软件验证比软件错误的范围更大，它关注于软件的失效问题。i e e e 制定了相 应的标准i e e es t d l 0 1 2 2 0 0 41 4 1 和一些指导i e e es t d l 0 5 9 1 9 9 3 【5 】，用于指导软件 的验证行为。航空航天、汽车、医疗设备等行业，作为高可靠软件的直接使用者， 也提出了自己的标准【6 】【7 】【8 1 ，用于目标码验证。 高可靠性软件验证，是软件验证的一部分。它是对关键的可能会造成灾难性 后果的软件的验证。这些高可靠性软件，一般存在于航天、汽车、能源、医疗设 备等行业。由于高可靠性软件验证的复杂性和专业性，当前对一般软件的可靠性 验证技术，并不能直接应用在高可靠软件验证中。高可靠性软件的验证工具存在 许多不足。特别是对于系统软件的验证、目标码的验证，没有更底层软件的支持、 不允许对代码进行插桩，更多的要依靠验证人员的经验。 浙江大学硕士学位论文第l 章绪论 1 2 软件可靠性概述 1 2 1 软件可靠性的概念 软件可靠性，是软件工程中一个重要的组成部分。软件可靠性的标准定义，是 在一段特定的自然单元或时间间隔内，软件无失效运行的概率【9 】。 在该定义中，软件可靠性的度量是按照自然时间来计算，而不是程序的执行 时间。并且，它注重的是程序运行的功能失效，而不是发生错误。 软件可靠性，是可靠性在软件方面的应用。它满足可靠性的一般性质，也具 有自己独特的特点。软件可靠性，满足可靠性理论：在一段特定的时间内，在一 定的条件下，设备能够执行它想要的功能的概率。它能表达为以下的公式： 尺( f ) = lf ( x ) d x ( 1 1 ) 其中，八x ) 为失败概率密度函数，t 为时间开始点。 作为可靠性，它具有下面四个特点：第一，可靠性是一个概率，它是一个随 机现象。第二，可靠性是基于想要的功能，它和失败没有必然的联系。第三，可 靠性是在一段时间内的可靠性。第四，可靠性是在状态条件下的操作。 软件可靠性的特点和上面略有不同。软件发生失效时，一般是由于软件本身 存在的缺陷造成的，是本身固有的，而不是可靠性中的随机现象。它在一个严格 的条件下可以重复出现，具有规律性。 1 2 2 软件可靠性的作用 软件可靠性，和软件测试有许多重叠的区域。但是，两者的目的有所不同。 后者，一般是为了提高软件质量，尽可能的通过各种测试方法和理论找出潜在的 错误。但是，由于软件是由人编写的，所以在软件中必然会存在一些错误，即使 通过测试，也会留下一些难以检测的错误。 正是为了了解和解决这些遗留下来的错误，软件可靠性出现了。软件可靠性， 是对软件正常运行中，发生失效的概率的研究，通过一定的方法对失效进行建模、 分析。软件可靠性研究，面对的是一个存在失效可能的系统，它分析失效的行为、 2 浙江大学硕士学位论文第l 章绪论 建立合理的备用系统来避免软件失效。 在一些对软件要求很高的行业，软件可靠性的研究尤为重要。这是由于一旦 软件失效，会造成巨大的损失。例如1 9 9 6 年6 月4 号，阿丽亚娜5 型火箭发射 失败，在发射3 7 秒之后，其指导和姿态信息完全丢失。原因就在于重用了阿丽 亚娜4 型火箭中一个模块，从而导致惯性参考系统失效【1 0 1 。又如，在7 0 8 0 年代， 美国、欧洲等地发生多起x 光照射剂量过量的医疗事故，造成了多人死亡，其原 因就是设计的软件有缺陷。 1 2 3 保证可靠性的方法 为了提高软件可靠性，除了采用软件工程、建立标准的质量管理体系等常用 方法外，还需要使用以下一些方法来进一步提高软件的可靠性。 第一个，引入模型化技术。该技术主要是对软件进行建模，尽量避免错误和 缺陷的进入。常用的方法有算法模型化、模拟模型化、可靠性模型【n 】、正确性模 型、软件危险分析与故障树分析【】2 】等。 第二，是采用容错设计技术【1 3 】，和第一个方法不同的是，容错技术更关注于 如何在发生错误的情况下，通过一定的设计避免对软件的功能产生影响。它包括 了恢复块、n 版本编程、分布式恢复块、一致性恢复块等多种方法。 第三，重用已经通过验证的模块。已经验证的模块，具有比较好的可靠性和 正确性。但是在使用时，依然要非常小心，兼容性问题将可能成为一个严重问题。 另外，重用模块中未使用的部分，也有可能造成严重问题，需要被去除。 第四，简单的设计。对于高可靠性软件，设计的越简单，其发生错误的可能 性越小，也就越稳定。 1 3 软件验证概述 1 3 1 软件验证的概念 软件验证，是软件可靠性的一部分，不同于软件测试，它是对软件的功能行 为的一种验证和确认行为。它通过一定的合理的行为，来观察软件的表现。 浙江大学硕士学位论文第l 章绪论 对于软件验证，在英文中有两个相似的词：v e r i f i c a t i o n 和v a l i d a t i o n 。这两个 词在中文中都具有验证的含义，但是又有所区别。v e r i f i c a t i o n 是确认最后的产品 是否实现了指定的需求。它需要在整个软件开发周期内，对开发的各个过程进行 验证和确认。v a l i d a t i o n 是检查产品的设计是否满足最后的功能使用，是一个高层 的检测。 在软件能力成熟度模型( c m m i s wv 1 1 ) 1 4 】中，v a l i d a t i o n 指的是评价软件在 开发或者结束阶段时，它是否满足指定需求的过程。而v e r i f i c a t i o n 是指评价软件 在某一个开发阶段，它是否满足从该阶段开始时提出的条件。 在大部分描述软件验证的标准中，v e r i f i c a t i o n 和v a l i d a t i o n 都是在一起出现， 简称为v & v 。在本文中，采用v & v 作为软件验证的定义，即不严格区分两者的 区别。在下面的描述中，软件验证均按照该含义进行理解。 1 3 2 软件验证的目的 正如软件验证的概念所说的，软件验证是验证和确认软件正开发或者结束阶 段，它的功能是否满足设计和需求的要求。通过软件验证，能够提高软件的正确 性、完整性和可靠性。这就是软件验证的总目的。 软件验证和软件测试有一定的重叠。例如，软件的验证也是需要通过编写一 些测试用例来进行验证。但是，两者的目的和范围各有不同。软件验证，贯穿了 软件工程的始终，在各个阶段，均需要进行软件验证，而软件测试，只是软件工 程中的一个环节，它关注于功能的正常运行，而不是是否符合需求和设计。 软件验证，更多的是一种评审行为，其目的是确认需求、设计和最终代码的 对应关系，即需求和设计能全部在最终代码上反映出来，而最终代码均可以在需 求和设计上找到对应的部分。 因此，软件验证对所有在设计、需求和代码的不一致的地方进行了特别关注。 这些没有一一对应的地方，可能是来自软件自身的缺陷，也有可能是最终代码生 成过程中，编译器、库函数等引入的错误。这些由测试等软件工程行为检测不到 的地方，正是软件验证的发挥作用的地方。 4 浙江大学硕士学位论文第l 章绪论 1 3 3 软件验证的一般方法 软件验证，作为软件可靠性的一部分，和一般的软件工程的测试具有一定的 相似性。但是，由于目的的不同，软件验证更多的是对软件功能、行为的正确性 验证。 从一般的方法来说，软件验证有下面几类验证方法f 1 5 】：传统的手工方法；走 查、观察和复查；正确性证明；模拟。 传统的手工方法 传统的手工方法，是最原始的检查、分析代码程序的方法。但是由于需求的 不断变化、代码的不断改变，手工检查要时刻进行。为了保证正确性，手工检查 要非常小心，可以交给第三方来进行检查。 在软件开发的早期，使用了该方法，这是由于当时的代码数量很少，采用手 工的方法，也可以快速的寻找出错误，或者验证完毕。但是，随着现在软件规模 的越来越大，多个人同时修改程序，代码时时刻刻都在变化。采用手工的方法已 经力不从心，除了一些小规模的程序可以应用外，对于大部分软件，采用手工方 法来进行验证，已经行不通了。 走查、观察和复查 随着软件规模的扩大，走查、观察和复查自然而然出现了。走查和观察，是 比较正式的手工检查。它使得编程者和测试者分离，共同组成一个团队。观察是 对程序一步一步对照需求，检查它是否符合预先定义的标准。而走查，是使用测 试用例，对一个程序手工模拟其流程，最后观察它的输出结果。当然，走查更重 要的目的是，对流程的疑问可以通过询问程序员来发现更多的可能错误。 正确性证明 正确性证明是对软件的正确性从理论上或者设计阶段进行验证。它检查程序 运行的逻辑、程序运行的约束条件是否满足需求。正确性证明，一般发生在程序 设计、需求阶段，和具体的计算机编程语言无关。 形式化方法，是一种描述数学逻辑、进行自动证明的工具。它可以应用在软 件的规格、开发和验证中。在软硬件设计中，使用形式化方法，是因为在其他工 塑垩奎堂堡主兰垡堡奎至! 雯丝笙 程领域中，使用适当的数学分析能够对设计的可靠性和健壮性有帮助1 6 1 。但是， 由于形式化方法的开销非常巨大，它一般只用于高度集成的系统，或者对目标码 进行验证【1 7 1 。 模拟 对于其他方法来说，模拟是最接近真实运行程序行为的测试方法。模拟是一 个可执行的模型，对应于软件的行为，它是一个非常强大的测试方法。 模拟，一般使用在实时系统中。在这些系统中，接口都是和“真实世界 中 的硬件联系在一起。对于非实时系统来说，模拟的开销十分巨大。 在模拟前，可以建立多个模型来预测模拟的结果，对比最后实际结果来验证 软件的正确性。 1 4 国内外发展现状 当前软件可靠性领域中，软件验证技术有了一定的发展。但是和其他的领域 比较，软件验证技术的发展速度无疑是比较慢的。这是由于，软件验证是一个语 义验证和确认的过程，无法采用自动化的方法。一些理论和工具的使用，能提高 一定的效率，但是最终的验证确认，还是需要人工来进行。 在国外，目前已经提出了以下的一些和软件验证相关的标准： _ i e e es t d1 0 1 2 2 0 0 4 标准。该标准是软件验证标准，列举了软件验证过程 中的行为，包括了分析、评估、复查、观察、测试等环节，同时对软件所 在的相关上下文环境进行评估。 i e e es t d1 0 5 9 1 9 9 3 标准。该标准对i e e es t d1 0 1 2 1 9 8 6 标准( 已经被s t d 1 0 1 2 2 0 0 4 版本所替代) 中的软件验证计划做了指南。 d o 1 7 8 b 标准。该标准对空运系统和空运设备认证的软件提出了要考虑 的事项。它由美国航天无线电技术委员会( r t c a ) 公布，被r t c a 和欧 洲民用航空电子组织( e u r o c a e ) 发展，最后被美国联邦航空局接受的 航空电子软件保证。 - 软件验证的一般理论。这是由美国食品和药品局( f d a ) 在2 0 0 2 年针 6 浙江大学硕士学位论文第l 章绪论 对医学设备软件和软件开发过程中的验证制定的一个指南。 对于软件的验证技术，比较新的技术方法如下： - f u n k h o u s e r 等人，在2 0 0 8 年，提出了一种使用u m l 使用用例，在特定 的执行场景下，进行源代码比较的验证方法【瑚。 - t a m a r a h a r o n s 等人，在2 0 0 6 年，针对嵌入式软件验证，提出了使用形式 化技术来覆盖和测试生成的方法，并且将该方法应用于i a 3 2 指令集中【1 9 】。 - j o c h e n 等人，在2 0 0 5 年，针对动态变换软件，提出了开启系统控制来约 束软件执行的方法【2 0 1 。 - n u r i td o r 等人，在2 0 0 4 年，提出了一种通过可缩放路径敏感的值流分析 来进行软件验证的方法【2 1 1 。 对于软件验证的工具，如下： _ e s p ，是一个基于路径敏感，对给定的性质，分析和其相关的分支行为来 进行验证的工具【2 2 1 。 _ s l a m ，由微软开发的用于模型检测、谓词抽象和谓词发现工具。用于验 证w i n d o w s2 0 0 0 的设备驱动【2 3 】。 l d r a ，一个商业化的自动化软件验证套件。它提供了对安全苛刻性软件 的验证，包括对相关标准的支持，例如d o 1 7 8 b 。在2 0 0 8 年，l d r a 被 l o c k h e e dm a r t i n 公司( l m c o ) 选择为猎户座航天器( c e v ) 程序的辅助验 证工具。 与国外早已经开始的软件验证相比，国内的软件验证刚刚开始起步。当前， 我国还没有一个比较好的软件验证工具，存在许多空白需要填补。对于高可靠性 软件的验证过程，依然要依靠人工手动来完成。 1 5 当前软件验证存在的问题 当前软件的验证技术，已经得到了一定的发展，但是软件的规模不一，使用 的用途不同，运行的平台不同，验证的方法和复杂性也不一样。 存在的主要问题如下： 7 浙江大学硕士学位论文第l 章绪论 l 当前的软件验证技术没有一个统一的标准。各个行业，都提出了自己行业 相关的软件验证技术的实施计划标准。但是这些标准都是属于一个特定的领域， 并且都是属于定性描述，没有定量的衡量方法。判断软件是否失效，也是一个语 义问题，很难通过一个自动化的方法，对验证的结果进行判断。 2 当前的软件验证技术，通过硬件和软件两个方式进行验证。通过硬件方式， 要针对具体的电路、端口、引脚，进行验证。这些验证在实施时耗费巨大，并且 得到的数据难以进行分析，没有直观的图形化的表示方法。通过软件方式，则存 在不能验证的软件不能到达的地方。 3 和软件工程结合的软件验证技术，注重源代码级的验证，忽略了目标码的 验证。人们在验证时，只是验证了源代码的正确性，对于真实运行的代码，并没 有真正进行验证。在真实运行的目标码和源代码之间，存在编译器的编译链接过 程。编译器的编译优化、潜在的b u g ，都会对最后产生的目标码和源代码之间的 对应关系发生改变，或者不能进行对应。编译器的安全性问题，使得目标码的正 确性验证面临困难。 4 当前的目标码验证，偏重于理论上的验证，即从需求、设计上进行验证和 证明。对最后生成的目标码部分的验证，验证工具较少，很多验证依然要靠手工 来完成。 1 6 论文研究背景和内容 随着计算机软件在各个行业的普遍应用，航空航天、汽车、医疗设备等对软 件可靠性要求非常高的行业，纷纷提出了自己的软件验证标准，对软件的行为和 功能加以控制。 各个行业内的企业在对软件进行验证时，不仅仅会考虑本行业内的软件验证 标准，同时也会寻找其他行业的相关标准，结合两者，得到一个比较经济、合理 的验证方案。例如在航空电子行业，以前都基于d o 1 7 8 b 标准，后来采用了汽车 行业的m i s r a 的标准。 这种行为正成为一种趋势，并由此给计算机带来新的验证技术的引入。例如 浙江大学硕士学位论文第l 章绪论 d o 1 7 8 b 标准的目标码验证要求，最初是应用在航空电子程序中。但是现在，被 逐渐应用在许多现代嵌入式控制应用软件中。安全苛刻要求的提高，意味着更多 的厂商采用目标码验证技术验证高可靠性软件。 本文属于航天创新基金项目研究内容的一部分，主要针对这种高可靠性软件 下的目标码验证技术的研究，例如d o 1 7 8 b 标准中目标码验证研究。同时，针对 目标码验证在真实平台下的困难，提出了虚拟化平台上的目标码验证，实现了虚 拟化平台支持的目标码验证工具b s v v t 。 b s v v t ，通过对b o c h s 虚拟化平台体系结构进行扩展，嵌入了支持软件验证 的底层目标码覆盖验证、分支图生成、分支反转与提示和故障注入技术，并根据 软件运行动态信息，集成软件验证的轨迹导出功能，从而提供系统级的目标码验 证支持，提高对高可靠性软件的正确性验证与失效恢复能力验证的能力。所有这 些，均不会对验证的程序的目标码做任何形式的改变，满足了航天方面对于软件 验证无侵入性的要求。 全文总共分为六章。 第一章“绪论 。分析了软件可靠性和软件验证的一般概念，对国内外软件 验证技术研究现状做了简单介绍，指出了当前软件验证存在的不足。最后介绍了 论文的研究背景和论文的组织结构。 第二章“软件验证相关技术综述 。本章，首先分析了现有的软件验证技术 的标准和工具。针对目标码验证，分析了其几种比较典型的验证方法。接着，介 绍虚拟化平台的概念和其对目标码验证的支持。最后，针对选用的b o c h s 模拟器， 介绍了它的基本体系结构和调试扩展支持。 第三章“b s v v t 验证工具总体设计”。本章，针对上一章提出的b o c h s 虚拟 化平台，在该平台基础上对b s v v t 目标码验证工具做了总体设计和各个功能的 介绍和原理分析，并对其中的一些难点进行了分析。 第四章“b s w t 验证工具实现。本章具体实现了b s v v t 验证工具。对实 现的难点，做了介绍。 第五章“实验结果和分析。本章首先介绍了使用的平台、环境和操作流程。 9 浙江大学硕士学位论文第1 章绪论 针对西门子套件，对b s v v t 的使用做了介绍。同时，分析了其性能。 第六章“总结和展望 。对全文的工作进行总结，对进一步的工作进行展望。 l o 浙江大学硕士学位论文第2 章软件验证相关技术综述 第2 章软件验证相关技术综述 软件验证技术，在各个行业普遍采用使用软件之后，开始变得重要。本章， 将对软件验证的一些技术进行介绍。这些技术，主要针对目标码验证技术，是本 文的理论和实现基础。 目标码验证技术，作为软件验证的一部分，最早出现在一些对于软件可靠性 非常高的行业，比如航空、航天、汽车等行业。随着当前一些嵌入式软件对安全 性的苛刻要求，目标码验证技术被引入到计算机行业中来。 目标码，是计算机运行的最终代码。对目标码的验证，是对其在机器上的实 际运行的二进制代码的验证。对于这种系统底层的代码验证，如果没有虚拟化平 台的支持，将变得十分困难。选用合理的虚拟化平台，将使得目标码验证技术变 得相对简单，节省了大量的人力、物力。 2 1 软件验证技术标准和工具 当前，软件验证技术在多个行业都得到了运用。一些需要高可靠性软件的行 业，都制订了本行业的软件验证标准。这里，将对和本文相关的几个技术标准和 工具进行具体介绍和分析。 2 1 1i e e es t d i 0 1 2 - 2 0 0 4 标准 i e e e 是美国电气和电子工程师协会的缩写。它是一个国际性的电子技术与信 息科学工程师的协会，其定义的标准在工业界有极大的影响。它也是一个广泛的 工业标准开发者，主要领域包括电能、能源、生物技术和保健、信息技术、信息 安全、通讯、消费电子、运输、航天技术和纳米技术。 在i e e e 标准中，关于软件的验证是发布在s t d1 0 1 2 标准中。该标准至少已 经经历了3 个版本，分别为s t d1 0 1 2 1 9 8 6 ，s t d l 0 1 2 1 9 9 8 ，s t d l 0 1 2 2 0 0 4 。 在这三个版本中，现在使用的是s t d l 0 1 2 2 0 0 4 ，它对s t d l 0 1 2 1 9 9 8 做了一些 小的修改。在这里，只介绍s t d l 0 1 2 2 0 0 4 标准。后文的i e e e 标准，均指 s t d l 0 1 2 2 0 0 4 标准。 浙江大学硕士学位论文第2 章软件验证相关技术综述 在i e e es t d l 0 1 2 2 0 0 4 中，主要描述了以下的内容： 软件完整性级别：定义了软件的完整性级别描述软件重要性。 一每一个软件完整度级别的最小验证( v & v ) 任务：定义了四个软件完整 性级别的最小验证任务。 - 每一个验证任务所需要的强度和严格程度：越高完整度级别，需要更大 的强度和严格程度。 _ 验证任务的详细标准：包括了正确性、一致性、完整性、准确性、可靠 性、可测试性的最小标准。 系统观点下的最小验证任务：包括了竞争分析、安全分析、风险分析、 可移植评估、退役评估。 在i e e e 标准中，提供了软件完整度的四个级别，它们的描述如表2 1 所示。 对于高可靠软件，一般需要执行第3 级，对于特别苛刻的软件安全验证等，要采 用第4 级。 表2 1i e e e 关于软件完整度的4 个级别 级别描述 4 软件必须正确执行，以避免严重的后果发生。( 人员损失、系统 损失、经济或社会损失) 。不能进行补救 3 软件必须正确执行，但是有些必要的功能没有实现，导致严重的 后果( 持久伤害、系统退化、经济社会影响) 。有部分补救措施。 2 软件必须正确执行，但是有些功能没有实现，导致微小的后果。 有完整的补救措施。 l 软件必须正确执行，一些功能的没有实现，导致的后果可以忽略。 不需要补救。 2 1 2d o 一1 7 8 b 标准 d o 1 7 8 b 标准，即机载系统和设备合格审定中的软件考虑，是由美国航 空无线电技术委员会( r t c a ) ，由r t c a 于1 9 9 2 年1 2 月1 日批准，被美国联邦 航空局接受的航空电子保证。 在d o 1 7 8 b 标准中，讨论了涉及到航空器和发动机上所用机载系统和设备中 1 2 浙江大学硕士学位论文第2 章软件验证相关技术综述 的软件开发过程中的适航性合格审定方面的问题。这些问题，大部关注于软件生 存周期内和系统生存周期内的过程，并没有讨论最终软件运行的问题。 d o 1 7 8 b 提出了软件等级的概念。软件等级是基于在系统安全性评估过程中 确定的软件对潜在失效状态的影响。软件等级意味着用来表明符合合格审定要求 的努力程度随失效状态的类别而变化。具体的软件等级及其定义如表2 2 所示。 表2 - 2d o - 1 7 8 b 对于软件等级的描述 级别描述 a 可能引起或导致系统功能失效，进而引起航空器灾难性失效状 态的异常状态的软件。 b 可能引起或导致系统功能失效，进而引起航空器危险的严重的 失效状态的异常状态的软件。 c 可能引起或导致系统功能失效，进而引起航空器较重失效状态 的异常状态的软件。 d 可能引起或导致系统功能失效，进而引起航空器较轻失效状态 的异常状态的软件。 e 可能引起或导致系统功能失效的异常状态的软件，它不会影响 航空器的工作性能或驾驶员工作量。 每一个级别中的异常状态，都是可以由系统安全性评估过程来表明。在 d o 1 7 8 b 中，只对a d 级软件进行合格审定。 d o 1 7 8 b 中，对系统需求、软件需求和结构、可追踪性数据、源代码、可执 行目标码和软件验证计划等各个方面都做了验证的指导原则和评审方法。 特别的，对于目标码，在验证方法中强调了以需求为基础的验证，它由结构 覆盖范围补充。需要有正确的测试用例以及鲁棒的测试用例来共同进行验证。软 件验证过程要提供在软件需求的实现与对软件需求的验证之间的可追踪性：由基 于需求的覆盖分析完成软件需求与测试用例之间的可追踪性，由结构覆盖分析完 成代码结构与测试用例之间的可追踪性。这种验证方法已经跨行业，在一些嵌入 式软件的验证中得到了应用。 浙江大学硕士学位论文 第2 章软件验证相关技术综述 2 1 3l d r a 及其工具套件 l d r a 是一家专门对软件提供自动化分析和测试工具的公司。该公司的测试 工具在航空、国防、核能和汽车部门得到使用，用来测试这些部门的软件是否达 到安全标准。 l d r a 具有一系列的工具。其中，l d r a t e s t b e d 提供了静态代码分析，代码、 质量和设计复查，以及代码覆盖率的验证。t b r u n 提供了自动化单元测试，t b r e q 提供了需求可追踪分析，t b m a n a g e r 扩展了t b r e q ，t b e v o l v e 提供了软件基线 管理。t b s a f e 提供了对d o 1 7 8 b 标准的安全认证，还提供了d o 1 7 8 b 工具资格 证明。 l d r a 工具套件满足多个标准，其中包括了d o 1 7 8 b 、i e c 1 2 5 0 8 和 m i s r a c 。其中前两个标准是对软件开发过程中的软件验证提出的，而最后一个 m i s r a c 是m i s r a 标准中规定如何使用安全的c 语言。 针对d o 1 7 8 b 标准下的目标码验证，l d r a 工具提供了一套完整的结构化语 言覆盖率分析方案，包括了语句、分支、测试路径、过程函数调用、布尔表达式 覆盖等各种形式的覆盖率测试。 l d r a 公司提供的目标代码验证工具表现为目前市场上最完善，最经济的解决 方案。这也使得该工具在美国很多重要部门的软件验证中得到广泛的使用。 2 2 目标码验证技术 2 2 1 目标码验证 目标码验证，就是对软件编译链接完成以后的目标码进行软件验证。它分析 其中的代码运行