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

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

前向可修正属性算术验证的研究

目前验证前向可修正属性的"展开方法"是不完备的,即当"展开定理"的局部条件不满足时,不能判断出系统不满足前向可修正属性.为此,提出一种基于状态转换系统的前向可修正属性验证方法,该方法将前向可修正属性的验证归约为可达性问题,进而可借助可达性检测技术完成属性的验证.该方法是完备的,且当属性不成立时,可以给出使属性失效的反例...     

一种基于Petri网的隐蔽信息流分析方法

隐蔽信息流分析是开发高等级可信计算机系统必须面对的问题.以Petri网作为开发安全系统的形式化建模工具,给出Petri网中隐蔽信息流存在的判定条件.提出该条件成立的两种网结构,进而可以在语法层次上预先判断隐蔽信息流的存在性,并使由此类结构引起的隐蔽信息流在系统的设计阶段得以避免.开发了一种基于Petri网可达图的隐蔽信息流存在性判定算法,算法遵循无干扰方法的思想,但是避免了无干扰方法中等价状态的区分和展开定理的使用.另外,算法采用深度优先搜索的策略,避免了Petri网全局可达图的构造.对复杂的安全系统,分析了子系统的各种组合运算对隐蔽信息流存在性的影响,降低了大规模系统分析的复杂度.     

多级安全系统中数据聚合的无干扰属性

基于信息流的安全模型较访问控制模型优势在于更本质的描述了什么是安全,自提出信息流的无干扰概念以来信息流模型就成为安全研究的中心之一,并提出了很多种无干扰模型.针对现存几种安全模型存在建模工具与分析工具不一致、不支持多级安全系统等问题.在广义无干扰模型以及聚合属性的基础上提出一种支持多级安全系统、多等级信息流策略状态转换且包含聚合属性的信息流安全模型,并给出了信息流策略的正式语义.     

基于模型检测的信息流策略安全性分析

分布式信息流控制是增强系统安全的一种有效方法,但其灵活性也增加了策略管理和分析的复杂性。策略的安全性分析判定系统的所有可达状态是否都能保持特定的安全属性,可以验证策略是否一致完备的满足安全需求。形式化定义了基于Kripke结构和计算树时序逻辑的信息流策略安全性分析问题,验证信息流允许、禁止和授权管理三类信息流安全目标。提出了分支限界和模型检测两种策略验证算法,实验结果表明,算法可有效验证分布式信息流控制系统是否满足特定安全需求,提高了分布式信息流控制的可用性。     

一个完整的无干扰模型

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

基于知识Petri网和归结规则的推理方法

本文提出了一种基于知识Petri网和归结规则的推理方法.通过知识Petri网描述命题逻辑知识库,将归结规则映射到知识Petri网上,根据库所和变迁的连接关系,定义了知识Petri网中的归结结构.利用归结结构,给出了基于知识Petri网的归结推理算法和扩展知识库的推理算法,并利用Wumpus实例验证了推理算法.该推理方法是可靠且完备的,能够利用知识Petri网的网络结构降低计算复杂性.     

不完备信息系统的属性约简算法

根据不完备信息系统的定义和特点,建立基于集合容差关系的粗糙集模型,构造条件属性的可辨识矩阵,分析决策属性的重要性。阐述并比较3种属性约简方法,对同一个不完备信息表的处理结果表明,3种方法可以得到基本一致的约简结果,验证了其有效性。     

信息流格模型的非法流分析

随着互联网的发展以及网络空间地位的上升,信息的重要性与日俱增。为确保信息安全,对非法信息流的控制显得尤为重要。文中分析了信息流格模型中信息流动的安全性,为更好地对模型内部的信息流进行分类,首先,对信息流格模型进行线性化分析,使得模型被线性化表述,并将其称为线性信息流格模型。接着,引入马尔科夫链,并利用马尔科夫链的常返态属性和瞬时态属性的概率变化,来量化表示模型中主体和客体之间的转换状态,从而检测出模型内部的各个信息流。进一步地,根据模型内部的主体和客体分别对应的常返态与瞬时态的概率对比,分析每个信息流的安全状态,即:当模型检测中同时出现两个常返态时,违反了安全模型,从而导致非法信息流的出现。由于概率变化存在同一性,该方法会产生误差并影响其检测结果。为弥补这一不足,介绍了SPA语言,然后对线性信息流格模型进行了SPA语言的描述,并采用形式化中的无干扰方法对马尔科夫链模型内概率同一性的不足进行补充说明。最后,检测出其中隐藏的非法信息流,判断出含误差下各个信息流的安全状态,并得出结论:符合安全模型但违反安全策略的信息流不满足无干扰属性。这对信息流安全检测软件的设计及硬件应用具有重要意义。     

广义不可推断属性符号化算术验证的研究

多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证方法——"展开方法"——验证的仅仅是属性成立的一个充分非必要条件,因此是不完备的.基于证伪技术提出一种完备的广义不可推断属性验证方法,该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程.为确保搜索过程能正确终止,即方法的完备性,提出状态转换系统的双构造运算,并在此基础上基于图结构理论给出最短反例的上近似计算.进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现了验证过程的符号化计算.最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用.     

