Design and assurance strategy for the NRL Pump

The NRL Pump forwards messages from a low level system to a high level system and monitors the timing of acknowledgments from the high level system to minimize leaks. It is the keystone to a proposed architecture that uses specialized high assurance devices to separate data at different security levels. We describe the software design and assurance argument strategy for this device, the Network NRL Pump, which can be used in any multilevel secure distributed architecture. We have completed the system requirements and logical design of a prototype pump and are working on its physical design     

Advanced transaction processing in multilevel secure file stores

The concurrency control requirements for transaction processing in a multilevel secure file system are different from those in conventional transaction processing systems. In particular, there is the need to coordinate transactions at different security levels avoiding both potential timing covert channels and the starvation of transactions at higher security levels. Suppose a transaction at a lower security level attempts to write a data item that is being read by a transaction at a higher security level. On the one hand, a timing covert channel arises if the transaction at the lower security level is either delayed or aborted by the scheduler. On the other hand, the transaction at the high security level may be subjected to an indefinite delay if it is forced to abort repeatedly. This paper extends the classical two-phase locking mechanism to multilevel secure file systems. The scheme presented here prevents potential timing covert channels and avoids the abort of higher level transactions nonetheless guaranteeing serializability. The programmer is provided with a powerful set of linguistic constructs that supports exception handling, partial rollback, and forward recovery. The proper use of these constructs can prevent the indefinite delay in completion of a higher level transaction, and allows the programmer to trade off starvation with transaction isolation     

一种消除时间隐通道的方法调用控制策略

采用消息过滤算法可以在支持对象模型的多级安全系统中实现强制访问控制。但是,这种算法会引入时问隐通道,可能致使机密信息泄露。本文提出并实现了一种可信的控制策略,在消息过滤算法中采用异步消息传递方式消除时间隐通道,并对系统中对象方法的执行进行调度,确保消除时间隐通道不会导致执行结果不正确。     

多级安全数据库保密性和数据完整性研究

保密性、完整性和可用性是多级安全数据库必须具备的三要素,然而完整性和保密性的要求往往不一致,现有的多级安全系统一般采用牺牲数据完整性和可用性的方法来获得较高的保密性。该文通过对传统安全模型进行改造,使之具有较高的保密性、数据完整性和可用性。     

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

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

基于精化的TrustZone多安全分区建模与形式化验证

TrustZone作为ARM处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术,支持在安全世界建立多个隔离分区来缓解这个问题,但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构,提出一种基于精化的TrustZone多安全分区建模与安全性分析方法,并基于定理证明器Isabelle/HOL完成了分区管理器的建模和形式化验证.首先,基于逐层精化的方法构建了多安全分区模型RMTEE,使用抽象状态机描述系统运行过程和安全策略要求,建立多安全分区的抽象模型并实例化实现分区管理器的具体模型,遵循FF-A规范在具体模型中实现了事件规约;其次,针对现有分区管理器设计无法满足信息流安全性验证的不足,设计了基于DAC的分区间通信访问控制,并将其应用到TrustZone安全分区管理器的建模与验证中;再次,证明了具体模型...     

A model for multilevel security in computer networks

A model is presented that precisely describes the mechanism that enforces the security policy and requirements for a multilevel secure network. The mechanism attempts to ensure secure flow of information between entities assigned to different security classes in different computer systems connected to the network. The mechanism also controls the access to the network devices by the subjects (users and processes executed on behalf of the users) with different security clearances. The model integrates the notions of nondiscretionary access control and information flow control to provide a trusted network base that imposes appropriate restrictions on the flow of information among the various devices. Utilizing simple set-theoretic concepts, a procedure is given to verify the security of a network that implements the model     

A hookup theorem for multilevel security

A security property for trusted multilevel systems, restrictiveness, is described. It restricts the inferences a user can make about sensitive information. This property is a hookup property, or composable, meaning that a collection of secure restrictive systems when hooked together form a secure restrictive composite system. It is argued that the inference control and composability of restrictiveness make it an attractive choice for a security policy on trusted systems and processes     

A trusted access method in software-defined network

In software-defined networks (SDN), most controllers do not have an established control function for endpoint users and access terminals to access network, which may lead to many attacks. In order to address the problem of security check on access terminals, a secure trusted access method in SDN is designed and implemented in this paper. The method includes an access architecture design and a security access authentication protocol. The access architecture combines the characteristics of the trusted access technology and SDN architecture, and enhances the access security of SDN. The security access authentication protocol specifies the specific structure and implementation of data exchange in the access process. The architecture and protocol implemented in this paper can complete the credibility judgment of the access device and user's identification. Furthermore, it provides different trusted users with different network access permissions. Experiments show that the proposed access method is more secure than the access method that is based on IP address, MAC address and user identity authentication only, thus can effectively guarantee the access security of SDN.     

