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

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

A comparison of semantic models for noninterference

The literature on definitions of security based on causality-like notions such as noninterference has used several distinct semantic models for systems. Early work was based on state machine and trace-set definitions; more recent work has dealt with definitions of security in two distinct process algebraic settings. Comparisons between the definitions has been carried out mainly within semantic frameworks. This paper studies the relationship between semantic frameworks, by defining mappings between a number of semantic models and studying the relationship between notions of noninterference under these mappings.     

基于自动机监控的二维降密策略

降密策略静态实施机制具有限制性过强的缺陷:它将降密策略语义条件判定为安全的程序排斥在外。为了建立更加宽容的实施机制,基于自动机理论,建立了二维降密策略的动态监控机制。程序执行中的命令事件被抽象为自动机的输入,自动机根据这些输入信息跟踪程序执行过程中的信息流,禁止违反降密策略的程序命令的执行。最后,证明了自动机监控机制的可靠性。     

多线程环境中的二维降密策略

降密策略的主要目的在于确保程序中敏感信息的安全释放。目前,降密策略的安全条件和实施机制的研究主要集中在顺序式程序设计语言,它们不能直接移植到多线程并发环境,原因在于攻击者能利用线程调度的某些性质推导出敏感信息。为此,基于多线程程序设计语言模型和线程调度模型,建立了支持多线程并发环境的二维降密策略,有效确保了在合适的程序点降密合适的信息;建立了多线程并发环境下该降密策略的动态监控机制,并证明了该实施机制的可靠性。     

软件系统的可信降密述评

无干扰模型是信息流控制中的基础性安全模型,能确保敏感信息的零泄露,但其安全条件的限制性过强。软件系统由于功能的需要不可避免地需要违反无干扰模型,释放合适的信息。为了防止攻击者利用信息释放的通道获取超额的信息,需要对释放的通道进行控制,建立信息可信降密的策略和实施机制。基于不同维度对现有的降密策略进行归类,大致归并为降密的内容、主体、地点和时间维度;并对现有降密策略的实施机制进行分类,大致可分为静态实施、动态实施和安全多次执行;对这些机制的特点和不足之处进行比较,并探讨了后续研究面临的挑战,展望了未来的研究方向。     

基于JSP的电子公文签名方案设计与实施

由于网络的开放性,文件在网络传输的过程中就会遇到诸如数据的篡改、中断、截取以及身份假冒等安全问题.因此,电子文件传输过程中所涉及的信息安全性问题是一个不可忽略的因素,也是电子文件传输全面推广应用的重要保障.本文首先分析了电子文件传输中存在的安全问题,然后阐述了如何在Java环境中通过应用密码技术提供的数字签名,实现安全的电子文件传输.     

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

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

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

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

基于嵌入式部件的通信加密平台设计

我们在嵌入式部件中通过对称性密钥和公钥密码算法的实现,并以此为基础建立数据加密及安全认证的安全模型。利用密码算法来保障数据的秘密与完整性。通过模型灵活的接口和设计原则,使其成为能够搭载多种媒介和设备的通信加密平台。     

基于信息流的多级安全策略模型研究

内部威胁是企业组织面临的非常严重的安全问题,作为企业最贵重的信息资产——文档,是内部滥用的主要目标。以往的粗粒度安全策略,如最小权限原则、职责分离等,都不足以胜任文档安全化的内部威胁问题。提出了一个崭新的多级安全策略模型,引入了文档信息流和信息流图概念,并提出了相关算法。它能依据系统上下文环境的变化,动态地产生信息流的约束条件,屏蔽可能产生的隐藏信息流通道。     

IP传真技术及其安全性研究

本文介绍了IP传真技术的基本概念和应用特点。在此基础上,详细分析了IP传真技术面临的安全性威胁,并提出了一种安全的解决方案。     

基于信息流的SELinux策略分析模型

针对SELinux安全策略分析和管理上的困难,提出了一种SELinux信息流分析模型SELIF。首先构造有效安全上下文集合和安全上下文的授权关系,然后根据许可权的信息流语义,用标记转换系统表示的安全上下文关系来刻画信息流。SELIF信息流模型可以直观地表达SELinux策略所描述的安全上下文之间的信息流路径,实现对复杂策略的直观分析和管理。     

信息流安全性的隐通道分析与研究

隐通道是信息流安全性研究的关键问题,国内外学者通过分析隐通道对信息安全问题进行了研究。通过分析隐通道产生条件,对两种重要的隐通道的分析方法进行了比较,提出了较为科学的改进思路。     

Specification and static enforcement of scheduler-independent noninterference in a middleweight Java

We introduce a new timing covert channel that arises from the interplay between multithreading and object orientation. This example motivates us to explore the root of the problem and to devise a mechanism for preventing such errors. In doing so, we first add multithreading constructs to Middleweight Java, a subset of the Java programming language with a fairly rich set of features. A noninterference property is then presented which basically demands program executions be equivalent in the view of whom observing final public values in environments using the so-called high-independent schedulers. It is scheduler-independent in the sense that no matter which scheduler is employed, the executions of the program satisfying the property do not lead to illegal information flows in the form of explicit, implicit, or timing channels. We also give a provably sound type-based static mechanism to enforce the proposed property.     

Comments on the ‘m out of n oblivious transfer’

This paper analyses the ‘m out of n oblivious transfer’, presented at the ACISP 2002 Conference. It is shown that the schemes presented in the paper fail to satisfy the requirements of the oblivious transfer.     

二维降密策略的内联引用监控方法

降密策略的静态实施机制存在限制性过强的缺陷,基于虚拟机的动态监控机制不能完全适合Web和即时编译环境。为此,基于内联引用监控方法,实施了基于内容和地点维度的二维降密策略。提出了内联引用监控方法的程序变形规则,并证明了该方法的可靠性;根据该程序变形规则,将源程序进行变形重写,生成一个新的程序,它能脱离外部监控环境,实现自我监控。     

社会信息化环境下的信息安全管理研究

本文对社会信息化环境下信息安全管理工作面临的严峻形势进行了分析,指出了当前信息安全管理存在的不足,在此基础上,就加强我国信息安全管理方面的工作提出了几点建议。     

Preventing Timing Leaks Through Transactional Branching Instructions

Timing channels constitute one form of covert channels through which programs may be leaking information about the confidential data they manipulate. Such timing channels are typically eliminated by design, employing ad-hoc techniques to avoid information leaks through execution time, or by program transformation techniques, that transform programs that satisfy some form of noninterference property into programs that are time-sensitive termination-sensitive non-interfering. However, existing program transformations are thus far confined to simple languages without objects nor exceptions.We introduce a program transformation that uses transaction mechanisms to prevent timing leaks in sequential object-oriented programs. Under some strong but reasonable hypotheses, the transformation preserves the semantics of programs and yields for every termination-sensitive noninterfering program a time-sensitive termination-sensitive non-interfering program.     

信息安全工程理论与实践

简要论述了信息安全工程的基本理论，给出了信息安全工程的流程图，并结合具体实践应用了信息安全工作的基本原理。     

基于硬件的计算机安全策略

计算机的安全问题日益突出,相应地,对计算机安全的研究也越来越受到重视,但目前对计算机安全的研究主要集中在软件方面,为了更有效地提高计算机的安全,对基于硬件的计算机安全进行了研究。应用分类的研究方法,较系统地提出了基于硬件的计算机安全策略,首先从计算机硬件的各个组成部分出发,分析如何提高计算机的安全,然后分析各组成部分如何协调一致。研究结果可以作为计算机安全策略的一部分,用于指导如何提高计算机的安全。