基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具.这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测.但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全.为了解决这些问题,文中提出...     

基于Coq的微内核操作系统程序验证方法研究

机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题;基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术;文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开展程序验证技术研究,根据霍尔逻辑的相关推理规则进行程序验证,并在定理证明辅助工具Coq中形式化表示霍尔逻辑的推理规则,针对机载操作系统的部分程序代码实例进行验证;实验结果表明基于定理证明的程序验证方法可以对软件程序代码的正确性进行验证,从而帮助软件提供商开发高可信的机载嵌入式软件。     

基于程序运行形式化分析的软件故障监控技术

关键软件要求极高的可靠性和安全性,然而当前的技术途径尚不能完全消除软件故障——软件测试不能保证软件正确性,模型检查等形式化验证技术也存在着诸多局限。文章提出了基于监控程序运行途径来捕获软件故障和验证程序性质正确性,构建了基于程序运行形式化分析的软件故障监控（SFMRFA）模型,在监控逻辑表达、程序插桩、multi-agent设计等关键技术的基础上开发计算机辅助工具来监控、分析和引导程序执行,使软件运行当中可测、可控,避免软件失效。     

面向程序分析的插桩技术研究

为了满足测试覆盖分析和软件调试等程序分析技术对插桩技术的需求,提出了插桩模型,开发了一款实用的插桩工具。基于双缓冲技术,构建词法分析器和语法分析器。在语法分析归约时同步收集插桩信息,然后根据插桩策略执行插桩,生成目标文件。得到的程序运行时信息被应用于影响广泛的四种软件自动调试分析方法。对于这四种方法。缺陷语句均被准确识别为最可疑语句。应用结果表明,该方法能够为准确高效的程序分析提供必要的运行时信息。     

基于性能分析的自适应插桩框架

插桩技术用于跟踪获取软件系统的运行时信息,是软件性能管理工具中不可或缺的一个部分。目前,存在的各类插桩工具所产生的插桩点在目标程序运行的过程中往往是不可改变的。在实际的程序异常、错误检测中,用户关心的程序代码的位置在不同阶段往往不同,因此目标程序运行的不同阶段所需要获取信息的插桩点位置是不同的,如果插桩点过多会导致插桩工具浪费系统资源,产生系统资源消耗过大的问题;插桩点过少则会导致无法准确定位目标软件发生异常位置。针对以上问题,使用基于线性回归和K-Means的分析模型,分析目标软件的性能数据,在其运行过程中动态地改变插桩点,尽可能的减少资源的消耗;另外,采用朴素贝叶斯分类模型对插桩类进行筛选,减少植入插桩点的类,可降低插桩带来的资源消耗。实验表明：与传统的工具相比,使用此插桩框架进行监控,被测网页的平均响应时间减少6.88%,同时对目标程序的干扰更小。     

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

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

一个基于Mathematica平台的程序安全性自动验证工具

程序安全性验证是程序验证的重要部分。基于不变式生成,将程序的安全性验证转化为验证不变式集合是否蕴含表示安全性的逻辑公式。针对简化的C程序,结合验证工具Theorema,在Mathematica平台上实现一个对程序安全性进行自动验证的工具。实验结果表明,该验证工具能够自动验证只含数值变量的C程序。     

一个基于Eclipse的通用Java程序插桩工具

插桩技术作为一种有效理解程序动态行为的手段,已经被广泛应用于程序分析、测试和验证中。然而,由于缺少通用的插桩工具,各种具体的应用往往需要从头开发特定的插桩程序,存在着大量的重复性工作。此外,由于在原始程序中插入了大量额外代码,致使调试过程变得更加复杂和困难。针对这些问题,提出了一个基于Eclipse的通用Java代码插桩工具,即通过规则定义匹配程序的执行点,从而定制针对各种分析、测试和验证插桩需求的支持。通过对插桩代码片段的显式/隐式切换实现其可见性管理,从而确保程序的理解和调试过程不受插桩代码影响。通过使用该工具,可以更好地将插桩技术应用于Java程序开发中。     

基于路径覆盖插桩的可执行代码测试工具实现

为解决传统程序插桩技术存在代码膨胀和运行时间较长的问题,提出对可执行代码进行控制流路径覆盖消除冗余的插桩策略。依据该策略设计一种针对Java可执行代码的单元测试工具,完成程序执行路径跟踪和覆盖率分析。对测试工具进行功能验证和性能分析,结果表明,该策略能够有效减少插桩点数量,降低插桩对被测程序时间特性的影响。     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

基于分离逻辑的程序验证研究综述

