非对称χ≠-演算的基同余

该文研究非对称χ^≠-演算的基同余．文中引入一组L-互模拟关系,并确定基互模拟就是由L-互模拟定义导出的12个互异的互模拟关系中的最小关系,给出了某些L-互模拟的开模拟性质,利用开模拟性质引入开基互模拟概念,并证明开基互模拟与基互模拟是一致的,构造了基于基同余的可靠和完备的等式系统,最后给出了基同余的完备性定理．     

扩展的基于角色访问控制模型的设计

协作系统的动态特性要求特定访问主体能够在安全监控下自主地进行访问主体角色关系配置．在研究开发的扩展的基于角色访问控制模型的基础上，应用对象建模方法对模型应用的关键问题提出了解决方案，包括一致性问题、动态监控、约束处理、安全控制等．该研究为扩展的角色的访问控制模型的实际应用提供指导，它可以应用到大型复杂系统，特别适用于动态协作系统，结合认证技术，可以实现大型复杂系统的安全保护．     

一种防火墙系统安全模型的形式描述

文中提出了一种防火墙系统的安全模型，该模型构筑在防火墙系统的安全服务基础之上，将安全模型抽象为若干安全服务的集合并用形式化的方法进行了描述，着重描述了安全服务的动态特性，安全模型的动态特性以及安全模型和防火墙系统之间的相互关系，提出了安全服务的双向性及关键服务集的概念，该模型在已实现的分布式动态防火墙原型系统中得到了验证。     

基于角色的工作流系统访问控制模型

工作流技术在办公自动化、电子商务、电子政务等领域得到广泛关注，工作流系统的安全问题变得日益突出．访问控制是工作流系统安全机制的重要环节．本文在NIST推荐的标准RBAC模型的基础上，结合实际情况，提出一种基于角色的工作流系统访问控制模型WRBAC．该模型描述了用户、角色、许可、活动等要素之间的关系，给出了静态和动态授权约束规则，能有效防止重要信息的泄漏和商业欺诈，满足工作流系统对访问控制的需求．     

基于STP方法的SCADE模型形式化验证框架

高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求。为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSMV模型,并将线性时态逻辑和计算树逻辑引入SCADE模型的需求规范中。分析结果表明,借助NuSMV模型检查器及其验证结果可检验复杂时序相关的安全性质,减少模型设计阶段的错误,提高系统的安全性和可靠性。     

面向服务的角色访问控制技术研究

面向服务的体系结构具有开发效率高、响应快、费用低等优点．但是由于其结构的松散耦合性和计算的动态性,从而造成其安全管理更为复杂．文章首先回顾了访问控制技术的发展,然后提出了一个面向工作流和服务的基于角色访问控制模型．在这个模型中,通过引入服务和授权迁移的概念,加强了对动态服务架构的描述能力．模型对用户角色权限的控制,是通过实际任务和服务状态进行管理的,这样能够有效地加强访问控制的灵活性和系统的安全性．     

计算机安全模型研究

安全模型是安全策略的表达，是建立和评估安全系统的向导．在提出基础模型、经典模型和多策略模型概念的基础上，回顾、分析了一些安全模型，着重对其中的一些模型做了比较，最后在总结了这些模型的基础上，展望了安全模型的可能发展趋势。     

安全协议的扩展Horn逻辑模型及其验证方法

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．     

基于粗糙集理论的安全考试系统*

为了进一步提高结合了传统静态安全技术和动态安全技术的计算机考试系统的安全性,提出了一种基于粗糙集理论的静态安全技术与动态安全技术相结合的高效低负荷的防御方法,用于监控进程的非正常行为。该方法从进程正常运行情况下产生的系统调用序列中提取出一个简单的预测规则模型,能有效地检测出进程的异常运行状态。同原有系统相比,用粗糙集理论建立正常模型要求的训练数据获取简单,而且得到的模型更适用于在线检测。实验结果表明,该系统的安全性优于原考试系统。     

一种多层次特权控制机制的设计与实现

特权控制机制是高安全等级操作系统中一个重要的组成部分，它能够提供系统恰当的安全保证级．给出了在自主开发的、符合GB17859—1999第4级“结构化保护级”的安胜安全操作系统中实现的一种多层次特权机制，它在用户管理层、主体功能层和程序文件3个层次实现特权控制和管理．该机制的实现使系统满足了RBAC的角色职责隔离、DTE域的动态功能隔离和POSIX标准的特权最小化等安全性质，证明以这种受控的方式使用特权可以有效地保证系统的安全性．     

一个通用PDM安全管理模型及实现

首先分析了国内外PDM系统安全管理策略的不足之处,详细介绍了PDM系统的安全策略、聚类静态安全模型、基于Petri网的动态安全模型、层次型分布安全模型和缺省安全模型,并给出相应的算法;最后,结合ZD－PDM系统给出了所述的安全模型的实现技术,并讨论了模型尚需进一步研究的问题。论文所述模型不仅适用于PDM系统,而且对于现有的其它管理信息系统也有重要的意义。     

