一种用于指针程序安全性证明的指针逻辑 被引量：20

1

作者 陈意云 华保健 +1 位作者 葛琳 王志芳 《计算机学报》 EI CSCD 北大核心 2008年第3期372-380,共9页

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

关键词 软件安全 指针逻辑 hoare逻辑 指针分析 类型系统

下载PDF 职称材料

一个程序验证器的设计和实现 被引量：11

2

作者 张志天 李兆鹏 +1 位作者 陈意云 刘刚 《计算机研究与发展》 EI CSCD 北大核心 2013年第5期1044-1054,共11页

形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状... 形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质. 展开更多

关键词 程序验证 hoare逻辑 形状图逻辑 程序分析 分离逻辑

下载PDF 职称材料

安全语言PointerC的设计及形式证明 被引量：8

3

作者 华保健 陈意云 +3 位作者 李兆鹏 王志芳 葛琳 江苏苏州215123 《计算机学报》 EI CSCD 北大核心 2008年第4期556-564,共9页

程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(sid... 程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的. 展开更多

关键词 软件安全 语言设计 类型系统 hoare逻辑 指针逻辑

下载PDF 职称材料

一种用于指针程序验证的指针逻辑 被引量：6

4

作者 陈意云 李兆鹏 +1 位作者 王志芳 华保健 《软件学报》 EI CSCD 北大核心 2010年第3期415-426,共12页

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便... 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合. 展开更多

关键词 软件安全 hoare逻辑 指针逻辑 携带证明的代码 出具证明的编译器

下载PDF 职称材料

一种基于规则的语言的公理语义 被引量：2

5

作者 魏振春 韩江洪 +1 位作者 陆阳 刘小平 《计算机工程与应用》 CSCD 北大核心 2008年第20期86-88,共3页

为了准确描述离散事件控制系统对象之间的逻辑关系和编写控制程序,提出了一种基于规则的语言——逻辑规则描述语言(LRDL)。用EBNF给出了LRDL的语法定义,基于Hoare逻辑的公理系统,形式化地给出并证明了LRDL的公理语义,为用LRDL编写的程... 为了准确描述离散事件控制系统对象之间的逻辑关系和编写控制程序,提出了一种基于规则的语言——逻辑规则描述语言(LRDL)。用EBNF给出了LRDL的语法定义,基于Hoare逻辑的公理系统,形式化地给出并证明了LRDL的公理语义,为用LRDL编写的程序的正确性证明提供了理论依据。 展开更多

关键词 规则 逻辑规则描述语言 公理语义 hoare逻辑 形式语法

下载PDF 职称材料

程序正确性证明及循环不变式的寻找方法 被引量：2

6

作者 王彩芬 《甘肃科学学报》 2000年第3期43-48,共6页

重点讨论了与程序验证相关的问题 ,并结合已有的求取循环不变式的方法给出了求已知循环程序的循环不变式的原则。

关键词 程序验证 hoare逻辑 循环不变式 程序正确性

下载PDF 职称材料

UML活动图的一种逻辑语义 被引量：4

7

作者 林添荣 蒋建民 《福建师范大学学报（自然科学版）》 CAS CSCD 北大核心 2010年第3期26-30,39,共6页

为使UML活动图在软件过程中精确地建模系统,必须给出它的形式语义.首先将UML活动图形式化为一个关系结构,其次用Hoare逻辑给出了它的语义表示,最后讨论了该语义的若干性质,并用一个实例来说明.

关键词 UML活动图 软件过程 形式语义 hoare逻辑

下载PDF 职称材料

一种汇编程序的形式验证框架 被引量：3

8

作者 李兆鹏 陈意云 +1 位作者 葛琳 华保健 《计算机研究与发展》 EI CSCD 北大核心 2008年第5期825-833,共9页

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

关键词 软件安全 出具证明编译器 指针逻辑 hoare逻辑 携带证明的汇编程序

下载PDF 职称材料

断言语言支持自定义谓词的程序验证器原型 被引量：3

9

作者 徐文义 陈意云 李兆鹏 《小型微型计算机系统》 CSCD 北大核心 2013年第7期1482-1486,共5页

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

关键词 程序验证 hoare逻辑 形状图逻辑 程序分析 自定义谓词

下载PDF 职称材料

程序断言的半自动生成及证明逻辑 被引量：3

10

作者 何锫 康立山 《计算机工程与应用》 CSCD 北大核心 2008年第14期18-20,30,共4页

如何生成程序断言对于软件验证十分重要。传统方法要求既要对程序结构有深入地把握又要做繁复的Hoare三元式推演工作。为了摆脱这些琐碎事宜,将致力于探讨一种半自动的断言生成方法。为便于理解,讨论主要以XYZ/VERI系统为论述背景。XYZ/... 如何生成程序断言对于软件验证十分重要。传统方法要求既要对程序结构有深入地把握又要做繁复的Hoare三元式推演工作。为了摆脱这些琐碎事宜,将致力于探讨一种半自动的断言生成方法。为便于理解,讨论主要以XYZ/VERI系统为论述背景。XYZ/VERI系统是一面向时序逻辑程序语言如XYZ/SE的类Hoare逻辑交互式验证系统。该工作一定意义上完善了其验证功能。 展开更多

关键词 hoare逻辑 序验证 程序断言 XYZ/VERI

下载PDF 职称材料

[α_1,α_2]1-概率拟Hoare逻辑及其可靠性证明

11

作者 吴新星 胡国胜 陈仪香 《计算机科学》 CSCD 北大核心 2015年第B11期93-99,共7页

基于C.A.R.Hoare提出的Hoare逻辑,给出了[α_1,α_2]1-概率拟Hoare逻辑,并证明了其可靠性。

关键词 hoare逻辑 hoare三元组 正确度 概率测度

下载PDF 职称材料

关于断言语言中引入逻辑变量的研究 被引量：2

12

作者 李为胜 罗奇鸣 陈意云 《小型微型计算机系统》 CSCD 北大核心 2017年第5期925-929,共5页

基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向.但是在Hoare逻辑中,仅依靠程序变量的断言语言无法表达程序上下文中不变性质.本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质,同时详... 基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向.但是在Hoare逻辑中,仅依靠程序变量的断言语言无法表达程序上下文中不变性质.本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质,同时详细介绍了引入逻辑变量带来的问题以及给出解决问题的途径,最后以带逻辑变量的平衡二叉树插入程序为例展示了引入逻辑变量的作用. 展开更多

关键词 hoare逻辑 形式化验证 逻辑变量 断言语言

下载PDF 职称材料

概率拟Hoare逻辑

13

作者 吴新星 胡国胜 陈仪香 《计算机科学》 CSCD 北大核心 2016年第4期177-181,191,共6页

基于Hoare逻辑,给出了概率拟Hoare逻辑,用于刻画程序执行的正确度,定量地描述理论与程序(或软件)实际执行之间的差距,反映理论被程序实现的程度,从而量化理论上正确的程序在实际执行时出错的可能性,以及解释正确度很高的两个程序串行复... 基于Hoare逻辑,给出了概率拟Hoare逻辑,用于刻画程序执行的正确度,定量地描述理论与程序(或软件)实际执行之间的差距,反映理论被程序实现的程度,从而量化理论上正确的程序在实际执行时出错的可能性,以及解释正确度很高的两个程序串行复合之后的整体正确度可能并不高等问题。 展开更多

关键词 hoare逻辑 hoare三元组 正确度 概率测度

下载PDF 职称材料

一种验证指针程序的方法 被引量：1

14

作者 张志天 陈意云 刘刚 《微型机与应用》 2011年第16期9-11,共3页

利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以便程序分析工具能建立各程序点的形状图,并以此来支持程序验证。探讨... 利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以便程序分析工具能建立各程序点的形状图,并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下,避免在Hoare逻辑上做复杂扩展的指针程序验证方法。 展开更多

关键词 hoare逻辑 形状图逻辑 程序分析 分离逻辑

下载PDF 职称材料

用HOARE逻辑证明C^(++)程序的正确性 被引量：1

15

作者 王彩芬 《兰州大学学报（自然科学版）》 EI CAS CSCD 北大核心 2000年第1期44-47,共4页

讨论了将HOARE逻辑应用于面向对象的程序设计语言C++程序的正确性证明的相关问题.

关键词 hoare逻辑 面向对象 程序设计

下载PDF 职称材料

一种 Hoare 逻辑软件复用部件的匹配描述 被引量：1

16

作者 胡和平 黄力芹 汪涛 《华中理工大学学报》 CSCD 北大核心 1997年第10期101-103,共3页

提出了一种基于Ｈｏａｒｅ逻辑的软件复用部件的匹配描述，它为建立复用部件库的检索机制以及软件的自动化生产提供了理论描述．

关键词 软件复用 hoare逻辑 复用部件 匹配 软件开发

下载PDF 职称材料

基于Hoare逻辑的过程调用的形式化方法 被引量：2

17

作者 雷富兴 张来顺 《计算机工程与设计》 CSCD 北大核心 2011年第1期197-201,共5页

采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这... 采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这个调用的前置条件,根据这些条件形式化求解调用的最强后置条件,也就是调用的语义作用。 展开更多

关键词 hoare逻辑 过程语义 过程调用语义 前置条件 后置条件

下载PDF 职称材料

栈指针程序的形式验证 被引量：2

18

作者 冯峰 罗奇鸣 陈意云 《小型微型计算机系统》 CSCD 北大核心 2017年第5期936-940,共5页

提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元... 提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元属性设计了相应的断言演算规则和演算过程中生成验证条件的方法.该方法可以解决访问路径别名判断、指针越界访问检查、非法指针解引用检查等问题.该方法已经在一个基于演绎推理的安全C语言验证系统中实现,并且成功验证了教材上常用的一些经典算法. 展开更多

关键词 程序验证 栈指针 静态区指针 路径别名 hoare逻辑

下载PDF 职称材料

基于Hoare逻辑的密码软件形式化验证系统 被引量：2

19

作者 郝耀辉 郭渊博 +1 位作者 罗婷 燕菊维 《计算机工程》 CAS CSCD 2012年第3期121-123,共3页

在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL中RC4算法的软件实现为例,对其功能正确性、保险性和信息流安全性进行验证,结果表... 在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL中RC4算法的软件实现为例,对其功能正确性、保险性和信息流安全性进行验证,结果表明,该系统具有较高的自动化水平,可在一定程度上降低形式化验证方法的复杂度。 展开更多

关键词 hoare逻辑 密码软件 形式化验证 程序规范 RC4算法

下载PDF 职称材料

一种用于指针程序的形状分析方法 被引量：1

20

作者 刘刚 胡凯平 宋发兴 《计算机与现代化》 2012年第4期82-85,共4页

指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻... 指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。首先介绍所提出的形状图和形状图逻辑;然后在此基础之上,设计一种基于形状图逻辑的形状分析方法。 展开更多

关键词 形状图 形状图逻辑 hoare逻辑 形状分析 程序分析

下载PDF 职称材料