断言语言支持自定义谓词的程序验证器原型

基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.     

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.     

一种汇编语言指针逻辑的设计与实现

软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证.     

基于C语言的字符串处理算法研究

本文针对字符串中取出整型数据这一问题提出了更加直观简单的算法,并用数组法和指针法都将其实现。实践证明,此算法正确且时间复杂度低,学生容易理解且能建立字符串处理的编程思想。     

基于CBMC有界模型检测的无线抄表路由协议验证

针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法。WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证十分适用。CBMC能够直接对C/C++源码进行验证,这样不仅省去了传统模型检测技术需要对代码抽象建模的工作,而且不用担心模型和代码之间可能存在的不一致性问题。首先利用CBMC系统自生成断言验证技术,找到WM2RP协议实现中可能存在的漏洞,并对实现协议的公司给予反馈。然后进一步借助CBMC提供的用户自定义断言技术,通过自定义断言的插入以及对实现代码的适当处理,验证了WM2RP协议的网络层接收函数实现与协议规范的相符性。     

一种汇编程序的形式验证框架

在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查.     

Borland C＋＋与汇编语言之间指针的传递

C语言与汇编语言之间的接口是从事计算机软硬件人员应熟练掌握的一门技术指针是C语言中引入的重要概念之一,灵活地运用它可以使函数问参数的传递简单方便。本文仅以在科技开发工作中总结出来的具体实例说明Borland C 与汇编语言之间指针传递的几种方式。所给例程均已在IBM386上运行通过。1.整型近指针的传递,返回整型值近指针的情况     

一种基于指针逻辑的代码安全属性分析方法

在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法.该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结果对源代码中的指针进行替换,从而避开了传统静态代码属性验证工具对指针处理功能太弱的瓶颈,可以实现对C语言中的部分指针及运算进行处理.     

基于断言的模拟矢量自动生成方法

VLSI模拟验证的一个关键问题是需要大量的模拟矢量来验证各种可能情况下设计的正确性.采用断言作为模拟验证的功能模型,提出和实现了一种基于断言的模拟矢量自动生成方法.针对要触发的断言,首先对设计进行化简,通过决策图模型将初始输入传播到断言,并将传播过程和断言条件一起转化成CLP约束,最后求解CLP约束生成模拟矢量.该方法的优势在于运用了字级(word-level)约束求解技术,能统一处理控制电路和数据通路间的数据传播,求解效率高;基于功能模型的模拟矢量生成技术,模拟矢量生成目标更明确;与动态加速技术相结合,使搜索过程效率更高;设计化简技术的运用使搜索过程计算复杂度只与断言有关.实验结果表明,该方法能快速找到并定位设计中的错误,生成模拟矢量效率更高.     

一种寻找测试值断言证明程序正确的方法

程序正确性证明采用程序调试虽然有利于检测程序的错误,但不能保证程序是正确的;采用程序验证虽然可以证明程序正确,但困难之处在于用户必须提出一系列的中间断言作为验证条件,而寻找这组中间断言是最困难的,也是程序验证的关键。为此,本文讨论对程序的静态分析产生的解的不变式与动态测试所获得的测试值相符合的方法,以此导出程序正确性的证明。这样既避免了程序验证所须的证明一组验证条件的长而使人腻烦的工作,也避免了程序调试必须选择样品调试数据的较难克服的困难。     

Proving the Correctness of Multiprocess Programs

The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs. Individual processes are represented by ordinary flowcharts, and no special synchronization mechanisms are assumed, so the method can be applied to a large class of multiprocess programs. A correctness proof can be designed together with the program by a hierarchical process of stepwise refinement, making the method practical for larger programs. The resulting proofs tend to be natural formalizations of the informal proofs that are now used.     

Redundant proofs of non-interference in Levin-Gries CSP program proofs

Summary The proof system for Hoare's CSP language proposed by Levin and Gries requires that non-interference be proven for each assertion used in the proof of a process. In the worst case, the effort required to provide such proofs could be enormous. The need for these proofs has been identified as a significant weakness of the system. In this paper, we show that most of the proofs of non-interference required are unnecessary. This suggest that proving non-interference in the Levin-Gries system may be far less burdensome than had previously been assumed.     

A pointer logic and certifying compiler

Proof-Carrying Code brings two big challenges to the research field of programming languages. One is to seek more expressive logics or type systems to specify or reason about the properties of low-level or high-level programs. The other is to study the technology of certifying compilation in which the compiler generates proofs for programs with annotations. This paper presents our progress in the above two aspects. A pointer logic was designed for PointerC (a C-like programming language) in our research. As an extension of Hoare logic, our pointer logic expresses the change of pointer information for each statement in its inference rules to support program verification. Meanwhile, based on the ideas from CAP (Certified Assembly Programming) and SCAP (Stack-based Certified Assembly Programming), a reasoning framework was built to verify the properties of object code in a Hoare style. And a certifying compiler prototype for PointerC was implemented based on this framework. The main contribution of this paper is the design of the pointer logic and the implementation of the certifying compiler prototype. In our certifying compiler, the source language contains rich pointer types and operations and also supports dynamic storage allocation and deallocation.     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

