基于变量访问序模式的中断数据竞争检测方法

在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而中断在并发语义、同步机制、调度机制等方面与线程（任务）有诸多不同,具有Ad-hoc特征,难以统一刻画,因此主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具SpaceDRC.实验表明,SpaceDRC能够在145毫秒内检测出约21400行程序中的真实数据竞争.SpaceDRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.     

基于UPPAAL的微内核操作系统程序验证方法研究

随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题。形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术。形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类。文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证。     

基于启发式的静态中断数据竞争检测方法

提出一种面向中断驱动型嵌入式软件的启发式静态数据竞争检测方法,并开发了原型工具H-RaceChecker.给定软件的源代码或目标程序,H-RaceChecker能够自动推断中断优先级状态、中断使能状态和内存访问状态等信息,在此基础上识别出每个程序点处可能的数据竞争,进而通过启发式精化策略对原始分析结果进行危险程度排序,提高人工确认结果的效率.实验验证了该方法的有效性.     

针对整数溢出潜在漏洞的快速定位系统

整数溢出漏洞作为一种历史悠久的漏洞,在当前的软件生态系统中仍然存在,且仍然可能导致严重的系统安全问题。对于整数溢出漏洞的检测工作主要是通过使用或结合符号执行,污点分析,模糊测试等技术进行,也取得了较好的效果。但是由于这些方法需要对检测目标进行深入的分析,这很大程度上限制了这些检测工具的推广和使用。该文针对整数溢出漏洞,分析了漏洞的产生原因和带来的安全威胁,设计和实现了一个基于静态语义匹配搜索的面向二进制文件的整数溢出潜在漏洞的快速定位系统。经测试,该系统能够检测出已公开的整数溢出漏洞。通过该系统检测软件中的整数溢出漏洞,及时对软件进行修复防护,可以有效提高软件的健壮性,减少整数溢出漏洞带来的安全隐患。     

关于在嵌入式软件开发中应用模型驱动开发技术的探讨

为解决传统嵌入式软件开发中存在的制约嵌入式软件开发效率和质量的问题,提出在嵌入式软件开发中应用模型驱动开发技术,介绍了模型驱动开发技术,分析了模型驱动开发技术的优势,并探讨了在嵌入式软件开发中应用模型驱动骨发技术的前景。     

中断驱动型嵌入式软件自动测试方案的实现

自动化测试作为一种重要的软件测试技术，如果将其引入嵌入式软件的测试流程，将会对软件的质量、成本和周期带来显著的效果。首先分析了基于模块化设计的嵌入式软件的特点和测试需求，随后提出了一套面向中断驱动型高可靠嵌入式应用的自动化测试解决方案，最后总结了自动化测试的优点及其适用范围。     

基于MDA的嵌入式软件开发平台设计

针对如何快速开发高质量的嵌入式软件的问题,实现了一种基于MDA的嵌入式软件开发平台EUP。该平台根据模型驱动的软件开发方法,集成UML建模、模型验证、模拟和自动代码生成技术等,为嵌入式软件的开发提供了一个统一的开发环境。分析了铁道交叉路口系统的实例,试验结果表明EUP平台能够方便、高效地实现模型模拟和验证,为快速开发高质量的嵌入式软件提供了一种可行的途径。     

嵌入式软件中断系统资源冲突检测技术研究

由于中断触发的随机性和不确定性,导致中断缺陷引发的问题时有发生,而且通常是不易追踪的严重软件故障,因此对中断系统软件的测试就提出了很高的要求,但是目前可用于中断系统资源冲突检测的工具缺乏.为有效检测由中断的资源冲突引发的软件问题,在分析了与中断相关的典型故障模式的基础上,提出了一种针对嵌入式软件中断系统的资源冲突进行检测的技术和方法.实验结果表明,该方法可有效检测出软件中与中断相关的资源冲突问题.     

WCSD动态检测方法

嵌入式软件最大堆栈深度(worst-case-stack depth,WCSD)是指导硬件设计和软件开发的重要指标,然而它的测量却极其困难.通过详细分析堆栈使用原因及其相互关系,建立多层中断叠加模型并提出一种WCSD动态检测方法,以检测嵌入式软件堆栈深度上限.同时,基于嵌入式软件全数字仿真平台完成实验以验证该模型和方法的可行性.实验结果表明,该模型和方法可测得较准确的WCSD结果,有助于在降低内存开铕,保证嵌入式系统的堆栈安全以及提高嵌入式软件的可靠性.     

基于程序特征谱整数溢出错误定位技术研究

