一种基于无干扰模型的信任链传递分析方法

基于可信计算组织(TCG)的完整性度量只能保证组件没有被篡改,但不一定能保证系统运行可信性.其问题在于,当组件运行时,受其它组件的干扰,出现非预期的信息流,破坏了信任链传递的有效性.文章在分析可信计算平台的信任模型基础上,基于无干扰理论模型,提出了一种分析和判定可信计算平台信任链传递的方法,用形式化的方法证明了当符合非传递无干扰安全策略时,组件之间的信息流受到安全策略的限制,隔离了组件之间的干扰,这样用完整性度量方法所建立的信任链才是有效的.     

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

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

面向无传递性安全策略的语法信息流分析方法

传统的语法信息流分析方法均基于实施机密性安全策略的信息流格模型,而格关系的传递特性使得该方法不能用来分析实施无传递性安全策略的系统的安全性。提出一种新的标识隐蔽信息流的语法信息流分析方法,该方法对实施具有传递性和无传递性安全策略的系统均适用。将信息流语义附加在每条语句之后,定义一种称为信息流时序图的图结构来刻画信息流发生的时序关系,给出了基于源程序的信息流时序图的构造方法,提出了一种基于时序图的隐蔽信息流的标识算法。另外,针对并发程序的并发特性,提出了一种简化信息流时序图的方法,在该方法下只要考虑并发进程之间特定的交互次序即可,而不需要考虑所有可能的交互方式。     

基于特征的网络安全策略验证

安全策略的完整性、正确性和一致性对网络信息系统的安全性能具有重要的影响.针对其验证问题,提出了基于特征的网络安全策略动态验证模型和算法.首先给出了安全策略完整性构造方法;并在此基础上,引入保护因子、敏感因子和安全因子等要素,建立了安全策略的正确性评估模型;最后,引入关联标识集,利用策略各属性特征间的作用关系,提出了安全策略的一致性检测算法.实验结果表明,该评估模型能有效地反映安全策略的安全性能,检测算法具有较高的处理效率,为网络安全策略的验证提供了一种新的解决途径.     

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

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

新型属性图文法反应式规约验证方法

属性图文法广泛应用在软件设计阶段建模和分析阶段。命题式时序逻辑（propositional temporal logic）无法直接表达建模实体包含随时间演化的关联属性反应式规约,提出一种可支持通用图文法转换系统中相应规约的验证方法,通过引入标记节点及属性,将包含相应关联属性的规约公式等价转换为命题式时序逻辑,从而可以间接支持该类型规约的验证。以流行的对象式属性图文法模型检测工具GROOVE为平台,结合启发案例,验证了所提出方法的有效性。     

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

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

支持起源回溯的最小化标识属性传播

数据起源主要描述数据的来源及随时间演化的过程。最小化查询数据表的标识属性传播是一个亟待解决的问题。通过构建等值传播链表EPL描述查询中的等值连接及其传递性,并基于EPL给出朴素标识属性传播方法实现高效溯源信息传播。然而标识属性通过等值连接可以识别非标识属性数值,简单地传播数据表的标识属性数值导致起源数据冗余传播。为避免溯源信息冗余,提出完全标识属性传播格及其剪枝策略,给出基于格剪枝的最优标识属性传播方法,实现溯源信息的最小代价传播。基于TPC-H Benchmark和人造数据集IAP-DB的实验结果验证了提出的基于标识属性传播的溯源方法可以高效实现数据起源信息传播。     

基于模糊多目标决策的智能仪表功能安全与信息安全融合方法

针对智能仪表典型功能模块和安全需求,文章设计了策略重叠消除和冲突消解相分离的融合方法框架,实现了对安全策略的形式化建模和属性特征提取.文章综合权衡安全防护能力、风险缓解程度和仪表资源受限等多方面因素,并考虑网络通信安全策略和控制行为动作安全策略在融合过程中的属性模糊偏好差异,得出最优的安全防护策略部署方案,通过仿真实验...     

位置不确定移动对象的连续概率反Skyline查询

为了确保包括非功能属性在内的服务规约与服务实际运行行为之间的一致性,提出一种Web服务运行时行为验证方法。首先对UML 2.0序列图进行扩展,将QoS属性和功能属性的描述统一起来,以精确表达Web服务的需求规约。然后,提出利用确定有限自动机构造出扩展序列图(Extended Sequence Diagrams,ESD)的语义模型的方法。最后,给出验证准则,根据Web服务的交互消息和规约建模的结果来验证Web服务运行时行为与需求规约之间的一致性。基于上述研究,设计开发了Web服务运行时验证工具(Runtime Verification Tool for Web Services,RVT4WS),以支持对Web服务运行时行为的验证。     

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.     

On the verification of intransitive noninterference in mulitlevel security.

