加权迁移系统线性时间属性及其安全性检测

针对加权迁移系统,提出了线性时间属性及其安全性检测。首先定义了半环K上的加权迁移系统,提出了加权线性时间属性概念,并根据权重函数确定加权线性时间属性的上确界、下确界和闭包; 接着给出了几种常见的加权线性时间属性并且讨论了它们的关系; 然后重点研究了加权安全性,通过加权自动机和闭包给出了加权正则安全性; 最后基于加权有穷自动机,建立了加权正则安全性的检测方法。检测过程结合半环和形式幂级数,构造了加权迁移系统和加权有穷自动机的乘积系统,将加权安全性检测问题转化为验证乘积系统的不变性,给出了加权正则安全性检测的算法和复杂度。实例结果表明,所提的方法能够对加权迁移系统的安全性进行检测。     

基于软件行为指纹的自检测防窜改技术研究*

对软件的行为进行抽象建模,通过安全hash函数计算软件的行为指纹,并通过自检测防窜改技术检测软件行为指纹,保护客户端软件的完整性和安全性。给出了软件的行为建模和检测,以及自检测防窜改系统,并作了系统安全性分析。     

基于软件行为指纹的自检测防窜改技术研究*

对软件的行为进行抽象建模,通过安全hash函数计算软件的行为指纹,并通过自检测防窜改技术检测软件行为指纹,保护客户端软件的完整性和安全性。给出了软件的行为建模和检测,以及自检测防窜改系统,并作了系统安全性分析。     

基于WLAN的入侵检测系统研究与设计

WLAN入侵检测技术作为一项安全技术,在保证WLAN的网络和系统安全性上起着非常重要的作用。针对WLAN的安全性问题,分析WLAN面临的一些主要攻击手段,对WLAN中的入侵检测典型技术进行探讨;设计一个WLAN入侵检测系统模型,并给出该系统模型的逻辑构成,对构成该系统模型的各个模块的功能及其实现技术进行详细阐述;对WLAN入侵检测系统的实现做了必要的研究与探讨。     

WLAN安全检测与评估系统的设计与实现

针对无线局域网存在的安全问题，设计并实现了无线局域网安全检测与评估系统。系统能够对基于802．11b的网络进行安全检测，结合漏洞扫描对网络安全性进行评估，给出评估报告及安全建议。     

一种基于移动代理的DIDS模型研究

对传统的分布式入侵检测系统（DIDS）的局限性进行了详细分析,并提出了一种基于移动代理的DIDS模型,给出了设计思想、系统结构和检测原理。该模型可有效的提高分布式入侵检测系统的安全性和适应性。     

基于移动代理技术的入侵检测系统模型

为提高入侵检测系统的效率和灵活性,提出一种基于移动代理的入侵检测系统结构模型.给出系统结构模型各功能模块的实现,并提出算法来保证移动代理的安全性.该结构模型对开发新型的入侵检测系统有一定的指导意义.     

基于Agent的分布式入侵检测系统

针对现有入侵检测系统存在的问题,论文提出了一个基于Agent的分布式入侵检测系统模型,该系统模型结合目前几种主要的入侵检测技术和数据挖掘技术,实现了入侵检测和实时响应的分布化,同时增强了入侵检测系统的灵活性、可伸缩性、鲁棒性、安全性以及入侵检测的全面性。文末给出了根据该系统模型实现的入侵检测系统的实验测试结果,证明了该系统对入侵检测的有效性和合理性。     

分布式入侵检测系统中自保护代理的系统设计

采用分布式结构的基于网络的入侵检测系统(NIDS)自身的安全性已经成为一个重要问题。在分析了已有NIDS的技术特点的基础上，根据其特性引入了报文过滤、进程控制、报文确认和安全通信的思想，提出了面向NIDS的向保护代理(Sclf-protcction Agent)的模型，并给出了SPA的体系结构与详细设计。在与已有的基于代理的入侵检测系统结合后，SPA可以提高NIDS的安全性。     

冷气机组的多参数测量系统与性能分析

