可生存的存储系统模型及其体系结构研究*

本文首先提出了一种可生存性存储系统的形式化模型定义,后结合模型给出了可生存性存储系统的体系结构。为可生存存储系统的设计构造提供指导思想,并系统可生存性的衡量提供基本方法。     

嵌入式系统可生存性分析模型研究

嵌入式系统的安全问题日益凸显,为此,提出一种嵌入式系统可生存性分析模型。借鉴近年来国内外研究成果,给出嵌入式系统可生存性的形式化定义,建立系统威胁、系统可生存性需求、系统可生存性策略3个子模型对嵌入式系统可生存性进行分析,形成一套系统可生存性分析的一般流程。实例分析表明,该模型能定量评估嵌入式系统的可生存性,并通过评估结果得到影响系统可生存性的主要因素。     

可生存性分析方法研究

系统在受到入侵后依然能够提供必要服务,并在一定时间内恢复受侵害的服务是系统可生存性的本质要求,与传统的将可生存性作为非功能系统属性描述的方法不同,将可生存性作为系统统一系统功能来研究,并用形式化语言来描述,定义和计算是一种全的思路和方法,对可生存性分析阶段可以采用的方法进行了深入的研究,分析,其中重点阐述了工作流回溯,攻击树建立等可生存性需求分析的方法,并给出了可生存性量化分析的算法。     

可生存网络系统的形式化定义

本文从网络系统的可生存需求出发,借鉴了近年来国内外的可生存研究成果,提出了规范化的网络系统的可生存性定义,并给出其形式化的描述及其实现模型,为下一阶段的系统可生存性的定量分析提供统一、规范的可生存性定义。     

基于SPN的信息系统生存性分析建模研究

研究基于随机Petri网(SPN)的信息系统生存性分析建模方法.首先,将信息系统抽象为请求组件、通信组件、处理组件和存储组件4个部分;其次,将信息系统工作流程形式化描述和生存性分析建模相结合,并分别描述了通用信息系统、系统组件失效修复、串联并接、冗余以及具有可生存属性组件的随机Petri网建模方法.从而对系统形式化描述的同时对系统生存性能做了定性和定量分析;最后,仿真实验证明基于SPN建模方法分析信息系统生存性的有效性和准确性,并为可生存的信息系统设计提供理论基础和指导.     

一种改进的信息系统生存性分析研究

采用层次化结构设计了一种新的系统状态分析模型,该模型可以用来量化信息系统的生存性。将系统定义为一种以服务为中心的层次结构,将生存性测试划分为防护能力、检测能力和恢复能力三级。并在层次化模型基础上计算了系统的生存性。通过一个案例,说明了层次化系统生存性计算方法不仅可以有效避免对系统的状态进行直接定义和分析,而且使系统生存性分析支持实际操作及程序化。     

基于状态转换的信息服务系统可生存性评估方法

可生存性评估是使用各种方法对目标系统进行定性及定量的生存性分析。本文提出了一个基于状态转换的信息服务系统可生存性评估方法,该方法包括一个系统生存性模型和一个生存性函数的定义。最后给出了使用这种评估方法对目标系统进行评估的实例。     

网络可生存性定义研究

对已经提出的网络可生存性定义进行了分析与研究,归纳并总结了网络可生存性的关键要素,然后基于这些要素给出了一个网络可生存性的定义;在该定义的基础上,提出了更加精确、全面、利于实现的七元组的形式化定义,为网络可生存性需求分析、设计和实现提供理论框架,同时也为验证实现的系统是否满足可生存性定义了标准.     

增强可生存性的访问控制模型

针对传统访问控制模型应用到可生存系统时存在的局限性,提出可生存性访问控制的概念和要求,并设计一种可生存性访问控制模型TTC。TTC模型在系统受到入侵而被控制之后仍然能保护关键服务和数据,能实时响应入侵检测报警并指导入侵恢复工作。它包括触发、跟踪和控制等三个规则。触发规则和跟踪规则利用攻击树跟踪入侵者在系统内的活动,控制规则禁止被跟踪的主体破坏关键服务和数据。通过对模型的形式化证明,模型的应用示例,以及与传统访问控制模型的对比,证实了TTC模型在增强可生存性方面的价值。     

基于模型检查技术的信息系统生存性研究

在运用Jha方法进行信息系统生存性研究时,没有分析不同攻击场景与系统节点失效之间的关联性,也未考虑系统提供多个服务情形下的生存性分析。针对上述问题,提出运用模型检查技术评价系统生存性的改进算法,建立多攻击场景、多个服务情形下系统生存性的计算模型,实例分析证明其具有较好的适用性。     