We propose an algorithmic approach to the problem of verification of the property of intransitive noninterference (INI), using tools and concepts of discrete event systems (DES). INI can be used to characterize and solve several important security problems in multilevel security systems. In a previous work, we have established the notion of iP-observability, which precisely captures the property of INI. We have also developed an algorithm for checking iP-observability by indirectly checking P-observability for systems with at most three security levels. In this paper, we generalize the results for systems with any finite number of security levels by developing a direct method for checking iP-observability, based on an insightful observation that the iP function is a left congruence in terms of relations on formal languages. To demonstrate the applicability of our approach, we propose a formal method to detect denial of service vulnerabilities in security protocols based on INI. This method is illustrated using the TCP/IP protocol. The work extends the theory of supervisory control of DES to a new application domain.     

Security invariants in discrete transition systems

The Shadow semantics is a qualitative model for noninterference security for sequential programs. In this paper, we first extend the Shadow semantics to Event-B, to reason about discrete transition systems with noninterference security properties. In particular, we investigate how these security properties can be specified and proved as machine invariants. Next we highlight the role of security invariants during refinement and identify some common patterns in specifying them. Finally, we propose a practical extension to the supporting Rodin platform of Event-B, with the possibility of having some properties to be invariants-by-construction.     

基于信息流的多级动态可信度量模型

系统运行时受环境和各种外界因素影响,加之内部多实体间信息流相互干扰,可能会破坏系统的可信性,最终导致产生非预期输出。现有研究主要针对初始化可信硬件环境下实体的完整性度量,未能考虑机密性带来的可信影响,同时对于实体可信度量的频率未能与实体推进时机同步。基于此提出一种基于信息流传递理论的多级动态可信度量模型,该模型以信息流的非传递无干扰理论为依据,通过引入可信代理模块,设计一种多级安全访问控制策略,分别从实体完整性和机密性两方面对系统中实体进行动态可信性度量。最后给出该模型的形式化描述和可信证明,结合抽象系统实例来说明该模型的有效性,相比现有研究,所提模型具有更好的度量实时性,是一种上下文感知的细粒度可信度量模型。     

Characterizing intransitive noninterference for 3-domain security policies with observability

This note introduces a new algorithmic approach to the problem of checking the property of intransitive noninterference (INI) using discrete-event systems (DESs) tools and concepts. INI property is widely used in formal verification of security problems in computer systems and protocols. The approach consists of two phases: First, a new property called iP-observability (observability based on a purge function) is introduced to capture INI. We prove that a system satisfies INI if and only if it is iP-observable. Second, a relation between iP-observability and P-observability (observability as used in DES) is established by transforming the automaton modeling a system/protocol into an automaton where P-observability (and, hence, iP-observability) can be determined. This allows us to check INI by checking P-observability, which can be done efficiently. Our approach can be used for all systems/protocols with three domains or levels, which is sufficient for most noninterference problems for cryptographic protocols and systems.     

Secure Information Flow via Linear Continuations

Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style (CPS) as a means of proving that such languages enforce noninterference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features and linear continuations.Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state.     

Dynamic security labels and static information flow control

This paper presents a language in which information flow is securely controlled by a type system, yet the security class of data can vary dynamically. Information flow policies provide the means to express strong security requirements for data confidentiality and integrity. Recent work on security-typed programming languages has shown that information flow can be analyzed statically, ensuring that programs will respect the restrictions placed on data. However, real computing systems have security policies that cannot be determined at the time of program analysis. For example, a file has associated access permissions that cannot be known with certainty until it is opened. Although one security-typed programming language has included support for dynamic security labels, there has been no demonstration that a general mechanism for dynamic labels can securely control information flow. In this paper, we present an expressive language-based mechanism for reasoning about dynamic security labels. The mechanism is formally presented in a core language based on the typed lambda calculus; any well-typed program in this language is secure because it satisfies noninterference.     

Noninterference in a predicative polymorphic calculus for access control

Polymorphic programming languages have been adapted for constructing distributed access control systems, where a program represents a proof of eligibility according to a given policy. As a security requirement, it is typically stated that the programs of such languages should satisfy noninterference. However, this property has not been defined and proven semantically. In this paper, we first propose a semantics based on Henkin models for a predicative polymorphic access control language based on lambda-calculus. A formal semantic definition of noninterference is then proposed through logical relations. We prove a type soundness theorem which states that any well-typed program of our language meets the noninterference property defined in this paper. In this way, it is guaranteed that access requests from an entity do not interfere with those from unrelated or more trusted entities.     

非传递无干扰下IP安全与TA安全关系研究

IP安全适用于非传递策略的无干扰模型。但是，满足IP安全的系统中仍然存在类似于动作先后顺序这样的信息，因此，提出了新的无干扰模型TA安全。对非传递无干扰下IP安全和TA安全进行比较分析，给出函数[ipurge]与函数[ta]的差别条件，函数[ta]隐藏了动作序列中部分动作的先后顺序，这些动作的先后顺序对于安全域是一种额外的信息。然后，使用该差别条件，提出当系统满足IP安全时，使系统满足TA安全所需要的条件并进行形式化推导。     

一个完整的无干扰模型

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