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

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

非传递广义无干扰属性符号化算术验证方法

广义无干扰属性规约了多级安全系统中具有传递性质的安全策略,而对于不满足传递性的策略则无法刻画.文中首先对广义无干扰属性进行扩展,提出了非传递广义无干扰属性的概念,进而可以规约无传递性的安全策略.文中提出了一种可符号化实现的非传递广义无干扰属性验证方法.该方法主要基于证伪和证真的基本验证策略,通过集成反例搜索和归纳证明完...     

基于接口精化的广义无干扰性研究

在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题。针对当前构件化软件设计过程中,信息流安全属性仅局限于二元安全级格模型的问题,在现有安全接口结构基础上提出广义安全接口结构,在广义安全接口结构上定义精化关系,并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性,首次将安全多执行的思想应用于构件化系统的信息流安全属性验证。使用 Coq 定理证明工具实现了接口自动机程序库以及对精化关系的判定过程,并用实例验证说明了无干扰属性定义的特点及判定方法的有效性。     

基于行为的结构化文档多级访问控制

针对当前云计算环境中因缺乏多级安全机制而使结构化文档容易产生信息泄露和非授权访问等问题,提出基于行为的多级访问控制(action-based multilevel access control model,AMAC)模型并给出策略的形式化描述.利用信息流中的不干扰理论建立AMAC不干扰模型,并证明AMAC模型中多级访问控制策略的安全性.与已有访问控制模型的比较与分析表明,AMAC模型既可以利用角色、上下文和用户访问行为以提高访问控制策略的灵活性,还可以依据用户,用户访问行为和结构化文档的安全等级实现多级安全机制.     

基于可信级别的多级安全策略及其状态机模型

虽然MLS(multilevel security)被广泛应用于各种安全系统,但是它不能实现信道控制等重要的安全策略.将可信级别的概念引入到MLS中,使其可以方便地实现各种信道控制策略.建立了一个实现这种基于可信级别的多级安全策略的访问控制状态机模型,并证明其对定义的策略是安全的,而且可以实现所有静态信息流策略.另外,还扩展了该模型,使其可以支持存储对象安全属性的动态改变.该模型克服了MLS不能解决安全降级问题以及不考虑完整性的缺点,同时又保留了传统分级策略模型易理解、易使用的优点.     

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

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

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

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

一个完整的无干扰模型

本文提出了基于主体行为的视图的新无干扰概念，描述了一个完整的、基于新概念的信息流安全模型。在模型中把计算机系统中的操作抽象为读和写两种访问模式并定义了相应的转换规则。该模型主要特点有：用于分析系统的安全性；支持多安全策略。     

基于Seal演算的分布式系统安全模型

针对目前分布式计算安全模型存在的不足,以能有效描述位置和移动性的形式化模型Seal演算为工具,将系统安全属性的刻画归结为系统进程在给定计算环境下的位置互模拟等价,提出一种无干扰安全模型,其可以方便地刻画不同的安全性质。为满足实际安全需求,提出了一种可复合的安全属性,并给出了相应的证明。最后,通过实例分析表明了模型的有效性。     

多级安全OS与DBMS模型的信息流及其一致性分析

数据库安全与操作系统安全密不可分,如果多级安全DBMS的安全策略不违反OS的安全策略,那么可以使用多级安全OS的安全机制来实现DBMS的部分安全功能,如强制访问控制．信息流分析使我们能更好地理解安全策略的意义和内容．该文给出了多级安全OS模型和以该模型为基础的多级安全DBMS模型,首次详细分析了它们在强制访问控制策略下的信息流集合．经过主客体的映射后,证明了数据库与操作系统的信息流集合是一致的,这个结论保证了利用OS的机制来实现DBMS的强制访问控制的合理性．     

计算机安全中的无干扰模型

与基于访问控制的形式安全模型相比,基于信息流的安全模型对于定义什么是安全来说更为本质,自提出信息流的无干扰概念以来,信息流模型成为安全研完的中心之一,并提出了多种无干扰信息流模型。本文基于进程代数框架研完这些模型,并给出了一些新的结果和证明。     