联合LDPC码与clipping降OFDM系统峰均比的方法*

针对正交频分复用(OFDM)系统中存在的高峰均比问题,提出了一种简单而有效的降低峰均比(PAPR)的联合方法,即将低密度奇偶校验码（LDPC）与传统的限幅(clipping)技术相结合的方法。该方法通过clipping技术降低OFDM信号的PAPR,同时结合LDPC码改善clipping技术带来的系统误比特率（BER）恶化与频域滤波降低带外功率辐射。MATLAB仿真结果表明,该方案能够简单而有效地降低PAPR并提高系统的BER性能,以及抑制带外功率辐射,证明了该联合方法的有效性。     

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

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

并行程序Petri网模型的结构性质

正确性是并行程序的基础,但是由于它的复杂性,其验证要比串行程序困难得多,因此有必要进行建模并研究其性质.从程序的角度出发,在将基于消息传递的并行程序转换为Petri网模型之后,证明了与并行正确的并行程序对应的Petri网模型应当满足的结构性质,包括强连通性、S-不变量、T-不变量、受控死锁性质以及守恒性,并举例说明了这些性质在并行程序验证中的应用.这些性质可用于并行程序的事前验证,而且避免了使用动态性质进行验证时的状态爆炸问题,从而提高并行程序设计和验证效率.同时这些方法具有良好的可推广性.     

Symbolic algorithmic verification of intransitive generalized noninterference

Generalized noninterference can be used to formulate transitive security policies,but is unsuitable for intransitive security policies.We propose a new information flow security property,which we call intransitive generalized noninterference,that enables intransitive security policies to be specified formally.Next,we propose an algorithmic verification technique to check intransitive generalized noninterference.Our technique is based on the search for counterexamples and on the window induction proof,and can be used to verify generalized noninterference.We further demonstrate that the search of counterexamples and induction proof can be reduced to quantified Boolean satisfiability.This reduction enables us to use efficient quantified Boolean decision procedures to perform the check of intransitive generalized noninterference.It also reduces spatial requirement by representing the space compactly,and improves the efficiency of the verification procedure.     

审计缓冲区的形式化模型及其验证

审计系统作为安全信息系统的一个重要组成部分,对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分,本文利用时序Petri网对审计缓冲区管理的实现方案进行建模,进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了Petri网缺乏描述系统事件之间时序关系的局限性,同时发挥了Petri网对系统并发和物理结构的有效描述及分析的优势,达到了系统验证的目的。     

基于Petri网的密码协议分析

在Federico提出的一种密码协议进程语言的基础上,建立了便于进行密码协议分析的简化Petri网模型,给出了协议满足秘密性的充要条件,并以NS公钥协议为例,用Petri网模型,结合归纳方法和串空间分析方法从密钥、新鲜数和协议主体三个方面的秘密性分析了该协议的秘密性,简化了协议秘密性的分析。     

基于Petri网的SysML活动图的分析与验证

系统建模语言(Systems Modeling Language,SysML)是目前国际上系统工程领域最新的标准建模语言,它包括语义和表示法两部分,缺乏分析和验证的手段。为了弥补这一不足,研究了SysML活动图到Petri网的转换方法,主要定义了将SysML活动图转换为相应Petri网可执行模型的6种转换规则。应用这些规则可以将活动图转换为Petri网模型,进而对其进行化简、分析和验证,同时可检测SysML的行为规范与并发相关的性质,如死锁、有界性等。采用列举法和模拟法验证了所建模型的一致性。证书申请活动图的实例表明,该方法是可行的。     

并发操作系统中基于有色Petri网的死锁检测与避免

1.引言系统的并发性与资源的共享性是并发操作系统的主要特征,其目的是最大限度地提高计算机资源的利用率。死锁是并发操作系统必须解决的一个重要问题。人们试图用不同的方法来解决死锁问题。如Dijkstra提出的有名的死锁避免的“银行家算法”,Coffman等人给出的死锁检测算法。 Petri网模型作为模拟与分析并发、异步、分布式系统的一种有效工具,已被用于解决操作系统中的许多问题。如进程通讯中的生产者/消费者问题、哲学家用餐问题,资源竞     

一种知识库校验工具PKBV的设计与实现

以Petri网建模基于规则的知识库,并据此开发出知识库校验工具PKBV,该工具通过对Petri网可达性及不变量的分析计算,来检查知识库中常见的完整性与一致性错误,针对具有多领域知识库的复杂系统,PKBV具有抽取多领域知识库之间的关联规则并进行校验的功能,满足了复杂知识系统的校验需求。     

基于Petri网的地铁车辆远程故障诊断

针对当前地铁车辆故障,特别是电气故障判断的自动化需求,结合Petri网故障树判断方法,对某型号的地铁车辆故障进行判断。先对Petri网进行简单的概述,然后构建电气系统的Petri网模型,并定义相关的规则,最后搭建Petri网模型验证平台,对上述的地铁车辆传动系统故障进行判断,结果通过地面服务器展示出来。