数据库管理系统强制访问控制形式化分析与明证

强制访问控制是保护数据库管理系统安全的有效机制.DMOSMAC是一个依赖于安全操作系统实现强制访问控制机制的数据库管理系统.在分析该系统实现的基础上,对该系统进行了形式化分析.给出了信息流的概念,将信息流集合作为被验证系统状态的一部分.信息流集合始终是一个递增的集合,利用信息集合流可防止删除等操作的证明被绕过的可能,保证验证过程的严密性.在信息流的基础上提出了一种对系统代码进行抽象、抽取的形式化分析方法.即抽象DMOSMAC系统状态,从源代码中提取操作规则,将BLP模型中的状态、访问规则分别与DMOSMAC系统的状态、操作规则建立映射关系,BLP模型中简单安全性和*-特性转换为面向信息流的状态不变式,继承BLP模型的相关安全公理和定理进行分析和证明;最后用定理证明器COQ进行安全性证明的方法.     

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

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

一种基于有限状态机的隐含信息流分析方法

安全系统中的隐含信息流对系统保密特性构成了严重威胁，对安全系统进行相应的信息流分析是发现隐含信息流的最有效方法．以往的信息流分析主要基于事件轨迹模型进行，不易在系统安全实践中得到利用．该文把安全系统及安全策略模型化为有限自动机，通过研究有限自动机的特性来分析安全系统的信息流特性，进而确定出系统中是否存在隐含信息流．自动机模型比轨迹模型更为直观和自然地表述系统安全策略，在实际系统中能更好地得到应用．     

面向智能变电站的信息流可靠性分析模型

智能变电站是智能电网可靠运行的关键环节和重要基础,为避免变电站可靠性的单一定性评估方法给变电站状态监测、检修决策带来的不足,在分析智能变电站及其信息流特征的基础上,从不同角度归纳了智能变电站网络可靠性的评估方法;给出一种基于信息流传输时延、丢包率和各信息流QoS要求的信息流可靠性评估模型,并通过在稳态和极限流量运行方式下对该模型进行了仿真实验,结果表明该方法能在一定程度上定量评估智能变电站信息流的可靠性问题。     

信息流安全特性的语义模型研究

以通信顺序进程为语法基础,结合信息安全模型对安全特性的约束,介绍并分析了几种针对信息流安全特性的语义描述,并提出了信息流安全的单向特性,对其进行了相关安全特性的证明,以期对正确标识合法信息流问题进行探讨,用于正确区分存在的不合法信息流,作为解决隐通道问题的理论依据,从理论分析的角度,尝试解决信息安全的根本性问题.     

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

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

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

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

移动边缘计算中安全信息流建模与分析

在移动边缘计算中,移动终端身份存在复杂性和动态性,对于高安全领域的任务卸载,需要对被卸载的任务进行实时跟踪,及时发现滥用行为才能保证任务卸载的安全性。然而,现有方法多基于信任评估机制选择高信任度节点进行卸载,并没有关注该节点自身发起的内部攻击问题。提出一种支持安全性分析的任务卸载方法。设计包含安全性分析的任务卸载流程,构建面向移动边缘计算的多级安全信息流模型,用于约束服务卸载、数据卸载和服务执行过程。在此基础上,基于偶图对任务卸载过程进行建模,构造标注迁移边的标号变迁系统,并利用模型检测技术验证是否满足相应的安全需求。案例分析和性能评估结果表明,该方法能够在秒级时间内预测任务卸载中的恶意行为,具有较好的可行性和有效性。     

基于间接信息流约束的访问控制模型

为解决跨域跨系统环境下的违规间接信息流问题,提出了一种联合访问控制模型.通过记录系统中的访问行为,构建跨系统的信息流图;在此基础上给出信息流图的安全性定理,定义系统的安全状态;通过制定安全规则,约束跨域跨系统环境中的访问行为.基于安全熵对模型的安全性进行分析和验证,验证结果表明了模型在间接信息流的安全防护能力方面优于传统模型.     

基于安全进程代数的非演绎安全模型的分析与验证

就刻画安全的性质而言,基于非演绎信息流的安全模型较基于访问控制的安全模型更为确切和本质。在基于迹语义对非演绎信息流安全模型进行分析的基础上,基于安全进程代数给出非演绎模型的形式化描述,然后基于系统的安全进程代数表达式给出非演绎模型的验证算法且开发了相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。     

Providing flexible access control to an information flow control model