随着软件业的飞速发展,人们对软件质量的要求也越来越高.整数溢出错误以其高危性和隐蔽性成为影响软件安全性和可靠性的重要因素之一.如何准确定位整数溢出错误是软件安全领域研究的热点.论文改进了现有错误定位模型,构建了整数溢出错误定位模型INTRank.实验结果表明:基于INTRank模型的语句可疑度估计方法可以较为准确地计算语句可疑度,使得程序员能够按照基于语句可疑度的优先级顺序检查源代码,找出导致整数溢出错误的原因,同时本文方法具有较低的漏报率.     

一种针对C程序缓冲区溢出的检测方法*

为了增强对程序缓冲区溢出漏洞的检测,提出一种利用CCured和BLAST对C程序进行分析的检测方法。首先利用CCured对C语言源程序进行运行时检测的代码插桩;然后用BLAST提供的自定义安全属性语言对这些插桩代码进行相关约束描述;最后让BLAST根据约束描述文件对代码插桩后的程序进行模型检测,就可以尽可能地找出C语言程序中潜在的缓冲区溢出漏洞。     

模型检验在航天测控软件上的应用研究

模型检验是确保程序质量的有效手段,能弥补软件测试的不足。但航天测控软件规模大、输入数据复杂、验证性质不明确等因素极大地阻碍了模型检验的应用。针对航天测控软件,分析了其特点以及对其执行模型检验的困难,提出了基于有界模型检验器CBMC的模型检验应用框架,包括航天测控数据的构造方法及验证性质的提取方法。随后,将该框架应用于外测数据处理软件,取得了良好的效果。     

Interrupt Verification via Thread Verification

Most of the research effort towards verification of concurrent software has focused on multithreaded code. On the other hand, concurrency in low-end embedded systems is predominantly based on interrupts. Low-end embedded systems are ubiquitous in safety-critical applications such as those supporting transportation and medical automation; their verification is important. Although interrupts are superficially similar to threads, there are subtle semantic differences between the two abstractions. This paper compares and contrasts threads and interrupts from the point of view of verifying the absence of race conditions. We identify a small set of extensions that permit thread verification tools to also verify interrupt-driven software, and we present examples of source-to-source transformations that turn interrupt-driven code into semantically equivalent thread-based code that can be checked by a thread verifier. Finally, we demonstrate a proof-of-concept program transformation tool that converts interrupt-driven sensor network applications into multithreaded code, and we use an existing tool to find race conditions in these applications.     

Automatic Buffer Overflow Warning Validation

Static buffer overflow detection techniques tend to report too many false positives fundamentally due to the lack of software execution information. It is very time consuming to manually inspect all the static warnings. In this paper, we propose BovInspector, a framework for automatically validating static buffer overflow warnings and providing suggestions for automatic repair of true buffer overflow warnings for C programs. Given the program source code and the static buffer overflow warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector provides suggestions to automatically repair it with 11 repair strategies. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically validate on average 60% of total warnings reported by static tools.

     

二进制程序整型符号转换缺陷的动态检测方法

针对符号转换错误引起缓冲区溢出的这类缺陷提出了一种面向二进制程序整型符号转换缺陷检测方法。以二进制插桩框架为基础,利用类型推断方法识别整型变量的符号类型信息,得到内存相关库函数中为冲突类型的参数的集合,并将其作为潜在的整型符号转换缺陷候选集。在中间代码层面插入检测代码做运行时检测,最终确定真正的整型符号转换缺陷。原型系统Sconvcheck的实验结果表明：该方法可以有效地检测出程序中的整型符号转换缺陷,并准确地定位错误发生的位置,而且误报率较低。     

BDD-based software verification

In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space; BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable’s domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.     

Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems. In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on (a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lock-acquisition and release in a program (building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time over existing approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL_?X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers.     

基于运行时类型分析的整形漏洞二进制检测和定位系统

整形漏洞(Integer-based vulnerability)是一种存在于C或C++代码中的漏洞,具有极其严重的破坏性。2006年CVE指出缓冲区溢出漏洞呈下降趋势,而其他一些漏洞,如整形溢出、符号转换错误等呈上升趋势。设计并实现了一种针对整形漏洞的二进制实时检测和定位的方法。针对整形漏洞攻击,首先将二进制文件转化为一种中间语言VEX;然后在运行时将与外部输入相关的数据着色,截获相关语句并记录信息;最后依据制定的检测策略对着色的数据进行检测并定位。选用常见的含有内存漏洞的程序来测试系统的有效性及其性能损耗。实验结果表明,该工具可以检测并且定位软件中绝大多数的整形漏洞,而且误报和漏报率都很低。