上世纪60-70年代以来,虽然有Floyd-Hoare逻辑的出现,但是使用形式化工具对命令式程序的正确性和可靠性进行自动验证一直被认为是极具挑战性、神圣不可及的工作.上世纪末由于更多的科研投入,特别是微软、IBM等大型公司研发部门的大量人力物力的投入,程序验证方面在本世纪初取得了不少进展,例如用于验证空客代码无运行时错误的ASTRÉE工具,用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆（Heap）：ASTRÉE工具假设待验证代码没有动态创建的堆,也没有递归;SLAM假设待验证系统已经有了内存安全性.事实上很多重要的程序,例如Linux内核、Apache、操作系统设备驱动程序等等,都涉及到对动态创建堆的操作.如何对这类操作堆的程序（heap-manipulating programs）进行自动验证仍然是个难题.2001-2002年分离逻辑（separation logic）提出后,其分离（separation）思想和相应的框（frame）规则使得局部推理（local reasoning）可以很好地应用到程序验证中.自2004年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如SpaceInvader/Abductor、Slayer、HIP/SLEEK、CSL等工作.本文将着重对这方面的部分重要工作进行阐述.     

动态存储管理安全验证的Coq实现

随着软件规模和复杂度的日益提升,软件安全的问题变得越来越严峻,同时有越来越多的研究工作集中在高可信软件的开发上 .由于类型系统表达能力的不足,现有的研究不触及底层软件的验证 .由于Hoare逻辑更好的表达能力,采用Hoare逻辑风格的推理,在汇编语言级别,使用Coq形式化与定理证明工具可以实现一个经过安全验证的动态存储管理函数库,这是程序验证技术一次有意义的实践 .实践表明,程序验证技术可以应用到高可信软件的开发上 .     

An Overview of the Runtime Verification Tool Java PathExplorer

We present an overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution of a Java program and check that it conforms with a set of user provided properties formulated in temporal logic. JPAX can in addition analyze the program for concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided specification. The tool facilitates automated instrumentation of a program's bytecode, which when executed will emit an event stream, the execution trace, to an observer. The observer dispatches the incoming event stream to a set of observer processes, each performing a specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic, where Maude is a high-speed rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated as an event driven monitoring process. Alternatively, temporal specifications can be translated into automata or algorithms that can efficiently check the event stream. JPAX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems.     

基于隔离逻辑的并行程序可靠性验证方法

并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。     

Monitoring method call sequences using annotations

In this paper we introduce JMSeq, a Java-based tool for monitoring sequences of method calls. JMSeq provides a simple but expressive language to specify the observables of a Java program in terms of sequences of possibly nested method calls. Similar to many monitoring-oriented environments, verification in JMSeq is done at runtime; unlike all other approaches based on aspect-oriented programming, JMSeq uses code annotation rather than instrumentation, and therefore is suitable for component-based software verification.     

Efficiently solving quantified bit-vector formulas

In recent years, bit-precise reasoning has gained importance in hardware and software verification. Of renewed interest is the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifier-free fragment of bit-vector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bit-vector formulas to avoid an exponential blow-up during construction. Solvers for quantified formulas usually flatten the input to obtain a quantified Boolean formula, losing much of the word-level information in the formula. We present a new approach based on a set of effective word-level simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on skeletons/templates. Experimental results on two different types of benchmarks indicate that our method outperforms the traditional flattening approach by multiple orders of magnitude of runtime.     

C程序数组越界的运行时验证技术研究与实现

缓存区溢出能引起非常严重的安全问题,对网络和分布式系统（如机群,网格,P2P系统等）构成严重威胁。数组越界在缓存区溢出中占据重要位置,如何检测数组越界错误是一个重要且极具意义的课题。针对该课题,给出一种对C语言数组越界进行运行时验证的方法。分析了数组越界的错误类型,根据这些类型分别研究了数组越界的运行时验证的思想;设计了基于程序插桩进行数组越界动态检测的算法,给出了该方法基于开源编译器Clang的具体实现;用实验证明了该方法是切实可行并且有效的。     

步进索引模型下的语义及其形式化

霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.     

Model-based monitoring and policy enforcement of services

Runtime monitoring is necessary for continuous quality assurance of Web Services. Sensors are critical in runtime monitoring to capture the data and detect anomalies. However, sensors in current monitoring systems are usually manually instrumented or hard-coded in the program. It is expensive to implement, and inflexible to change at runtime. The paper extends our previous research on collaborative monitoring and proposes a model-based approach for automatic generating sensors and enforcing policies. Web Services standards WSDL and OWL-S are taken as the models of service interface, workflow, and semantic. Sensors are generated based on the models from two perspectives: (1) dependency analysis of the data, operations, and services with respect to the ontology model of domain concepts and usage context; (2) coverage strategies to decide the specific logic and paths to cover and the data to capture by the monitoring sensors. Policies are defined as a 3-tuple of type, subject and assertion sets and are specified using WS-Policy standards. They are associated to the sensors and enforced at runtime by the policy engine that interoperates with service execution engine to communicate runtime behavior information and verification results. Prototype system is implemented based on the Eclipse platform where sensors are implemented as the listeners to the process execution and instrumented into the middleware including the OWL-S execution engine and SOAP engine. Experiments show that the monitoring results in low overhead of the system performance, reduced effort and enhanced flexibility of sensor instrumentation.