Emerging security requirements

Interest in the security of information systems has increased partly because of evolving systems maturity, and partly in response to dramatic intrusions into major systems. These have included intrusions by amateur ‘hackers’ which, although embarrassing have caused no substantial damage. Intrusions from employees are far more damaging but have not been widely publicized. The paper describes the US government's security policy and its implications for private organizations. A security policy is basic to the concept of security and defines the manner in which an information system can access and manipulate data. Protection mechanisms which enforce security policies are discussed. Mandatory and discretionary policies which form a particular security policy are outlined. The characteristics of a formal security model are also defined, and the design of a secure operating system is discussed. The present status of information systems security is outlined.     

利用类型推理验证Ad Hoc安全路由协议

提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简Dolev-Yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.     

基于可达关系的安全协议保密性分析

借助形式化的方法或工具分析安全协议是非常必要而且行之有效的.进程演算具有强大的描述能力和严格的语义,能够精确刻画安全协议中各个参与者之间的交互行为.作者以进程演算为基础,嵌入消息推理系统以弥补进程演算固有的缺乏数据结构支持的特点,尝试地提出了一个基于可达关系的安全协议保密性分析模型.基于此模型,形式化地描述了安全协议的保密性,证明了一定限制条件下的可判定性.并且以TMN协议为例,给出了该模型的实例研究.     

A uniform presentation of confidentiality properties

Security (in the sense of confidentiality) properties are properties of shared systems. A suitable model of shared systems, in which one can formally define the term security property and then proceed to catalog several security properties, is presented. The purpose is to present various information-flow properties in a manner that exposes their differences and similarities. Abstraction is the main tool, and everything that is not central to the purpose is discarded. The presentation is generic in the model of computation. The abstraction lays bare a regular structure into which many interesting information-flow properties fall. A shared system is represented by a relation. How this model lets one reason about information flow is discussed and the term information flow property is formally defined. Various information-flow properties are described. Composability and probabilistic security properties are addressed     

A generalized approach to the mean first passage time of a dynamic power system

A stochastic approach to the security evaluation of a dynamic system is presented. The mean first passage time (MFPT) of a multi-dimensional system from its domain of attraction is defined as a security measure, and a closed form expression for the asymptotic estimate of the MFPT is derived. The proposed method encompasses various multi-dimensional dynamic systems, and the analysis of a power system model is used as a case study. The power system is represented by a multi-bus constant voltage, constant impedence model, and the assumption of low damping is waived to widen the application of the results. In this study, small perturbations in dynamic systems have been modelled as weak wideband gaussian coloured noises. Corresponding sensitivity results for a 19-bus power system are presented.     

P2DR模型中策略部署模型的研究与设计

分析动态自适应网络安全模型P2DR的缺陷,提出对P2DR模型的几点改进建议。针对模型中策略相关不足设计了一个策略部署模型,该部署模型实现了策略统一定制、自动分发、自适应管理等功能,同时在部署模型中引入了安全事件关联分析的思想,共享设备间安全信息以实现安全策略的联动操作,达到安全事故及时响应的目标。该部署模型实现了P2DR模型的动态性和自适应以及策略核心作用。     

Uniform stabilization of discrete-time switched and Markovian jump linear systems

The uniform stability of discrete-time switched linear systems, possibly with a strongly connected switching path constraint, and the existence of finite-path-dependent dynamic output feedback controllers uniformly stabilizing such a system are both shown to be characterized by the existence of a finite-dimensional feasible system of linear matrix inequalities. This characterization is based on the observation that a linear time-varying system is uniformly stable only if there exists a finite-path-dependent quadratic Lyapunov function. The synthesis of a uniformly stabilizing controller is done without conservatism by solving any feasible system of linear matrix inequalities among an increasing family of systems of linear matrix inequalities. The result carries over to the almost sure uniform stabilization of Markovian jump linear systems.     

基于马尔可夫模型的云系统安全性与性能建模

针对云环境缺乏安全性评估的问题,提出一种评估系统安全性的建模方法,并建立了云环境下的安全性-性能（S-P）关联模型。首先,针对云系统中最重要的组成部分,即虚拟机,建立了评估其安全性的模型,该模型充分反映了安全机制和恶意攻击两个安全因素对虚拟机的影响;随后基于虚拟机与云系统之间的关系,提出评估云系统安全性的指标;其次,提出一种分层建模方法来建立S-P关联模型。利用队列理论对云计算系统的性能进行建模,然后基于贝叶斯理论和相关分析建立了安全性和性能之间的关联关系,并提出评估复杂S-P相关性的新指标。实验结果验证了理论模型的正确性,并揭示了安全因素引起的性能动态变化规律。