基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究

隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.     

扩展不干扰模型(ENISM)及基于CSP的描述和验证方法

在不干扰理论的基础上,提出扩展不干扰模型ENISM及其验证方法,用以描述和分析操作系统中的信息流策略.工作包括:(1)依据系统功能模块定义多个执行域,以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础;(2)给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC;(3)基于通信顺序进程给出ENISM-CC的语义及操作系统模块设计的形式化描述和验证方法.     

面向服务访问控制策略精化描述

策略精化是解决分布式应用访问控制策略配置复杂性的重要方法.现有的策略精化技术给出了分层策略描述和逐层精化的方法,但是描述和处理策略之间关联问题能力不足,影响策略精化应用.为此给出了策略和包括组合、互斥、精化、访问路径协同等策略之间关系的形式描述方法,提出了能够描述策略之间关联属性的精化算法和记录策略和策略之间这些关联属性的策略精化树构建方法,为策略精化中的策略关联问题处理提供基础.策略精化树还能直观呈现访问控制的服务品质协议(service-level agreement,SLA).     

数独问题的一种简单解法

在计算机解决数独问题的算法中,回溯法是非常有效的。这是一种数据结构简单、算法逻辑清晰、程序简洁明了、运行高速有效的解题方法,并结合源程序与实例进行说明和论述。     

汇编级顺序语句块的自动形式化规约及其验证

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。     

HybridHP:一种轻型的内核完整性监控方案及其形式化验证

虽然传统的虚拟化监控方法可以在一定程度上保障操作系统安全.然而,虚拟监控器VMM中管理域Domain0的存在以及操作系统级的切换所带来的性能损失是很多具有大型应用的操作系统所不能接受的.注重硬件虚拟化技术的监控能力而摒弃其不必要的虚拟化能力,提出了一个新型的通用的虚拟化监控框架HybridHP,并实现其原型.HybridHP将管理域和虚拟机监控机制两者整合到被监控操作系统的地址空间,具有很好的获取被监控系统操作语义的能力.利用Isabelle/HOL形式化辅助证明工具验证HybridHP的隔离性、安全性和监控能力.最后对HybridHP进行了攻击实验和性能评估,结果显示HybridHP提供了和传统的虚拟化监控方案相同的安全保障,并具有很好的系统性能.     

凸复合函数极小化的二阶条件

在不可微最优化问题中,凸复合函数F=h○f(其中h:R~m→R是有限值凸函数,f:R~n→R~m是连续可微函数)的极小化问题有着重要意义。J.V.Burke给出了函数f是二阶连续可微情况下的凸复合函数F极小化的二阶充分必要条件。本文扩展了Burke的工作,给出了f是C~(1,1)类函数情况下的二阶充分和必要条件。     

分布式应用访问控制策略精化冲突分析

随着云技术的发展,分布式应用平台朝着弹性资源和环境动态变迁的方向发展。分布式应用访问控制策略精化计算与资源和环境相关,也需要较强的性能与这种动态性相适应。现有的访问控制策略空间冲突分析方法虽然可以用于分布式访问控制策略精化中的策略冲突分析,但是该类算法以权限赋值单元为单位计算,计算粒度过细导致性能较低。提出了基于集合求交递推算法,以权限赋值单元集合为单位计算策略冲突来提高计算粒度。理论分析与实验结果表明该算法具有较高性能, 适用于云平台策略精化计算的高性能的需求。     

一种优化入侵检测系统的方案

基于特征的入侵检测系统是目前的入侵检测技术的主流。文中提出了一种针对每一个网络报文,即时的创建一个单一的特征集合来进行匹配的方案,从而减少了匹配的工作量,提高了系统的效率。     

利用对称多处理器提高NIDS的性能

网络入侵检测系统(NIDS)通过捕获和分析网络数据包判断是否存在攻击行为。由于网络带宽越来越高,NIDS的处理能力越来越难以跟上网络的速度。该文提出了一种利用对称多处理器(SMP)提高NIDS处理能力的方法,通过多个CPU并行的处理网络数据包改善系统的性能。经过对NIDS处理过程的分析,设计了一种有效的并行处理结构,保证在不同CPU上运行的线程能够高度并行的执行。此外,该文提出的线程同步方式既保证了程序功能的正确,又避免了对共享资源的互斥访问,进一步提高了线程的并行度。实验证明,在具有双CPU的SMP结构上实现的NIDS的性能比单CPU系统提高了80%。