处理指针相等关系不确定的指针逻辑

为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质　证明.     

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

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

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

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

一种用于指针程序的形状分析方法

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

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

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

一种基于集合符号的自动推理扩展方法

在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.     

一阶逻辑知识库的检测

本文提出的方法是以Loveland的MESON一阶逻辑定理证明过程为基础,用于一阶逻 辑规则知识库的冗余性和不一致性的检测.知识库的规则可包含非真、或及if-and-only-if 规则.系统以交互形式从正、反向推理研究知识库规则增加时的变化.     

动态描述逻辑推理的并行计算技术

在设计用于处理大规模本体和数据的推理引擎时,推理引擎的可扩展性是一个需要研究的重要问题.动态描述逻辑要在真实环境中获得成功应用,需要在推理中采用并行计算技术.提出了两种方法将并行计算技术应用于动态描述逻辑推理.方法1是设计分布式动态描述逻辑框架.分布式动态描述逻辑由若干独立的动态描述逻辑所组成,这些动态描述逻辑两两之间通过桥规则联系起来.提出了基于Tableau的分布式推理算法,从而为分布式动态描述逻辑提供了全局推理能力,并且该算法可以将大的推理任务分解为若干子任务,而这些子任务可以被不同的推理主体并行处理.方法2是并行化动态描述逻辑的Tableau算法的不确定分支.不确定分支的并行计算使得推理任务可以在若干独立机器上同时执行.最后,介绍了推理引擎的原型实现并评估了其性能.实验结果表明提出的两种方法取得了明显的推理加速效果.     

扩展AL-log挖掘日志本体的ILP方法

为发现Web使用记录中所蕴涵的用户访问模式,在深入分析日志本体中事件间的抽象关系后,提出适用于原子事件和复合事件间整分关系推理的ALC传播规则扩展已有的推理模式,并在此基础上提出一种挖掘日志本体的ILP方法.该方法结合描述逻辑和Horn规则在知识表示和推理过程中互补的特点,采用AL-log混合系统构建知识库,利用约束SLD-反驳消解和扩展ALC传播规则从日志本体中学习用户访问模式,达到站点商业智能和个性化的目的.最后给出验证该方法的实例,实验结果表明了该方法的可行性和有效性.     

基于指针映射集的动态内存故障测试方法研究

动态内存故障在使用指针的程序中是普遍存在的,采用动态测试方法进行测试难以准确定位故障源.而现有的静态分析方法主要存在漏报和误报过多的情况.针对这些问题,提出了指针映射代数系统的概念,全面地反映了指针与内存之间的映射关系,并给出了面向不同故障的指针映射集的构造规则,以此为基础建立了动态内存故障模型.通过指针映射集和故障模型,可以自动检测内存释放异常、内存泄露和空指针引用等动态内存故障,提高了测试效率.在分析过程中,还综合应用了控制流图和路径条件,提高了测试结果的精度.实验结果表明,该方法能够有效检测动态内存故障,而且出于规则定义较为全面,漏报和误报率也较低.     

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.     

两维时间域上的一种区间逻辑

为了给超稠密计算模型建立一种逻辑工具,首先定义了一个两维的超稠密时间域,在这个时间域上定义了一种区间逻辑,并提出了该逻辑的一个推理系统。并用轨道概念定义了两维超稠密空间中的计算,最后讨论了一些相关的问题。     

基于污点指针的二进制代码缺陷检测

污点指针严重影响二进制代码数据流和控制流的安全。为此,提出一种二进制代码缺陷检测方法。引入指针污点传播规则,结合路径约束条件和边界约束条件得到缺陷引发条件,构造能够引发4类污点指针代码缺陷的输入数据。在Linux系统下实现ELF二进制代码缺陷检测工具,测试结果表明,该方法能降低测试用例生成数量,并发现Linux系统工具的1个虚函数调用控制缺陷和2个指针内存破坏缺陷。     

分层格值命题逻辑系统中几类推理规则的讨论

在基于格值逻辑的不确定性推理的研究中,推理规则的选取是其重要研究内容之一。基于分层格值命题逻辑系统,提出了几类既包含有语义又含有语法的推理规则,且这些推理规则具备协调水平的特性;同时也证明了这几类推理规则在一定程度上有闭性。     

服务组合中基于线性逻辑的消息语义匹配

介绍一种自动服务组合模型服务消息语义化匹配验证的方法。该方法先从服务描述中提取服务消息模型和服务行为模型,后将服务行为模型转换为形式化的有限状态自动机。根据有限状态自动机中的服务接口可以转化为本体概念,服务行为可以转换为线性逻辑表达式描述,使用线性逻辑的演绎方法对服务消息的匹配性和可满足性进行验证。同时,对线性逻辑的演绎定理进行适当扩展以适应服务组合的需要。     

面向分层移动IPv6 网络的动态指针推进机制

基于指针推进机制的分层移动IPv6方案因未考虑移动锚点管理域的影响,导致较高的注册和报文分发开销.提出一种面向分层移动IPv6网络的动态指针推进机制(dynamic pointer forwarding scheme for HMIPv6 networks,简称DPF-HMIPv6),移动节点可根据所选移动锚点的管理域大小,动态调整指针推进机制.若所选移动锚点的管理域大于特定阈值,则移动节点通过在接入路由器间构建指针链来避免频繁地向移动锚点注册;若所选移动锚点的管理域小于阈值,则移动节点通过在移动锚点间构建指针链来避免频繁地向家乡代理注册.数值分析和仿真实验的结果表明,该方案能够有效解决现有方案存在的问题,显著降低分层移动IPv6网络的开销.