一种对多级安全模型安全性的分析方法

由于BLP模型的基本安全公理不能完全证明模型的安全性,因此,在分析BLP改进模型的安全性时,如果模型的安全策略十分复杂而不能直接判断其安全性,或者模型由于改变了安全属性定义等而动摇了基本安全公理的推理基础时,应从其他角度证明改进模型的安全性.利用基于系统动作的不干扰模型,从信息流的角度给出一种对多级安全模型的形式化分析方法,为多级安全模型的安全性验证提供了一种新的途径.该不干扰模型把不干扰关系扩展到系统动作之间,提出了新的单步展开定理,可描述多级安全模型中的动态策略.通过以ABLP与DBLP模型为实例进行分析,说明了该分析方法的实用性.     

基于无干扰理论的完整性度量模型

针对现有可信计算完整性度量方案不能反映程序执行时动态特征的问题,提出一种基于系统操作无干扰的完整性度量模型,该模型借鉴信息流的无干扰理论,通过分析进程操作的完整性及进程间完整性的传递,从动态的角度对系统的运行完整性进行度量.对该模型进行形式化的描述和分析表明,该模型直观、易懂,且不局限于某种特定的实现方式.     

基于信息熵的隐通道能力分析*

给出了一种基于信息熵的隐通道能力分析方法。该方法首先利用无干扰分析法分析隐通道,得到系统状态转换分布特性,然后引入信息熵,进而推导出隐通道能力表达公式。该方法能较好地对隐通道能力进行定量分析,不仅可以对隐通道能力的大小进行计算,还可以分析隐通道能力的影响因素。最后,给出了存在于多级安全数据库中的一种隐通道,并用该方法分析计算了该隐通道的能力。     

Automated enforcement for relaxed information release with reference points

Language-based information ftow security is a promising approach for enforcement of strong security and protection of the data confidentiality for the end-to-end communications. Here, noninterference is the standard and most restricted security property that completely forbids confidential data from being released to public context. Although this baseline property has been extensively enforced in various cases, there are still many programs, which are considered secure enough, violating this property in some way. In order to control the information release in these programs, the predetermined ways should be specified by means of which confidential data can be released. These intentional releases, also called declassifications, are regulated by several more relaxed security properties than noninterference. The security properties for controlled declassification have been developed on different dimensions with declassification goals. However, the mechanisms used to enforce these properties are still unaccommodating, unspecific, and insufficiently studied. In this work, a new security property, the Relaxed Release with Reference Points （R3P）, is presented to limit the information that can be declassified in a program. Moreover, a new mechanism using reachability analysis has been proposed for the pushdown system to enforce R3P on programs. In order to show R3P is competent for use, it has been proved that it complies with the well-known prudent principles of declassification, and in addition finds some restrictions on our security policy. The widespread usage, precision, efficiency, and the influencing factors of our enforcement have been evaluated.     

基于托架动不干涉条件的停车设备链传动系统的设计

建立了垂直循环式停车设备托架运动不干涉条件，提出了根据托架运动不干涉条件设计停车设备链传动系统的方法。模型试验表明，所给出的托架运动不干涉条件和链传动系统设计方法合理可行，可用于实际停车设备链传动系统设计。     

基于虚拟化技术的信息流控制方法

随着信息技术的发展,越来越多的企业利用资源的共享、信息的交换以及交互操作等方式开展工作。信息的安全问题越来越引起人们的关注,尤其是涉密信息的安全。因此必须对不同安全密级信息的流动进行严格控制。本文分析了现有的采用分区机制的可信系统的信息流控制方法的不足,并对传统的多级安全操作系统中信息流的安全性进行探讨,利用现在流行的虚拟化技术,采用显示安全标记和隐式安全标记相结合的方法提出了一种基于虚拟机的信息流安全控制方法,并通过无干扰理论进一步验证了该信息流控制方法的安全性和有效性。     

基于加权下推系统优化可达性分析的Java安全信息流研究

信息流安全的形式化以无干扰性为标准属性.针对目前字节码级的信息流安全分析均未基于对程序无干扰性的语义表示,提出了一种基于语义的无干扰性自动验证方法.为适应语言特性和应用环境的限制,将基本自合成扩展为低安全级记录自合成,以支持对标错状态的可达性分析,保证标错状态不可达时对应字节码程序满足无干扰性.在此基础上为提高实际验证效率提出了3种模型优化方法.实验说明方法的可用性、效率、可扩展性及模型优化的实际效果.     

一个非确定系统的不干扰模型

提出系统动作对信息域的不干扰概念,并在此基础上将不干扰模型推广到非确定系统.由于基于系统动作的不干扰概念简化了系统动作序列的提取操作,该模型的单步展开条件具有简洁的形式并易于理解和使用.推广后的不干扰模型不仅能够验证静态信息流策略,还可以验证各种动态信息流策略.最后设计了一个基于动态标记的访问控制模型,并在该模型中定义了读、写、执行等操作的具体语义,然后利用不干扰模型对其安全性进行了形式化验证.     

基于无干扰理论的交换行为可信性分析方法

针对目前数据安全交换中缺乏对交换行为的动态监管,无法保障数据交换的安全实施问题,提出一种基于无干扰理论的交换行为可信性分析方法。该方法首先从交换进程的角度对交换行为进行形式化建模,然后将无干扰理论与可信计算的思想相结合,提出不同阶段、不同模式下交换行为可信的约束规则,交换行为可信性判定定理及安全证明,最后结合一个具体的应用示例说明该方法的可用性。     

一种基于系统动作的非确定不干扰模型

 本文提出一种基于系统动作的非确定不干扰模型,把不干扰关系拓展到系统动作之间,并表明信息流的产生同时依赖于发起者和观察者的动作,可通过允许发起者动作而阻止观察者动作的方法避免信息流动.最后设计了一个多级安全系统,并为排除隐蔽信道提供了一种新的方法.