Derivation of data intensive algorithms by formal transformation:the Schnorr-Waite graph marking algorithm

Considers a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program control information with other data structures or which are developed as a combination of a basic idea with an implementation technique. Our approach is based on applying proven semantics-preserving transformation rules in a wide spectrum language. Starting with a set theoretical specification of “reachability”, we are able to derive iterative and recursive graph marking algorithms using the “pointer switching” idea of Schorr and Waite (1967). There have been several proofs of correctness of the Schorr-Waite algorithm, and a small number of transformational developments of the algorithm. The great advantage of our approach is that we can derive the algorithm from its specification using only general-purpose transformational rules, without the need for complicated induction arguments. Our approach applies equally well to several more complex algorithms which make use of the pointer switching strategy, including a hybrid algorithm which uses a fixed length stack, switching to the pointer switching strategy when the stack runs out     

lcc.NET: targeting the .NET Common Intermediate Language from Standard C

The core of the Microsoft .NET platform includes a new virtual machine (VM), the Common Intermediate Language, also known as MSIL. Unlike most other VMs, including the Java VM, MSIL is specifically designed to support a wide range of languages. While it is designed primarily for type‐safe, object‐oriented languages, it also has facilities that support both low‐level languages and very high‐level languages. For example, it accommodates unsafe pointer arithmetic and tail calls. This paper describes the implementation of a MSIL back end for lcc, a retargetable compiler for Standard C. C is at one end of the range of languages that MSIL intends to support and lcc is just about the simplest ‘real’ C compiler that is widely available. Porting lcc to MSIL thus provides a realistic test of how well MSIL supports this class of languages and provides a glimpse at its performance costs. This effort succeeded, but static initializations, function pointers, separate compilation and address arithmetic were major problem areas. These problems also suggested improvements to lcc's code‐generation interface and they exposed a long‐standing error in the lcc front end. Preliminary measurements suggest that programs compiled by the MSIL back end run two to three times slower than those compiled by lcc native Intel x86 back end, but the MSIL programs have some important diagnostic benefits. Copyright © 2003 John Wiley & Sons, Ltd.     

Accurate garbage collection in uncooperative environments revisited

Implementing a concurrent programming language such as Java by means of a translator to an existing language is attractive as it provides portability over all platforms supported by the host language and reduces development time—as many low‐level tasks can be delegated to the host compiler. The C and C++ programming languages are popular choices for many language implementations due to the availability of efficient compilers on a wide range of platforms. For garbage‐collected languages, however, they are not a perfect match as no support is provided for accurately discovering pointers to heap‐allocated data on thread stacks. We evaluate several previously published techniques and propose a new mechanism, lazy pointer stacks, for performing accurate garbage collection in such uncooperative environments. We implemented the new technique in the Ovm Java virtual machine with our own Java‐to‐C/C++ compiler using GCC as a back‐end compiler. Our extensive experimental results confirm that lazy pointer stacks outperform existing approaches: we provide a speedup of 4.5% over Henderson's accurate collector with a 17% increase in code size. Accurate collection is essential in the context of real‐time systems, we thus validate our approach with the implementation of a real‐time concurrent garbage collection algorithm. Copyright © 2009 John Wiley & Sons, Ltd.     

基于悬浮指针的软件脆弱性分析及防范技术

悬浮指针（Dangling Pointer）是指代码中已被释放,但仍然可能被访问的对象指针。悬浮指针漏洞是指由于程序访问了悬浮指针所指向的地址而引起的软件脆弱性。为了提高程序的安全性,及时发现并防范程序中可能存在的安全漏洞,对基于悬浮指针的漏洞进行了比较全面的分析。主要讨论了漏洞成因、漏洞特点、利用原理、分析了利用ECX、利用Look＆sides链表的悬浮指针漏洞利用方法。最后,针对利用此类漏洞的特点提出了几点防范检测设想。     

Passing dynamic objects by reference in Fortran 90: application to time-dependent quantum chemistry

A new effective strategy of passing large variable size objects to subroutines and back in fortran 90 is described. The objects are passed by reference utilizing user-defined pointer type variables declared in a shared module. The efficiency of the developed approach is demonstrated by applying it to program the analytic solution for action of the powers of Hamiltonian on the Hermite polynomial type basis function.     

Live sequence charts applied to hardware requirements specification and verification

Techniques and tools for formally verifying compliance with industry standards are important, especially in System-on-Chip (SoC) designs: a failure to integrate externally developed intellectual property (IP) cores is prohibitively costly. There are three essential components in the practical verification of compliance with a standard. First, an easy-to-read and yet formal specification of the standard is needed; we propose Live Sequence Charts (LSCs) as a high-level visual notation for writing specifications. Second, assertions should be generated directly from the specification; an implementation will be scrutinized, usually by model checking, to check that it satisfies each assertion. Third, a formal link must be made between proofs of assertions and compliance with the original specification. As an example, we take the Virtual Component Interface (VCI) Standard. We compare three efforts in verifying that the same register transfer level code is VCI-compliant. The first two efforts were manual, while the third used a tool, lscAssert, to automatically generate assertions in LTL. We discuss the details of the assertion generation algorithm.