近年来,随着软件规模的扩大、复杂度的提升、应用领域的拓展,软件的可信性问题已成为用户、从业人员和研究人员共同关注的焦点。目前业界公认的一个观点是,如何在软件开发的早期尽可能地发现并排除软件缺陷以节省成本,是构建可信软件的重要途径。由于静态分析技术可以基于程序片段进行分析,无需执行程序,且可以针对小概率缺陷实施有效测试,因此成为构建可信软件的有效手段。静态分析的结果不可能做到既是可靠的(sound)又是完备的(complete),导致其分析结果不精确从而出现误报(false positive)或漏报(false negative)。误报率与漏报率是评价静态分析技术的主要指标,而如何提高静态分析的精度以降低缺陷检测中的误报率和漏报率已成为影响静态分析技术实用性的关键,也是国内外该领域的研究热点。本文的研究工作受国家高技术研究发展计划“863”基金项目“软件的安全性缺陷模型及基于安全性缺陷模型的测试技术(2009AA012404)”、“勾化软件协同生产和运行演化集成平台及服务环境(2012AA010101)”及国家自然科学基金项目“航天嵌入式软件缺陷检测方法研究、系统研发及应用(91018002)”的支持,以提升静态缺陷检测工具的精度及效率为主要目标,主要做了以下四个方面的工作：1、引入符号化三值逻辑以提高数据流分析的精度基于抽象解释的数据流分析技术,通过各种数值抽象域表示变量的取值信息,通过抽象域上的计算来反映变量间的运算关系。区间抽象域是最简单、最直观的变量取值表示形式,具有较高的运算效率,因此己在静态分析及程序验证工具中广泛应用。然而,区间抽象域是典型的非关系型抽象域,只能表示变量的离散取值信息而无法表示变量间的关联关系,与其他关系型抽象域相比,其表示能力相对较弱,因此基于区间抽象域的静态分析技术其分析精度有限。符号分析技术很好地克服了在静态分析时不能确定程序中变量取值的问题,且可以表示变量间的线性关联关系,从而弥补了基于区间抽象域的数据流分析技术的先天不足,一定程序上提高了分析精度。但对于程序中普遍存在的变量间的逻辑关联关系,经典的符号分析技术却无法表示,仍旧会产生精度损失；并且,符号分析技术主要处理对象为程序中数值类型的变量,对C语言中指针类型的变量及内存操作支持较少。本文提出一种基于符号化三值逻辑模型(Symbolic Three-Valued Logic, STVL)的数据流分析万法,对经典的的符号分析技木进行扩展,从而可以统一描述变量间的线性及逻辑关系,提高数据流分析的精度；同时,STVL模型可以优化指针模型,对指针运算、内存建模提供支持,增强了缺陷检测系统对指针及内存相关缺陷的检测能力。2、基于符号化函数摘要模型的上下文敏感的函数间分析技术精确的程序分析技术都应包含两种基本的分析方式：分析单个函数语法语义行为的函数内分析(Intra-procedure Analysis),及分析函数调用等函数间交互行为的函数间分析(Inter-procedure Analysis)。经典的函数间分析方法包括内联展开(procedure inlining)、记录函数调用串(call string)及计算函数摘要(procedure summary)等方法。由于函数内联及调用串技术均属于穷尽计算方法(exhausitive computing),需要对函数进行重复展开或重复分析,因此复杂度相对较高。本文提出一种基于符号化函数摘要模型(Symbolic Procedure Summary Model, SPSM)的上下文敏感的函数间分析技术：(1)在函数内分析过程中,生成统一的符号化函数摘要模型实例,包括后置摘要、函数特征摘要及前置约束摘要；(2)在函数调用点处,根据上下文的数据流值与SPSM中摘要条件的对比,获取对应的符号化函数摘要,并将调用点处的实际数据流值替换摘要信息中的符号值,即进行符号化函数摘要实例化,从而实现了上下文敏感分析；(3)对于存在多级函数调用的情况,通过自定义的摘要传递函数(summary transfer function)进行自下而上的摘要传递,精确地模拟了多级函数调用的实际运行时信息,从而可以检测由于函数调用引起的潜在缺陷。3、基于缺陷模式的程序切片方法以提高路径敏感缺陷检测方法的效率及精度路径敏感分析方法考虑不同数据流分支间的组合关系,可以记录控制流上的不同路径信息,从而有效减少静态分析时的误报。精确的路径敏感分析方法会记录程序中的所有路径信息,虽然该方式精度较高,但这种全路径分析方法由于存在路径爆炸的危险,会严重影响分析效率。因此,实用的路径敏感分析方法往往采用一些折衷策略,例如在控制流汇合处进行数据流合并,或者通过分析路径的可达性避免不可达路径上的数据流传递等。本文将程序切片技术应用于缺陷检测,提出一种基于缺陷模式的程序切片方法,该方法基于缺陷特征和路径条件建立切片准则,根据控制流节点上的数据流信息与切片准则的包含关系进行程序切片,得到的切片程序在缺陷检测时不仅切片掉了缺陷无关节点,从而减少了数据流迭代时的计算量,而且与源程序完全等价从而保证了静态分析的保守性。为了进一步减少误报,提出一种基于切片程序的缺陷状态合并策略,根据控制流分支节点的路径条件,对缺陷状态添加状态属性,从而有选择地对控制流汇合节点进行状态合并,以提高检测精度。4、前向数据流分析与逆向约束搜索相结合的误报消除技术研究前文所述的数据流分析方法、函数间分析方法及路径敏感分析技术,均属于前向数据流分析范畴。在综合采用了各种提高数据流分析精度的技术后,静态缺陷检测仍然会存在一定数量的误报,因此对静态缺陷检测的初始结果进行进一步的求精,即进行误报消除,便成为提高缺陷检测精度的有效手段。在对比分析了各种误报消除技术的基础上,本文提出了一种前向数据流分析结合逆向约束搜索技术的缺陷检测方法：前向数据流分析的保守数据流解可以用于缺陷状态迭代,并得到初始的缺陷检测结果；根据缺陷发生处的数据流特征,逆向搜索可能导致缺陷发生的约束条件,该约束条件可以作为通用约束求解器的输入判断缺陷的可满足性,从而对初始的缺陷检测结果进行精化。同时,在数据流分析过程中结合符号分析技术,不仅提高了数据流分析的精度,且便于约束表示及转化,提高了约束搜索的效率