基于模型检测的数据流异常测试技术研究

程序的执行体现为数据在变量中的流动。对C/C++源代码中变量定义使用情况进行分析,针对变量未赋值就使用、变量重复赋值和变量定义后未使用三种数据流异常情况,使用程序阅读自动机,把程序转换为变量状态机,使用ALCCTL时序逻辑和模型检验工具,验证程序是否满足定义的可信模式。提出了新的静态查找变量使用故障的方法。该方法已应用于面向故障的软件测试系统中。     

CTCS-2级列控系统的形式化建模与验证

由于 CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使其转化为NuSMV模型。将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证,验证结果都为true,表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性。     

一种用C++动态扩展C#程序的方法

提出一种用非托管C++(以下简称C++)动态扩展C#程序的方法。利用托管C++作为适配器,由C++类继承C#基类,并且获取C#程序提供的服务;将C++类利用托管C++作为适配器,通过C#基类的派生类提供给C#程序动态加载。实例表明该方法能够使C++编写的类继承C#程序中的类,获取C#程序提供的服务;并且使C#程序能够动态创建并调用C++类对象。该方法能够为C++源代码的重用、C++源代码与.NET平台语言的混合编程等提供解决方案。     

面向多线程程序的内存安全运行时验证

Linux操作系统、嵌入式系统、航电系统、通信系统等一般都是用C/C++语言进行编写。因为C语言具有偏底层硬件、移植性强、执行效率高等优秀特性。但是随着多核并行机的出现，许多语言也开始支持多线程编程。由于C语言本身存在着对内存访问时，不对内存边界进行检查的问题，从而造成软件系统相关的可靠性和安全性问题。对多线程C语言程序来说，由于多线程程序的不确定性，使得运行时验证多线程C程序的内存安全问题变得更加困难。通过使用基于改进的指针运行时验证技术、多核多线程技术、并行计算、无锁数据结构技术、源代码插桩技术方法，并结合开源工具Clang编译器实现原型工具Movec对多线程C程序的支持。该工具实现了对多线程C程序内存安全问题的运行时验证。然后通过Mibench和SARD测试用例进行实验，验证了该工具对多线程C程序进行运行时验证的有效性。     

采用Clang/LLVM的C++源代码覆盖率分析插装方法

近年来,越来越多的安全关键软件系统运行在国产Linux操作系统上,其中大多数采用C++开发,而C++正在扩展新版语言规范,已有的覆盖率统计插装工具不能满足要求。给出一种基于Clang/LLVM的C++源代码覆盖率统计插装方法,利用开源社区Clang/LLVM库提供的C++源代码解析和操作功能,构建面向C++源代码的语句、分支和MC/DC覆盖率统计框架,在运行时采集覆盖率信息并进行统计分析,输出覆盖率分析报告。实际案例表明,该方法简易实用,能够满足真实工程软件的覆盖率测试分析需求。     

C/C++软件测试工具的元数据结构设计与实现

针对用C/C++语言进行的语义分析,设计一种中间结构,即元数据结构。元数据结构实现了源代码的语义层次上的抽象,通过元数据结构和相关应用语义配置,过滤出源程序中符合应用的语义内容,实现软件测试工具的程序插装等功能。在中间结构实现过程中,构造一个二次解析引擎,以解决传统解析方法的复杂性及不确定性,实现对各种编程语言的支持。     

基于XML的软件安全静态检测方法研究

安全关键软件设计使用的C/C++语言含有大量未定义行为,使用不当可能产生重大安全隐患。软件静态检测是从软件代码和结构中找出安全缺陷的重要手段。从安全规则的角度,提出了基于XML（eXtensible Markup Language）中间模型的静态检测方法。该方法将C/C++源代码解释为XML中间模型,将安全规则转化为缺陷模式,利用Xquery查询表达式对软件安全缺陷进行定位。基于该方法的原型系统检验结果表明：该方法能够有效地检测出违反安全规则的软件缺陷,并具有安全规则可定制的特点。     

基于状态转换的PLC程序模型构建方法

针对可编程逻辑控制器（PLC）程序在进行NuSMV模型检测时需要手工对程序进行建模,不仅浪费人力且容易出错的问题,提出一种基于状态转移的PLC程序模型自动化构建方法。该方法首先分析结构化文本（ST）语言特性并解析ST程序为抽象语法树;其次,在抽象语法树基础上,根据不同的文法结构进行控制流分析生成控制流图;然后,通过数据流分析得到程序依赖图;最后,根据程序依赖图生成NuSMV的输入模型。实验结果表明,所提方法实现了ST程序到NuSMV输入模型的自动化构建,并且构建的NuSMV输入模型既保留了ST程序的原有特性又符合NuSMV模型检测工具输入的规范,与传统手工模型构建方法相比,提高了模型生成的效率和准确率。     

基于源代码分析的逆向建模*

逆向建模通过对源代码进行分析,提取出代码中的对象信息、结构信息、流程信息等,生成对象间的关系描述、结构描述、系统流程描述等设计模型描述。逆向建模过程中对源代码的分析处理与编译过程的前端处理相似,只是处理的复杂程度与产生的目标结果不同,因此可以采用编译技术对源代码进行处理。通过逆向建模可以弥补软件设计中缺少或缺失的模型设计文档,帮助代码阅读者更好地理解程序,帮助软件的测试和优化。介绍了对C/C++源代码进行逆向建模的实现。     

基于控制流切片的代码安全缺陷检测方法

为轻松获得程序的可能执行路径,进而实现程序变量的状态跟踪,提出了一种C/C++源代码控制流提取算法,通过该模型获取控制流切片,产生局部控制流图,将数据流异常检测与安全子集检测相结合,弥补了单独使用安全子集方法无法跟踪数据流的不足,增强代码安全隐患的挖掘能力.利用控制流图化简,排除部分不可达控制流信息,提高跟踪效率.通过对3个Linux内核源文件的检测,验证了该方法不仅可以检测出违反安全子集的代码安全隐患,同时对代码数据流异常检测提供支持,准确率达94.9％.     