基于代码路径的安全操作系统性能优化方法

为了满足面向访问验证保护级的要求, 研发新一代高等级安全操作系统, 我们采用微内核的架构设计和实现了面向访问验证保护级的安全操作系统原型系统(VSOS), 并通过设计和实现新的访问监控器来满足安全内核设计原则中的不可旁过和总是被调用两项要求, 但访问监控器的引入导致VSOS的性能产生较大的损耗. 提出了一种基于代码路径优化的方法, 用于改进访问监控器的实现和调用方式, 以及可信路径机制的实现方式. 实验表明, 通过此方法VSOS的性能和可信路径过程的用户体验都得到了提升.     

可信计算在P2P系统中的应用

用户可以使用P2P系统高效地实现大规模信息的共享。然而,由于缺乏共享信息的完整性和认证性机制,现有的P2P系统易于受到各种安全攻击。作为工业界的标准,可信计算技术为类似问题提供了一个革命性的解决方案。提出了一种可信计算架构,实现P2P系统的完整性和认证性。     

区块链在数据安全领域的研究进展

大数据时代,数据已成为驱动社会发展的重要的资产.但是数据在其全生命周期均面临不同种类、不同层次的安全威胁,极大降低了用户进行数据共享的意愿.区块链具有去中心化、去信任化和防篡改的安全特性,为降低信息系统单点化的风险提供了重要的解决思路,能够应用于数据安全领域.该文从数据安全的核心特性入手,介绍区块链在增强数据机密性、数...     

基于TrustZone的可信移动终端云服务安全接入方案

可信云架构为云计算用户提供了安全可信的云服务执行环境,保护了用户私有数据的计算与存储安全. 然而在移动云计算高速发展的今天, 仍然没有移动终端接入可信云服务的安全解决方案. 针对上述问题, 提出了一种可信移动终端云服务安全接入方案, 方案充分考虑了移动云计算应用背景, 利用ARM TrustZone硬件隔离技术构建可信移动终端, 保护云服务客户端及安全敏感操作在移动终端的安全执行, 结合物理不可克隆函数技术, 给出了移动终端密钥与敏感数据管理机制. 在此基础之上, 借鉴可信计算技术思想, 设计了云服务安全接入协议, 协议兼容可信云架构, 提供云服务端与移动客户端间的端到端认证. 分析了方案具备的6种安全属性, 给出了基于方案的移动云存储应用实例, 实现了方案的原型系统. 实验结果表明, 可信移动终端TCB较小, 方案具有良好的可扩展性和安全可控性, 整体运行效率较高.     

Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone

As a trusted execution environment technology on ARM processors, TrustZone provides an isolated and independent execution environment for security-sensitive programs and data on the device. However, running the trusted OS and all the trusted applications in the same environment may cause problems---The exploitation of vulnerabilities on any component may affect the others in the system. Although ARM proposed the S-EL2 virtualization technology, which supports multiple isolated partitions in the secure world to alleviate this problem, there may still be security threats such as information leakage between partitions in the real-world partition manager. Current secure partition manager designs and implementations lack rigorous mathematical proofs to guarantee the security of isolated partitions. This study analyzes the multiple secure partitions architecture of ARM TrustZone in detail, proposes a refinement-based modeling and security analysis method for multiple secure partitions of TrustZone, and completes the modeling and formal verification of the secure partition manager in the theorem prover Isabelle/HOL. First, we build a multiple secure partitions model named RMTEE based on refinement: an abstract state machine is used to describe the system running process and security policy requirements, forming the abstract model. Then the abstract model is instantiated into the concrete model, in which the event specification is implemented following the FF-A specification. Second, to address the problem that the existing partition manager design cannot meet the goal of information flow security verification, we design a DAC-based inter-partition communication access control and apply it to the modeling and verification of RMTEE. Lastly, we prove the refinement between the concrete model and the abstract model, and the correctness and security of the event specification in the concrete model. The formalization and verification consist of 137 definitions and 201 lemmas (more than 11,000 lines of Isabelle/HOL code). The results show that the model satisfies confidentiality and integrity, and can effectively defend against malicious attacks on partitions.     

Towards multilaterally secure computing platforms—with open source and trusted computing

We present a security architecture for a trustworthy open computing platform that aims at solving a variety of security problems of conventional platforms by an efficient migration of existing operating system components, a Security Software Layer (PERSEUS), and hardware functionalities offered by the Trusted Computing technology. The main goal is to provide multilateral security, e.g., protecting users' privacy while preventing violations of copyrights. Hence the proposed architecture includes a variety of security services such as secure booting, trusted GUI, secure installation/update, and trusted viewer. The design is flexible enough to support a wide range of hardware platforms, i.e., PC, PDA, and embedded systems. The proposed platform shall serve as a basis for implementing a variety of innovative business models and distributed applications with multilateral security.     