信息安全模型研究

首先介绍了安全系统的形式化开发方法，分析和比较了各种安全模型的安全特征。并针对分布式环境对安全模型的通用性和可结合性的要求，着重分析了无干扰模型和非推理模型。并以此为基础提出了改进的无干扰模型和非推理模型。     

内网安全监管审计系统的架构设计

为了规范企业内网用户的操作行为,防止内部敏感信息泄露,适应企业内网大规模多级化的特点,提出了内网安全监管审计系统,对系统的总体架构设计进行了阐述.介绍了基于P2DR模型的系统安全模型;基于"服务器-控制台-受控代理"的系统物理结构;基于角色访问控制机制的分布式授权管理模型;基于TCP/lP协议的跨越因特网的不同局域网之间的系统通信机制.     

基于扩充敏感标记的格理论模型研究

为在实现多级安全系统过程中有效兼顾BLP模型与Biba模型,分析安全模型敏感标记集合在数学上形成的格理论,提出一种能够有效融合这些模型的敏感标记格安全理论模型,以同时标识信息机密性与完整性,通过构建新的敏感标记格理论模型,为信息安全模型研究提供一定的理论依据。     

公安网络系统中基于对抗的攻防安全研究

公安系统网络层次多,覆盖面广,网络问题遭遇不法分子利用,将会带来难以估计的后果,甚至会影响到国家安全。本文针对公安系统网络,分析了公安系统网络安全风险与存在的问题,在信息对抗理论与技术的大发展基础上,对基于对抗的网络攻防理论和手段进行研究。此研究帮助抵御公安网络风险,为公安网络安全提供理论支撑。     

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

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

动态系统的一致同余安全

研究动态系统的安全问题．针对动态系统运行时间配置的可变特性，引入了动态系统的进程代数模型和复杂动态系统概念，定义了动态系统的一致安全性质和一致同余安全性质．基于观察同余等价，构造了一类一致同余安全模型．本文证明，动态系统的安全性质是一致安全性质，而对于复杂动态系统，其安全性质是一致同余安全性质．     

Information leak detection in business process models: Theory,application, and tool support

Despite the correct deployment of access control mechanisms, information leaks can persist and threaten the reliability of business process execution. This paper presents an automated and effective approach for the verification of information flow control for business process models. Building on the concept of place-based non-interference and declassification, the core contribution of this paper is the application of Petri net reachability to detect places in which information leaks occur. Such a feature allows for the use of state-of-the-art tool support to model-check business process models and detect leaks. We show that the approach is sound and complete, and present the Anica tool to identify leaks. An extensive evaluation comprising over 550 industrial process models is carried out and shows that information flow analysis of process models can be done in milliseconds. This motivates a tight integration of business process modeling and non-interference checking.     

基于安全标签的访问控制研究与设计

为了保障信息的安全性和保密性,对信息的访问和操作需要遵循一定的安全策略.安全标签是实现多级安全系统的基础,是实施强制访问控制安全策略的前提.对基于安全标签的强制访问控制模型的实现方案和技术进行了较为详细地分析,主要从安全标签的定义、组成、存储、比较算法和实现等几个方面进行了讨论.鉴于安全标签在高安全等级数据库系统中的重要作用,并在自行开发的具有自主版权的数据库管理系统LogicSQL上实施了该方案,使其至少达到B1级别安全.     

涉密环境桌面虚拟化多级安全系统设计与实现

为解决涉密环境对于桌面虚拟化的多级安全防护需求,文章提出了一种面向涉密环境的桌面虚拟化多级安全模型--vDesktop-BLP模型。该模型结合桌面虚拟化应用场景,对经典BLP多级安全模型进行了改进,实现了对涉密环境桌面虚拟化系统中信息流流向的多级安全控制。文章还对模型进行了系统实现,对其中的安全机制进行了详细设计,最终保证虚拟桌面间最主要的两类信息交互行为（网络通信行为和存储设备读写行为）能够符合涉密信息系统多级安全的要求。