高安全级信息系统中的特权控制机制及其模型研究

为满足高安全级信息系统最小特权需求,提出一种强制访问控制模型EPMM。该模型采用三权分立机制对系统中的特权管理进行改进,将原有的超级用户划分为系统管理员、安全管理员和审计管理员,将其中任一个管理员的权限控制在其职责范围内。建立了模型公理系统并对主要定理进行了证明,使非法用户或异常操作对系统所造成的损失降为最小。     

基于ECⅡ代数的概念格属性约简

概念格是数据分析与知识发现的重要理论.知识发现的一个重要方面是知识约简,因而找到简单有效的约简方法是非常必要的.本文从形式背景上ECⅡ代数结构的角度出发,研究了概念格的属性约简定理,约简方法及属性特征.     

Aziz-Diffie协议的形式化分析及其改进

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议安全性的一条可靠而准确的途径。作为形式化分析方法的典型代表BAN逻辑由于其直观、易用等优点得到广泛的应用。概述了BAN逻辑,并基于BAN逻辑对Aziz-Diffie无线网络密钥协议进行了形式化描述和分析,验证了协议存在的漏洞,同时提出了该协议的改进方案。     

云计算研究综述

介绍了云计算产生的背景和云计算的定义,辨析了云计算与其他计算形式的区别,阐述了云计算的特点及其体系结构,展望了云计算的发展前景。     

CTCS-3级列控系统车地交互流程形式化建模与验证

正在建设的时速300 km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程:任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心(RBC)、车载设备(ATP)和铁路专用移动通信网(GSM-R)的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性.     

GMA架构下监控信息工作流模型探讨

分析了GMA架构的核心流程,基于活动网络图提出了一种监控信息工作流模型的定义,设计了基于GMA的工作流模型.在引入XYZ/E线性时序逻辑语言中的时序算子的基础上,给出了GMA体系架构的生产者与消费者之间主要信息交互活动工作流模型的形式化语义.     

基于超图文法的软件体系结构动态演化

提出用带约束的超图表示软件体系结构,给出基于超图态射的软件体系结构动态演化通用产生式规则的形式化语义和操作,定义类型超图作为体系结构风格,运用超图文法和体系结构风格建模软件体系结构动态演化.为了验证软件体系结构动态演化的正确性,采用模型检测技术,设计算法对软件体系结构动态演化性质进行形式化验证,并应用模型检测工具进行实验分析.该方法既提供了图形化的直观表示,又展示了基于文法的形式化理论框架.     

形式复环上的规范内积模

考察内积模的内积象性质。抽象出形式复环与Ｇ·Ｓ同构概念，并给出形式复环一些判定。     

Evaluation Model of System Survivability

This paper puts forward a survivability evaluation model, SQEM （Survivability Quantitative Evaluation Model）, based on lucubrating the main method existed. Then it defines the measurement factors and parses the survivability mathematically, introduces state change probability and the idea of setting the weights of survivability factors dynamically into the evaluating process of SQEM, which improved the accuracy of evaluation. An example is presented to illustrate the way SQEM works, which demonstrated the validity and feasibility of the method.     

Hurwitz同余定理

建立了简明的Hurwitz定理,并考虑了它在简化已有结论的证明和创立大量同余式方面的应用.它例示着数学研究的模式性.