Multilevel security: reprise

Multilevel security is the prevention of unauthorized disclosure among multiple information classes. The threat source for the disclosures includes unauthorized users and subverted software operating on behalf of authorized users. The terminology might be more explicit if we could call this concept multidomain confidentiality, but it is worth resisting multiplying terminology. Nonetheless, we should understand that multilevel security means multidomain confidentiality. The author asks if there is less need for multilevel security today, and if there is still a need, how we might address it.     

Provably secure identity-based authenticated key agreement protocols with malicious private key generators

Identity-based authenticated key agreement is a useful cryptographic primitive and has received a lot of attention. The security of an identity-based system relies on a trusted private key generator (PKG) that generates private keys for users. Unfortunately, the assumption of a trusted PKG (or a curious-but-honest PKG) is considered to be too strong in some situations. Therefore, achieving security without such an assumption has been considered in many cryptographic protocols. As a PKG knows the private keys of its users, man-in-the-middle attacks (MIMAs) from a malicious PKG is considered as the strongest attack against a key agreement protocol. Although securing a key agreement process against such attacks is desirable, all existent identity-based key agreement protocols are not secure under such attacks. In this paper, we, for the first time, propose an identity-based authenticated key agreement protocol resisting MIMAs from malicious PKGs that form a tree, which is a commonly used PKG structure for distributing the power of PKGs. Users are registered at a PKG in the tree and each holds a private key generated with all master keys of associated PKGs. This structure is much more efficient, in comparison with other existing schemes such as threshold-based schemes where a user has to register with all PKGs. We present our idea in two protocols. The first protocol is not secure against MIMAs from some kinds of malicious PKGs but holds all other desirable security properties. The second protocol is fully secure against MIMAs. We provide a complete security proof to our protocols.     

Design of secure operating systems with high security levels

Numerous Internet security incidents have shown that support from secure operating systems is paramount to fighting threats posed by modern computing environments. Based on the requirements of the relevant national and international standards and criteria, in combination with our experience in the design and development of the ANSHENG v4.0 secure operating system with high security level (hereafter simply referred to as ANSHENG OS), this paper addresses the following key issues in the design of secure operating systems with high security levels: se- curity architecture, security policy models, and covert channel analysis. The design principles of security architecture and three basic security models: confidentiality, integrity, and privilege control models are discussed, respectively. Three novel security models and new security architecture are proposed. The prominent features of these proposals, as well as their applications to the ANSHENG OS, are elaborated. Cover channel analysis (CCA) is a well-known hard problem in the design of secure operating systems with high security levels since to date it lacks a sound theoretical basis and systematic analysis approach. In order to resolve the fundamental difficulties of CCA, we have set up a sound theoretical basis for completeness of covert channel identification and have proposed a unified framework for covert channel identification and an efficient backward tracking search method. The successful application of our new proposals to the ANSHENG OS has shown that it can help ease and speedup the entire CCA process.     

基于属性封印的可信传输协议设计

基于非对称密码学的传统信息交换机制中,通过密钥实现信息保密及平台身份认证的方式存在较多安全不足.由此,基于可信计算研究的新PC体系结构提出一种实现传输终端配置安全性认证和保障数据传输及使用安全的信息传输方案,并且基于属性封印的思想,采用Pederson承诺和离散对数不等的零知识证明该方案,设计了具体密码协议以实现该方案.通过随机预言模型证明了该协议的安全性,并将该协议应用于一个真实的移动支付实例,展示了其使用方式.     

A novel policy-driven reversible anonymisation scheme for XML-based services

This paper proposes a reversible anonymisation scheme for XML messages that supports fine-grained enforcement of XACML-based privacy policies. Reversible anonymisation means that information in XML messages is anonymised, however the information required to reverse the anonymisation is cryptographically protected in the messages. The policy can control access down to octet ranges of individual elements or attributes in XML messages. The reversible anonymisation protocol effectively implements a multi-level privacy and security based approach, so that only authorised stakeholders can disclose confidential information up to the privacy or security level they are authorised for. The approach furthermore supports a shared secret based scheme, where stakeholders need to agree to disclose confidential information. Last, it supports time limited access to private or confidential information. This opens up for improved control of access to private or confidential information in XML messages used by a service oriented architecture. The solution provides horizontally scalable confidentiality protection for certain types of big data applications, like XML databases, secure logging and data retention repositories.