基于抽象解释的服务间消息的数据约减

面向服务软件中服务间消息的变量值可能存在无穷域的情况,从而导致模型检测时产生状态空间爆炸问题。为了使终止性验证在实践上可行,需要约减模型状态空间的大小,使得计算时间和空间需求合理。为此,基于抽象解释的区间抽象理论扩展了经典区间抽象域方法,并在统一的区间抽象域方法上借助异常控制流图对变量进行区间分析,在此基础上逆向分析得到服务间消息的变量区间集。变量区间上任意值相对于终止性验证是等价性,因此从每一个变量区间集中选取一个代表值,可组成服务间消息变量的约减值,从而为异常处理的终止性验证提供了约减的初始配置,有效避免了状态空间爆炸。     

基于层次单元划分的软件模型检测技术研究

通过对近年来软件模型检测领域流行的几种技术进行综述,提出了一种基于层次单元划分,使用引导式搜索方式的软件模型检测方案。本方案分为预处理、单元划分、状态空间搜索三个阶段,其中使用on-the-fly技术提高了搜索性能。实验证明,该方案在解决状态爆炸问题上有较好的效果。     

基于抽象和组合方法的网络协议验证

由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。     

一种基于Petri网的隐蔽信息流分析方法

隐蔽信息流分析是开发高等级可信计算机系统必须面对的问题.以Petri网作为开发安全系统的形式化建模工具,给出Petri网中隐蔽信息流存在的判定条件.提出该条件成立的两种网结构,进而可以在语法层次上预先判断隐蔽信息流的存在性,并使由此类结构引起的隐蔽信息流在系统的设计阶段得以避免.开发了一种基于Petri网可达图的隐蔽信息流存在性判定算法,算法遵循无干扰方法的思想,但是避免了无干扰方法中等价状态的区分和展开定理的使用.另外,算法采用深度优先搜索的策略,避免了Petri网全局可达图的构造.对复杂的安全系统,分析了子系统的各种组合运算对隐蔽信息流存在性的影响,降低了大规模系统分析的复杂度.     

一种基于状态扩展的安全协议验证机制

基于模型检测验证协议的方法存在状态空间爆炸问题,其中基于目标绑定搜索状态空间的方法有效控制了状态空间,但不能完全给出协议的运行情况。针对这一问题,提出了一种基于状态扩展的安全协议自动化验证机制,首先对协议状态进行初始搜索,给出协议运行需要的事件,得到协议基本状态,然后进行扩展搜索,考虑基本状态与其他协议运行的关系,形成协议扩展状态。该机制能够有效反映出协议的运行情况,且能够同时对多种安全性质进行验证。     

基于广义污点传播模型的操作系统访问控制

动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalized taint propagation model,简称GTPM),它继承了污点传播在最小权限方面的特点,拓展了污点传播语义,以试图关闭已知隐蔽通道,引入了主体的降密和去污能力以应对污点积累;还利用通信顺序进程(CSP)语言描述了模型的规格,以明确基于GTPM的操作系统的信息流控制行为的形式化语义;基于CSP的进程等价验证模型定义了可降密无干扰,并借助FDR工具证明形式化构建的抽象GTPM系统具有可降密无干扰安全性质.最后,通过一个示例分析了模型的可用性提升.     

安全协议自动验证工具的状态空间剪枝

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。     

模型检测中虚假反例检测方法

抽象技术是解决模型检测状态空间爆炸的一种有效方法,但其中一个重大的障碍是对系统的抽象会引入原始系统中本来不存在的行为,即可能会引入虚假反例。因此,需要根据反例对抽象模型进行精化。如何判定一个反例是虚假反例还是真实反例,在抽象精化过程中相当重要。本文根据状态的前驱和后继定义失效状态,给出虚假反例的定义,并基于此提出检测虚假反例的并行算法。     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题。针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法。根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型。利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例。实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题。     

The SH-Verification Tool — Abstraction-Based Verification of Co-operating Systems

The sh-verification tool comprises computing abstractions of finite-state behaviour representations as well as automata and temporal logic based verification approaches. To be suitable for the verification of so called co-operating systems, a modified type of satisfaction relation (approximate satisfaction) is considered. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not abstracted) behaviour. The well known state space explosion problem is tackled by a compositional method combined with a partial order method. Received March 1997 / Accepted in revised form July 1998     

基于抽象和搜索空间划分的安全性判定方法

为满足访问控制策略安全性快速判定的要求,提出一种基于谓词抽象和验证空间划分的访问控制策略状态空间约减方法,将在访问控制策略原始状态机模型上的安全性分析工作转移到包含较少状态的抽象模型上,并进一步划分抽象模型的验证空间,以提高效率。理论分析和实验数据均表明,其安全性分析所需的时间和空间都得到有效约减。与传统方法相比,它具有速度更快、自动化程度更高等优点。     

Abstraction and composition: a verification method for co-operating systems

Behaviour of systems is described by formal languages: the sets of all sequences of actions. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not abstracted) behaviour. To be suitable for verification of so called co-operating systems, a modified type of satisfaction relation for system properties (approximate satisfaction) is considered. The well known state space explosion problem is tackled by a compositional method formalized by so called co-operation products of formal languages.     

基于分段模型检测的云服务跨域认证协议的形式化分析与验证

针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。     

A practical data-flow verification scheme for business processes

Data in business processes becomes more and more important. Current standard languages for process modeling like BPMN 2.0 which include the data flow reflect this. Ensuring the correctness of the data flow in processes is challenging. Model checking, i.e., verifying properties of process models, is a well-known technique to this end. An important part of model checking is the construction of the state space of the model. However, state-space explosion typically is in the way of an effective verification. We study how to overcome this problem in our context by means of reduction. More specifically, we propose a reduction on the level of the process model. To our knowledge, this is new for the data-flow analysis of processes. The core of our approach are so-called regions of the process model that are relevant for the verification of properties describing the data flow. Non-relevant regions are candidates for reduction of the process model, yielding a smaller state space. Our evaluation shows that our approach works well on industrial process models.     

An iterative approach to verification of real-time systems

Verification of real-time systems is a complex problem, requiring construction of aregion automaton with a state space growing exponentially in the number of timing constraints and the sizes of constants in those constraints. However, some properties can be verified even when some quantitative timing information is abstracted. We propose a new verification procedure, where increasingly more complex abstractions of the region automaton are iteratively constructed. In many cases, the procedure can be stopped early, and thus can avoid the state space explosion problem.     

Distributed Explicit Bounded LTL Model Checking

Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method  model checking  is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour.     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

Uppaal到PVS的时间自动机翻译器

Uppaal是一种对实时系统模型进行建模和验证的工具,PVS（Prototype Verification System）是开发和分析形式化规格说明的原型证明系统。介绍了Uppaal2PVS翻译器的设计与实现,给出了一种将用Uppaal生成的时间自动机规格说明翻译成PVS文件的方法,从而将模型检查问题转换成了定理证明问题,解决了潜在的状态空间爆炸问题。最后给出了一个实例。