共查询到13条相似文献,搜索用时 78 毫秒
1.
2.
3.
软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证. 相似文献
4.
5.
程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的. 相似文献
6.
利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以便程序分析工具能建立各程序点的形状图,并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下,避免在Hoare逻辑上做复杂扩展的指针程序验证方法。Abstract: Analysis and verification of programs dealing with pointers are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems. Using our method, programmers must declare the shapes that the recursive data 相似文献
7.
8.
一种基于指针逻辑的代码安全属性分析方法 总被引:1,自引:0,他引:1
在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法.该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结果对源代码中的指针进行替换,从而避开了传统静态代码属性验证工具对指针处理功能太弱的瓶颈,可以实现对C语言中的部分指针及运算进行处理. 相似文献
9.
在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查. 相似文献
10.
如何生成程序断言对于软件验证十分重要。传统方法要求既要对程序结构有深入地把握又要做繁复的Hoare三元式推演工作。为了摆脱这些琐碎事宜,将致力于探讨一种半自动的断言生成方法。为便于理解,讨论主要以XYZ/VERI系统为论述背景。XYZ/VERI 系统是一面向时序逻辑程序语言如XYZ/SE 的类Hoare逻辑交互式验证系统。该工作一定意义上完善了其验证功能。 相似文献
11.
随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出.并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大.为此,提出一种基于分离逻辑的新的验证方法.该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值.实例进一步说明,此方法更有效,同时也简化了验证的规模. 相似文献
12.
介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向. 相似文献
13.
A pointer logic and certifying compiler 总被引:6,自引:0,他引:6
Chen Yiyun Ge Lin Hua Baojian Li Zhaopeng Liu Cheng Wang Zhifang 《Frontiers of Computer Science in China》2007,1(3):297-312
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. 相似文献