采用C＋＋代码插装的实时软件内存错误分析

在航天领域中,安全关键的大型实时软件系统往往直接影响到任务成败,一般难以全面检测、分析或避免内存泄漏等常见内存错误。定义了实时软件的12种典型内存故障模式,提出了一种基于C＋＋代码插装的实时软件内存错误快速分析方法。该方法通过对C＋＋源代码进行静态分析,获取指针变量相关信息;通过C＋＋代码插装和运行不同测试用例,实时收集统计C＋＋指针对象的分配、释放、赋值、c-use和p-use使用情况,结合实时软件的典型内存故障模式进行分析,并自动生成详情报告。应用案例表明,该方法能够高效快捷地发现实时软件潜在的典型内存错误,从而有效提高软件质量。     

μC/OSⅡ内存管理的一种改进方法

研究了μC/OSⅡ的内存管理,发现当对一个申请到的内存块进行越界写操作或产生了指向空闲内存块指针区(头几个字节)非法指针时可能会破坏它指向下一个空闲内存块的指针,这样,空闲内存块链表就会被破坏.出于安全性要求,必须将控制信息与用户使用的空闲内存块分开,内存块的控制信息属于系统数据,必须对其进行保护.利用μC/OSⅡ的就绪表(Ready List)中任务的调入和删除原理,构造一个内存管理表,实现内存块的分配和释放.由此,μC/OSⅡ在内存管理中存在的安全性问题得到了解决.     

μC/OSⅡ内存管理的一种改进方法

研究了μC/OSⅡ的内存管理,发现当对一个申请到的内存块进行越界写操作或产生了指向空闲内存块指针区(头几个字节)非法指针时可能会破坏它指向下一个空闲内存块的指针,这样,空闲内存块链表就会被破坏.出于安全性要求,必须将控制信息与用户使用的空闲内存块分开,内存块的控制信息属于系统数据,必须对其进行保护.利用μC/OSⅡ的就绪表(Ready List)中任务的调入和删除原理,构造一个内存管理表,实现内存块的分配和释放.由此,μC/OSⅡ在内存管理中存在的安全性问题得到了解决.     

μC／OSII内存管理的一种改进方法

研究了μC／OSII的内存管理，发现当对一个申请到的内存块进行越界写操作或产生了指向空闲内存块指针区(头几个字节)非法指针时可能会破坏它指向下一个空闲内存块的指针，这样，空闲内存块链表就会被破坏。出于安全性要求，必须将控制信息与用户使用的空闲内存块分开，内存块的控制信息属于系统数据，必须对其进行保护。利用μC／OSII的就绪表(Ready List)中任务的调入和删除原理，构造一个内存管理表，实现内存块的分配和释放。由此，μC／ISII在内存管理中存在的安全性问题得到了解决。     

一种用于类C语言环境的安全的类型化内存模型

使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证.     

指针的学习与应用

指针是C程序设计的重点和难点，也是软件界的讨论热点：、正确而灵活地运用指针，可以有效地表示复杂的数据结构，能动态分配内存，直接处理内存地址等。在学习和应用指针过程中，传统的指针概念和用法常常使人感到困惑。文中提出了单星指针、双星指针等新概念，比较全面地介绍了指针的理论和应用．     

一种实现C语言变量“动态定义”的方法

1.问题分析 C语言中变量定义的实质(或目的),是为了在编译时能为其分配相应的存储单元。同时,C语言又提供了指针机制,允许使用指针对内存单元进行操作。而且,C语言经编译后,取得并使用四个逻辑上不同、且用于不同对象的内存区域,它们分别是:栈、堆、全局变量区、程序代码区,其中“堆”是一个自由内存区域,C语言可通过内存分配函数(malloc()、calloc()),动态地从中获得所需空间。由指针指向被分配的内存块,其     

以管理者视角突破C++指针教学难点

