基于系统调用和齐次Markov链模型的程序行为异常检测

异常检测是目前入侵检测领域研究的热点内容.提出一种新的基于系统调用和Markov链模型的程序行为异常检测方法,该方法利用一阶齐次Markov链对主机系统中特权程序的正常行为进行建模,将Markov链的状态同特权程序运行时所产生的系统调用联系在一起,并引入一个附加状态;Markov链参数的计算中采用了各态历经性假设;在检测阶段,基于状态序列的出现概率对特权程序当前行为的异常程度进行分析,并根据Markov链状态的实际含义和程序行为的特点,提供了两种可选的判决方案.同现有的基于隐Markov模型和基于人工免疫原理的检测方法相比,提出的方法兼顾了计算成本和检测准确度,特别适用于在线检测.该方法已应用于实际入侵检测系统,并表现出良好的检测性能.     

基于吸收Markov链的网络入侵路径分析方法

从攻击者角度对网络进行入侵路径分析对于指导网络安全防御具有重要意义。针对现有的基于吸收Markov链的分析方法中存在的对状态转移情形考虑不全面的问题和状态转移概率计算不合理的问题,提出了一种基于吸收Markov链的入侵路径分析方法。该方法在生成攻击图的基础上,根据攻击图中实现状态转移所利用的漏洞的可利用性得分,充分考虑了非吸收节点状态转移失败的情况,提出了一种新的状态转移概率计算方法,将攻击图映射到吸收Markov链模型;利用吸收Markov链的状态转移概率矩阵的性质,计算入侵路径中节点的威胁度排序和入侵路径长度的期望值。实验结果表明,该方法能够有效计算节点威胁度排序和路径长度期望;通过对比分析,该方法的计算结果相比现有方法更符合网络攻防的实际情况。     

转移概率未知下具有双Markov 链的网络控制系统控制器设计

研究一类基于Markov模型的网络控制系统的稳定性和镇定控制器设计问题.针对网络控制系统中受控对象模型的随机切换和通信过程中的丢包问题,利用具有两个独立Markov链的离散时间Markov跳跃系统进行建模.在该Markov跳跃系统模态转移概率矩阵部分元素未知的情况下,充分考虑转移概率的约束条件,给出系统可镇定的充要条件和状态反馈控制器的设计方法.最后通过仿真示例验证了所提出方法的有效性.     

输入为Markov序列时的多用户检测算法

考虑当用户序列存在时间相关性时的多用户检测，并假设这种相关性可以用Markov链描述，在传统的线性最大似然检测器中嵌入一个隐Markov模型估计过程。因为输入序列是Markov链，检测器的输出可以看成是被噪声污染的Markov序列，Markov模型估计子用于估计用户序列及其转移概率，而估计得到的用户序列用来更新检测器的估计。因此，检测器和用户序列可以通过迭代的方式求解。仿真结果显示本文算法能充分利用信道输入的时间相关性．效果优于传统的最大似然线性检测器。     

基于马尔科夫链的主机异常检测方法研究

提出了基于马尔科夫链模型的主机异常检测方法,首先提取特权进程的行为特征,并在此基础上构造Markov模型。由Markov模型产生的状态序列计算状态概率,根据状态序列概率来评价进程行为的异常情况。利用Markov模型的构造充分提取特权进程的局部行为特征的相互关系。实验表明该模型算法简单、实时性强、检测率高、误报率低、适合用于在线检测。     

不确定图最可靠最大流算法研究

文中首先基于可能世界模型提出了不确定图的最可靠最大流问题和可靠性计算模型,这对于构建可靠性网络、可靠传输路径选择以及系统薄弱环节分析等一系列实际问题具有重要意义;然后基于简单路径组合思想提出了一种求解最可靠最大流的算法SPCA,通过简单路径流量的组合,在无需求得所有最大流分布的情况下获得最可靠最大流,并在组合过程中引入概率剪枝与约束剪枝策略,对无效组合进行过滤,从而显著地提高了算法效率;接着文中针对SPCA算法易受路径数量及瓶颈容量影响的问题,又提出一种基于状态空间划分的最可靠最大流算法SDBA,该算法的主要思想是将不确定图所蕴含的子图空间划分为互不相交且满足最大流值的闭合区间集合,进而寻找所有闭合区间中概率最大的下界状态,经证明这个下界状态对应子图中的最大流分布为最可靠最大流;最后通过实验,比较了两种算法的性能.实验结果表明SDBA算法相对于SPCA算法其空间复杂度有一定的增加,但时间复杂度方面具有较大的优势,能够很好地解决SPCA算法性能受制于容量的问题,具有更好的性能与适用性.     

概率计算树逻辑的限界模型检测

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

Bounded Model Checking for Probabilistic Computation Tree Logic

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

基于软件层次化模型的软件测试数据生成

针对基于Markov链模型的软件测试技术在测试数据生成时不考虑软件的结构信息,生成的测试数据集对代码路径的覆盖能力以及缺陷检测能力都较低的问题,将统计测试与基于Markov链模型的测试相结合,提出了一种新的软件测试模型——软件层次化模型。该模型涵盖了软件与外部环境之间的交互,同时描述了软件内部结构信息。还给出了该模型测试数据集的生成算法：首先生成符合使用情况的测试序列,然后为测试序列生成覆盖软件内部结构的输入数据。通过针对示例软件的实验结果表明,与基于Markov链模型的测试方法对比,基于软件层次化模型的测试在满足软件测试充分性要求的同时,提高了测试数据集的代码路径覆盖能力和缺陷检测能力。     