Protecting privacy within an application is essential. Many information flow control models have been developed for that protection. We developed an information flow control model based on role-based access control (RBAC) for object-oriented systems, which is called OORBAC (object-oriented role-based access control). According to the experiences of using OORBAC, we found that a model allowing every secure information flow and blocking every non-secure flow is too restricted. We propose that the following flexible access control features should be offered: (a) non-secure but harmless information flows should be allowed and (b) secure but harmful information flows should be blocked. According to our survey, no existing model offers the above control. We thus revised OORBAC to offer the control. The revised OORBAC have been implemented and evaluated. This paper presents flexible access control in the revised OORBAC and the evaluation result.     

Instruction-level security typing by abstract interpretation

We present a method based on abstract interpretation to check secure information flow in programs with dynamic structures where input and output channels are associated with security levels. In the concrete operational semantics each value is annotated by a security level dynamically taking into account both the explicit and the implicit information flows. We define a collecting semantics which associates with each program point the set of concrete states of the machine when the point is reached. The abstract domains are obtained from the concrete ones by keeping the security levels and forgetting the actual values. Using this framework, we define an abstract semantics, called instruction-level security typing, that allows us to certify a larger set of programs with respect to the typing approaches to check secure information flow. An efficient implementation is shown, operating a fixpoint iteration similar to that of the Java bytecode verification. This work was partially supported by the Italian COFIN 2004 project “AIDA: Abstract Interpretation Design and Application”.     

Checking secure information flow in Java bytecode by code transformation and standard bytecode verification

A method is presented for checking secure information flow in Java bytecode, assuming a multilevel security policy that assigns security levels to the objects. The method exploits the type‐level abstract interpretation of standard bytecode verification to detect illegal information flows. We define an algorithm transforming the original code into another code in such a way that a typing error detected by the Verifier on the transformed code corresponds to a possible illicit information flow in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright © 2004 John Wiley & Sons, Ltd.     

Secured Information Flow for Asynchronous Sequential Processes

We present in this article a precise security model for data confidentiality in the framework of ASP (Asynchronous Sequential Processes). ASP is based on active objects, asynchronous communications, and data-flow synchronizations. We extend it with security levels attached to activities (active objects) and transmitted data.We design a security model that guarantees data confidentiality within an application; this security model takes advantages of both mandatory and discretionary access models. We extend the semantics of ASP with predicate conditions that provide a formal security framework, dynamically checking for unauthorized information flows. As a final result, all authorized communication paths are secure: no disclosure of information can happen. This theoretically-founded contribution may have a strong impact on distributed object-based applications, that are more and more present and confidentiality-demanding on the Internet, it also arises a new issue in data confidentiality: authorization of secured information flow transiting (by the mean of futures) through an unsecured component.     

RBAC模型的非法信息流控制

由于缺乏信息流控制机制,RBAC模型的授权访问可能导致不安全的信息流.为了保护RBAC模型系统中信息的机密性,定义了RBAC模型的非法信息流概念,给出了非法信息流的检测、更新以及控制算法.将这些算法用于RBAC模型的授权管理可有效防止信息的非授权泄漏,实现安全的访问.     

INFORMATION FLOWS IN HIERARCHICAL SYSTEMS

Relations between information flows and structure are discussed for two major classes of systems which have information-processing functions. It is shown that for both classes hierarchical structure is ideally suited for efficiency in the information processing. A partition law of information flow is developed which shows that the sum of the information flows through atomic components of a deterministic system can be partitioned into flow within the system devoted to system coordination, input flow which affects the output (throughput), and input flow which is blocked by the system.     

分布式系统中有向流的最优调控算法

本文从图论的角度研究了分布式系统中有向流的两个特征，最大流及在给定调节量下的最优控制。获得了明确的结论，并通过相应算法实现求解，本研究对于生产中的物料，电网，电信网信息流控制具有较强的应用价值。     

Information flow control in object-oriented systems

We describe a high assurance discretionary access control model for object oriented systems. The model not only ensures protection against Trojan horses leaking information, but provides the flexibility of discretionary access control at the same time. The basic idea of our approach is to check all information flows among objects in the system in order to block possible illegal flows. An illegal flow arises when information is transmitted from one object to another object in violation of the security policy. The interaction modes among objects are taken into account in determining illegal flows. We consider three different interaction modes that are standard interaction modes found in the open distributed processing models. The paper presents formal definitions and proof of correctness of our flow control algorithm     

基于信息速配的安全标定方法

针对指挥信息系统中系统间信息交换要求,本文提出了一种基于信息速配的安全标定方法,通过对数据在系统间流转的分析,提出一种基于信息特征速配的数据标定方法,并采用非接触式的安全标定与采样方式,实现了对指挥信息系统间传输数据的采样与统计。