指针是C++语言教学的重点和难点。以一级指针、二级指针的教学为例,以管理者和被管理者的新视角突破指针教学的难点,帮助学生理解和提高应用指针的能力,取得良好的教学效果。     

C语言内存错误分析与研究

指针是C语言的精华所在,正确使用指针能使程序简洁高效,能避免内存错误和程序异常,保证程序的正确性和可移植性。针对指针在编程过程中可能出现的错误,阐述了C编译器对数据进行内存分配的策略,通过具体的实例进行分析,并给出解决方法。     

C语言指针的理解与运用

指针是C语言中广泛使用的一种数据类型，运用指针编程是C语言的主要风格之一。利用指针变量可以直接对内存中各种不同数据进行快速处理，理解和运用好指针可以编出简洁明快、性能强的C程序。     

Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic-Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool-plcc was implemented to automatically verify a number of non-trivial pointer programs.     

Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.     

C程序中的内存泄漏机制分析与检测方法设计

C语言作为安全关键软件的主要实现语言,其存在的内存泄漏缺陷具有很高的隐蔽性和危害性,如何保证内存泄漏检测的准确性和高效性是一大挑战。静态分析具有直接分析源码、能够较早发现软件错误,从而降低修复代价的优势。基于静态分析技术,提出了一种基于路径敏感的值流分析的内存泄漏检测方法,首先进行指针分析生成精确指向信息;然后基于指向信息构建值流约束,执行可达性分析以识别程序中的泄漏路径;最后借助指针与内存地址的有效生命周期进行验证。在典型基准C程序上的实验结果分析表明,本文方法与现有技术相比在效率和精度上都具有一定优势。     

MemSafe: ensuring the spatial and temporal memory safety of C at runtime

Memory access violations are a leading source of unreliability in C programs. As evidence of this problem, a variety of methods exist that retrofit C with software checks to detect memory errors at runtime. However, these methods generally suffer from one or more drawbacks including the inability to detect all errors, the use of incompatible metadata, the need for manual code modifications, and high runtime overheads. This paper presents a compiler analysis and transformation for ensuring the memory safety of C called MemSafe. MemSafe makes several novel contributions that improve upon previous work and lower the cost of safety. These include (i) a method for modeling temporal errors as spatial errors, (ii) a metadata representation that combines features of both object‐based and pointer‐based approaches, and (iii) a dataflow representation that simplifies optimizations for removing unneeded checks. MemSafe is capable of detecting real errors with lower overheads than previous efforts. Experimental results show that MemSafe detects all memory errors in six programs with known violations as well as two large and widely used open source applications. Finally, MemSafe ensures complete safety with an average overhead of 88% on 30 programs commonly used for evaluating the performance of error detection tools. Copyright © 2012 John Wiley & Sons, Ltd.     

Precise Call Graphs for C Programs with Function Pointers

The use of pointers presents serious problems for software productivity tools for software understanding, restructuring, and testing. Pointers enable indirect memory accesses through pointer dereferences, as well as indirect procedure calls (e.g., through function pointers in C). Such indirect accesses and calls can be disambiguated with pointer analysis. In this paper we evaluate the precision of one specific pointer analysis (the FA pointer analysis by Zhang et al.) for the purposes of call graph construction for C programs with function pointers. The analysis is incorporated in a production-strength code-browsing tool from Siemens Corporate Research in which the program call graph is used as a primary tool for code understanding.The FA pointer analysis uses an inexpensive, almost-linear, flow- and context-insensitive algorithm. To measure analysis precision, we compare the call graph constructed by this analysis with the most precise call graph obtainable by a large category of existing pointer analyses. Surprisingly, for all our data programs the FA analysis achieves the best possible precision. This result indicates that for the purposes of call graph construction, inexpensive pointer analyses may provide precision comparable to the precision of expensive pointer analyses.     

A low-level memory model and an accompanying reachability predicate

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.     

一种用于指针程序安全性证明的指针逻辑

在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.