基于Markov链模型的MANET连通性分析

提出一种基于Markov链模型的移动Ad hoc网络（MANET）连通性分析方法。建立节点可靠性分析的Markov链模型,使之便于计算节点的可靠性概率。基于此,建立网络剩余节点数以及故障节点数状态转移的Markov链模型,并推导出计算节点随机网络连通概率的公式。通过Matlab仿真验证了理论分析的正确性。     

Counterexample Generation in Probabilistic Model Checking

Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.     

p-Automata: New foundations for discrete-time probabilistic verification

We introduce p-Automata, which are automata that accept languages of Markov chains, by adapting notions and techniques from alternating tree automata to the realm of Markov chains. The set of languages of p-automata is closed under Boolean operations, and for every PCTL formula it contains the language of the set of models of the formula. Furthermore, the language of every p-automaton is closed under probabilistic bisimulation. Similar to tree automata, whose acceptance is defined via two-player games, we define acceptance of Markov chains by p-automata through two-player stochastic games. We show that acceptance is solvable in EXPTIME; but for automata that arise from PCTL formulas acceptance matches that of PCTL model checking, namely, linear in the formula and polynomial in the Markov chain. We also derive a notion of simulation between p-automata that approximates language containment in EXPTIME and is complete for Markov chains. These foundations therefore enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics.     

Partial Order Reduction for Probabilistic Branching Time

In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper presents partial order reduction criteria for Markov decision processes and branching time properties, such as formulas of probabilistic computation tree logic. Moreover, we provide a comparison of the results established so far about reduction conditions for Markov decision processes.     

Probabilistic symbolic model checking with PRISM: a hybrid approach

In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed.     

Model checking probabilistic systems against pushdown specifications

Model checking is a fully automatic verification technique traditionally used to verify finite-state systems against regular specifications. Although regular specifications have been proven to be feasible in practice, many desirable specifications are non-regular. For instance, requirements which involve counting cannot be formalized by regular specifications but using pushdown specifications, i.e., context-free properties represented by pushdown automata. Research on model-checking techniques for pushdown specifications is, however, rare and limited to the verification of non-probabilistic systems.In this paper, we address the probabilistic model-checking problem for systems modeled by discrete-time Markov chains and specifications that are provided by deterministic pushdown automata over infinite words. We first consider finite-state Markov chains and show that the quantitative and qualitative model-checking problem is solvable via a product construction and techniques that are known for the verification of probabilistic pushdown automata. Then, we consider recursive systems modeled by probabilistic pushdown automata with an infinite-state Markov chain semantics. We first show that imposing appropriate compatibility (visibility) restrictions on the synchronizations between the pushdown automaton for the system and the specification, decidability of the probabilistic model-checking problem can be established. Finally we prove that slightly departing from this compatibility assumption leads to the undecidability of the probabilistic model-checking problem, even for qualitative properties specified by deterministic context-free specifications.     

使用模型检测解决概率布尔网络优化控制

系统生物学期望对复杂生物系统建立一个真实的、可计算的模型,以便于以系统的角度去理解生物系统的演变过程。在系统生物学中,一个重要的主题是通过外部的干预控制发展关于基因调控网络的控制理论,以作为未来基因治疗技术。目前,布尔网络及其扩展的概率布尔网络已经被广泛用于对基因调控网络进行建模。在控制问题的研究中,概率布尔控制网络的状态迁移本质上构成一条有限状态空间的离散时间马尔科夫决策过程。依据马尔科夫决策过程的理论,通过概率模型检测方法解决网络中有限范围优化控制问题和无限范围优化控制问题。针对带有随机干扰且上下文相关的概率布尔控制网络,使用概率模型检测器PRISM对其进行形式化建模,然后将两类优化控制问题描述为相应的时序逻辑公式,最后通过模型检测寻找出最优解。实验结果表明,提出的方法可以有效地用于生物网络的分析和优化控制。     

Scalable distributed on-the-fly symbolic model checking

This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. The extra memory requirement for counterexample generation is evenly distributed among the processes by a memory balancing procedure. At no point during computation does the memory of a single process contain all the data. This enhances scalability. Collaboration between the parallel processes during counterexample generation reduces memory utilization for the backward step. We implemented our method on a standard, loosely- connected environment of workstations, using a high-performance model checker. Our initial performance evaluation, carried out on several large circuits, shows that our method can check models that are too large to fit in the memory of a single node. Our on-the-fly approach may find counterexamples even when the model is too large to fit in the memory of the parallel system.     

Simulating perfect channels with probabilistic lossy channels

We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicate over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are undecidable for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1. In this paper, we consider a model of probabilistic lossy channel systems, where messages can be lost only during send transitions. In contrast to the model of Baier and Engelen, once a message is successfully sent to channel, it can only be removed through a transition which receives the message. We show that checking whether safety properties hold with probability 1 is undecidable for this model. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.     

Model-checking algorithms for continuous-time Markov chains

Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.     

Model Checking Markov Chains with Actions and State Labels

In the past, logics of several kinds have been proposed for reasoning about discrete-time or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state properties and action sequences. For this purpose, we introduce the logic as CSL which provides a powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic CSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero, we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated with an elaborate model of a scalable cellular communication system, for which several properties are formalized by means of asCSL formulas and checked using the new procedure