Platform‐independent code conversion within the C++ locale framework

This paper describes some of the author's experiences from a C++ implementation of a concordance program for texts in Old West Norse (also known as Old Icelandic) and Runic Swedish. Since the input to the program used a character repertoire that no standard one‐byte character encoding covers, it was natural to use Unicode to represent data both inside the program and in external files. Inside the program, each character was represented with C++ ‘wide characters’; the input and output was represented in UTF‐8. The author constructed C++ code conversion facets that convert data between those two representations during file I/O. This enabled him to successfully compile, and run, the concordance program on both Linux (Fedora Core 3 with gcc 3.4.2) and Windows XP (using Visual C++ .NET 2003). The only necessary change to the source when changing platform was isolated to the lines selecting which code conversion facet to use—all other pieces of code remained unchanged. In particular, the author could still use the standard C++ locale framework for collation and code conversion, in spite of the fact that the library‐provided code conversion facets had been replaced. Copyright © 2006 John Wiley & Sons, Ltd.     

Mobile agent‐based computational steering for distributed applications

The mobile agent‐based computational steering (MACS) for distributed applications is presented in this article. In the MACS, a mobile agent platform, Mobile‐C, is embedded in a program through the Mobile‐C library to support C/C++ mobile agent code. Runtime replaceable algorithms of a program are represented as agent services in C/C++ source code and can be replaced with new ones through mobile agents. In the MACS, a mobile agent created and deployed by a user from the steering host migrates to computing hosts successively to replace algorithms of running programs that constitute a distributed application without the need of stopping the execution and recompiling the programs. The methodology of dynamic algorithm alteration in the MACS is described in detail with an example of matrix operation. The Mobile‐C library enables the integration of Mobile‐C into any C/C++ programs to carry out computational steering through mobile agents. The source code level execution of mobile agent code facilitates handling issues such as portability and secure execution of mobile agent code. In the MACS, the network load between the steering and computing hosts can be reduced, and the successive operations of a mobile agent on multiple computing hosts are not affected whether the steering host stays online or not. The employment of the middle‐level language C/C++ enables the MACS to accommodate the diversity of scientific and engineering fields to allow for runtime interaction and steering of distributed applications to match the dynamic requirements imposed by the user or the execution environment. An experiment is used to validate the feasibility of the MACS in real‐world mobile robot applications. The experiment replaces a mobile robot's behavioral algorithm with a mobile agent at runtime. Copyright © 2009 John Wiley & Sons, Ltd.     

Global analysis and transformations in preprocessed languages

Tool support for refactoring code written in mainstream languages such as C and C++ is currently lacking due to the complexity introduced by the mandatory preprocessing phase that forms part of the C/C++ compilation cycle. The definition and use of macros complicates the notions of scope and of identifier boundaries. The concept of token equivalence classes can be used to bridge the gap between the language proper semantic analysis and the non-preprocessed source code. The CScout toolchest uses the developed theory to analyze large interdependent program families. A Web-based interactive front end allows the precise realization of rename and remove refactorings on the original C source code. In addition, CScout can convert programs into a portable obfuscated format or store a complete and accurate representation of the code and its identifiers in a relational database.     

基于GCC的C/C＋＋源程序静态信息提取技术

给出了一种基于GCC的AST中间文件来提取C/C＋＋语言源程序静态信息的方法。主要思想是利用GCC编译源程序时产生的AST文件,借助XOgastan工具将其转换成GXL格式文件,然后从GXL格式文件转换成标准的XML文档,最后树形化地显示源程序的结构关系。     

Verilog到C翻译器的设计与实现

介绍了一种将Verilog硬件描述转化到等价C／C＋＋代码的自动翻译器的实现过程，并给出了简化Verilog行为模型的疗法、非阻塞赋值串行化的优化算法和一些访存优化原则。该方法没计的翻译器的生成代码可直接由C/C＋＋编译器汇编成可执行程序后进行仿真。采用龙芯RTL作为系统输入的测试表明，该方法的仿真速度可比一般仿真软件有成倍的增加，并能在系统评估和分析上发挥显著的成效。     

基于符号执行的底层虚拟机混淆器反混淆框架

针对Miasm反混淆框架反混淆后的结果是一张图片,无法反编译恢复程序源码的问题,在对底层虚拟机混淆器（OLLVM）混淆策略和Miasm反混淆思路进行深入学习研究后,提出并实现了一种基于符号执行的OLLVM通用型自动化反混淆框架。首先,利用基本块识别算法找到混淆程序中有用的基本块和无用块;其次,采用符号执行技术确定各个有用块之间的拓扑关系;然后,直接对基本块汇编代码进行指令修复;最后,得到一个反混淆后的可执行文件。实验结果表明,该框架在保证尽量少的反混淆用时前提下,反混淆后的程序与未混淆源程序的代码相似度为96.7%,能非常好地实现x86架构下C/C++文件的OLLVM反混淆。     

Linux平台下基于源代码插装的动态内存检测

在C／C＋＋语言程序中．指针的使用使代码灵活、简便．但所带来的类似内存泄漏、内存写溢出等的内存使用的错误却很难分析和消除．针对这些容易出现的内存使用错误．提出了Linux平台下一种基于源文件信息提取和源代码插装的动态内存检测方法，设计实现了一个动态内存检测模块DDMEM．可以检测源代码的内存泄漏、内存写溢出、释放野指针和内存管理函数的不匹配等问题．给出了写溢出错误的一个实例检测，以验证方法的有效性．