并发反应式系统的组合模型检验与组合精化检验

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.     

ARINC653实时任务可调度性验证方法

针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方法,利用模型检验工具UPPAAL对IMA系统进行建模仿真,并结合统计模型检验(Statistical Model Checking,SMC)与符号模型检验(Symbolic Model Checking,MC)来验证其可调度性。实验结果表明,该方法不仅快速验证了IMA系统的可调度性,而且能够准确定位不可调度任务。     

多智体系统中约简状态空间的限界模型检测算法

为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.     

基于不可满足核的近似逼近可达性分析

近年来,形式化验证技术受到了越来越多的关注,它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支,具有十分广阔的发展前景.本文中我们研究并提出了一种新的模型检测技术,可以有效地对迁移系统进行模型检测,包括不安全性检测和证明安全性.与现有的模型检测算法不同,我们提出的这种方法——基于不可满足核（unsatisfiable core,UC）的近似逼近可达性分析（UC-based approximate incremental reachability,UAIR）,主要利用不可满足核来求解一系列的候选安全不变式直至生成最终的不变式,以此来实现安全性证明和不安全性检测（漏洞查找）.在基于SAT求解器的符号模型检测中,我们使用由可满足性求解器得到的UC构造候选安全不变式,如果迁移系统本身是安全的,我们得到的初始不变式只是安全不变式的一个近似.然后,我们在检查安全性的同时,逐步改进候选安全不变式,直到找到一个真正的不变式,证明系统是安全的;如果系统是不安全的,我们的方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法,我们利用不可满足核进行安全性模型检测,取得了相当好的效果.众所周知,模型检测领域没有绝对最好的方法,尽管我们的方法在基准的可解数量上无法超越当前的成熟方法例如IC3、CAR等,但是我们的方法却可以解出3个其他方法都无法解出的案例,相信本方法可以作为模型检测工具集很有价值的补充.     

一种有效的基于LTL和Petri网的模型检测方法

模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。     

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

随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题。形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术。形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类。文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证。     

UC-based Approximate Incremental Reachability

In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in safety-critical areas. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This study analyzes and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, Unsatisfiable Core (UC)-based Approximate Incremental Reachability (UAIR), mainly utilizes the UC to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, this study uses the UC obtained by the satisfiability solver to construct the candidate safety invariant, and if the transition system itself is safe, the obtained initial invariant is only an approximation of the safety invariant. Then, while checking the safety, the study incrementally improves the candidate safety invariant until it finds a true invariant that proves the system is safe; if the system is unsafe, the method can finally find a counterexample to prove the system is unsafe. The brand new method exploits UCs for safety model checking and achieves good results. It is known that there is no absolute best method in the field of model checking. Although the proposed method cannot surpass the current mature methods such as IC3 and complement Approximate Reachability (CAR), in terms of the number of solvable benchmarks, the method in this paper can solve three cases that other mature methods are unable to solve. It is believed that the method can be a valuable addition to the model checking toolset.     

基于属性的访问控制策略的正确性验证

基于属性的访问控制策略以更精确的粒度控制着用户或进程对系统资源的访问,因此获得了越来越广泛的应用。然而必须保证所制定策略的正确性,才能防止对系统资源的非法访问,因此必须研制出一种有效的方法来验证策略的正确性。基于模型检测技术提出了一种访问控制策略的覆盖性与完整性验证方法。主要思想是将覆盖性与完整性验证归约为模型检测问题。将规则集与其变异分别视为模型,以模态逻辑公式描述其性质。调用模型检测算法,分别在模型及其变异模型上检测性质,生成反例报告以确定模型故障点和模型规则缺失点,同时分析性质本身的完善性,最终以完善后的模型和性质再次调用模型检测算法来完成覆盖性与完整性验证。实例分析结果表明覆盖性验证能够有效发现错误的规则,完整性验证能够有效识别验证规则的完备性。方法依托于模型检测工具完成,具有自动化程度高、易操作、测试结果可靠的特点。     

计算树逻辑特性模式研究

模型检查是系统验证的有效方法,在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画,然后在模型检查工具中进行检验。介绍计算树逻辑的语法及语义,根据计算树逻辑中特性模式的划分及作用范围给出计算树逻辑常见的特性模式,包括缺失性模式、存在性模式、普遍性模式、优先性模式和跟随性模式等。