本文阐述了用８０９８单片机来控制测量四台冷气机组的冷水温度、系统的压力和检测温度。文章给出了系统的硬件结构框图，介绍各部分电路的工作原理。文章又论述了系统的软件功能和软件的主要模块流程。本文还讨论了系统的可靠性与安全性，因而有一定的实用价值。     

模糊安全性和活性

形式规约使用形式语言构建所开发的软硬件系统的规约,刻画系统的模型和性质。其中,性质规约中的分支时间规约对于系统验证有着非常重要的作用。在经典情形下,系统性质规约是基于二值逻辑的,不能描述不一致或不确定的信息。因此,将其推广到模糊逻辑背景下,有助于对模糊系统进行形式验证。文中首先给出了性质规约中分支时间属性在模糊背景下的形式化定义,重点研究了其中的安全性和活性;然后,定义了两种闭包操作,从而产生了4种类型的属性,即泛安全性、泛活性、存在安全性和存在活性;最后,证明了每个分支时间属性,或是存在安全性和存在活性的交,或是泛安全性和泛活性的交,或是存在安全性和泛活性的交。     

The Unit-B method: refinement guided by progress concerns

We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems, satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events’ scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our approach by an example to show that systems development can be driven by not only safety but also liveness requirements.     

Liveness Checking as Safety Checking

Temporal logic is widely used for specifying hardware and software systems. Typically two types of properties are distinguished, safety and liveness properties. While safety can easily be checked by reachability analysis, and many efficient checkers for safety properties exist, more sophisticated algorithms have always been considered to be necessary for checking liveness. In this paper we describe an efficient translation of liveness checking problems into safety checking problems. A counter example is detected by saving a previously visited state in an additional state recording component and checking a loop closing condition. The approach handles fairness and thus extends to full LTL.     

Reasoning About Probabilistic Behavior in Concurrent Systems

Certain aspects of the behavior of concurrent systems are intrinsically probabilistic in nature, e.g., the behavior of imperfect communication media used in network protocols. We address the problem of expressing such behavior in an algebraic calculus for communicating systems. The introduction of probabilistic information in the calculus alleviates the problem of proving liveness, as proving liveness now amounts to proving that its probability is 1. A methodology for proving both safety and liveness is developed and used in proving the correctness of the Alternating Bit Protocol.     

Efficient reduction of finite state model checking to reachability analysis

Two types of temporal properties are usually distinguished: safety and liveness. Recently we have shown how to verify liveness properties of finite state systems using safety checking. In this article we extend the translation scheme to typical combinations of temporal operators. We discuss optimizations that limit the overhead of our translation. Using the notions of predicated diameter and radius we obtain revised bounds for our translation scheme. These notions also give a tight bound on the minimal completeness bound for simple liveness properties. Experimental results show the feasibility of the approach for complex examples. For one example, even an exponential speedup can be observed.     

Defining liveness

A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that ‘something good’ eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property.     

并发系统的安全性与活性的验证方法

网络环境下的分布式系统是典型的并发系统。安全性和活性是并发系统最为关注和需要保证的两个主要性质。然而在并发系统建模和形式化验证时,面临着描述繁琐、复杂和难以理解的问题,特别是当并发系统的规模（并发进程数目）较大时其性质验证时的效率问题更是严重阻碍了并发系统模型检测与验证技术的应用。将组合可达性分析和标号迁移系统的模块化思想与模型验证技术相结合,提出了一套有效的性质验证方法。论证、分析了三个并发系统安全性和活性验证定理,据此导出了并发系统的安全性与活性验证的有效算法。并通过一个简单实例,对算法有效性进行了初步验证。     

时间自动机可达性分析算法的改进

模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。     

基于行为时序逻辑系统性质研究

文章研究行为时序逻辑(TLA)中行为(Action)的性质及行为之间的关系,提出"行为活性"和"行为安全性"概念,从行为的视角重新给出系统活性和安全性的定义,使得安全性和活性定义更加直观和容易理解,并证明了新老定义的等价性。