开放系统的恶意代码防御模型

提出了一个适用于开放系统环境的恶意代码防御模型。把系统内部划分为可信域和不可信域,可信域由已标识客体和已授权主体构成,不可信域由未标识客体和未授权主体构成。为把低完整性级别的信息限制在不可信域以防范恶意代码对可信域的渗透和攻击,定义了主体授权规则、客体访问规则和主体通信规则。为使可信域可以安全地同外界进行信息交换,引入了可信完整性部件。可信完整性部件由安全性检查部件和可信度提升部件构成,其中前者对所有要进入可信域的客体进行安全性检查,后者把经检查被认为是安全的客体转移到可信域并提升其完整性级别,从而在不损害安全性的前提下提高系统的可用性。     

基于可信计算的保密和完整性统一安全策略

为解决在高安全等级操作系统应用的保密性/完整性统一多级访问控制模型可用性差问题及增强其安全性,为系统引入可信计算（TCPA）技术并指出它对安全机制的增强作用。对可信计算平台环境下保密性/完整性统一的访问控制模型中可信主体的特性进行描述,给出具体安全策略。它将可信主体纳入访问控制模型,有助于划分可信主体并能够限制其权限。     

面向移动Web操作系统的BLP改进模型及应用

作为重要的机密性策略经典模型,BLP模型通过对主体和客体进行分级和标记,并引入高安全等级的引用监视器,实现信息系统的强制访问。随着移动智能终端的普及,Web操作系统因其具有移动性、移植性、高扩展性和跨平台性等优点,成为移动政务系统的主要解决方案之一,并越来越受到研究人员的重视。但现有的Web操作系统对机密性要求不高,无法满足移动政务系统对安全保密的需求。本文从安全模型构建入手,对智能终端的Web操作系统进行抽象建模,并重定义BLP模型的元素,增强主客体的访问控制以提高其机密性。鉴于BLP模型缺乏可信主体的最小权限原则和完整性约束,本文在改进的BLP模型当中重新划分主体、客体的安全级,增加可信级别标记和角色映射函数,并针对现有的Web操作系统进行模型映射,实现了最小权限原则、主体完整性约束和域间隔离机制,可有效提高Web操作系统机密性等级。     

基于双重完整性的可信证明模型

传统可信远程证明方法对于动态证明问题描述不足,且在可信证明过程中,证明主/客体交互行为对于可信性的影响缺乏理论依据。为此,提出一种基于证明主/客体双重完整性的可信证明模型,在该模型中引入可信性概念,定义可信属性及可信状态的建立规则,根据该模型设计可信证明系统,并分析主/客体不同完整性的证明方法。     

基于平台可信等级的RBAC模型研究与改进

针对RBAC模型仅仅依靠用户身份进行角色和权限分配,未考虑用户平台的安全及可信性的问题,提出一种基于平台可信等级的改进RBAC模型(TLPRBAC)。TLPRBAC模型引入可信平台和可信等级两个实体元素,改进了实体关系和授权规则。改进的RBAC模型采用将角色与可信等级、可信等级与访问客体相关联的方法,实现不同可信等级主体对不同安全级别客体的细粒度访问控制。最后提出一个TLPRBAC模型在政府内网中的文件访问控制应用方案。     

NUTOS系统多策略安全模型设计与实现

传统的MLS策略侧重于信息机密性保护，却很少考虑完整性，也无法有效实施信道控制策略，在解决不同安全级别信息流动问题时采用的可信主体也存在安全隐患。为了在同一系统中满足多样性的安全需求，给出混合多策略模型——MPVSM模型，有机组合了BLP、Biba、DTE、RBAC等安全模型的属性和功能，消除了MLS模型的缺陷，提高了信道控制能力和权限分配的灵活度，对可信主体的权限也进行了有力的控制和约束。给出MPVSM模型的形式化描述以及在原型可信操作系统Nutos中的实现，并给出了策略配置实例。     

一种结合用户许可的多级安全策略模型

针对BLP模型存在“向上写”规则破坏数据完整性、主体分配权限过大及客体安全等级不变的问题,提出一种结合用户许可的多级安全策略模型。该模型利用可信度标识对主体写操作进行完整性保护,通过用户许可标识解决BLP模型和可信度标识存在的主体分配权限过大问题,结合系统管理员仲裁机制对修改的客体安全等级进行动态调整。理论分析表明,该模型能够保证系统的安全。     

基于Petri网的动态访问控制模型

访问控制是保障信息系统安全的一种主要机制,通过限定主体对客体的访问权限,确保对信息资源访问的合法性,达到保证信息的机密性、完整性和可用性的目的。通常,这种机制主要通过静态的访问控制矩阵实现,不随信息系统处理的任务变换而调整。利用Petri网的基本原理,提出了一种适合于信息系统的访问控制模型,随着信息系统的状态变化动态授予访问控制权限,实现对信息系统资源安全的动态保护。     

基于可信验证的DBMS访问控制模型

针对目前访问控制模型在系统的安全实现方面存在的不足,在RABC的基础上,提出了可信操作环境下基于可信验证的DBMS访问控制模型,该模型满足系统的保密性和完整性需求,最大程度实现信息双向流动,同时支持最小特权安全特性,是一个权限分配灵活的访问控制模型。     

扩展的BLP模型及其应用

分析经典BLP模型中的非可信主体当前敏感级fC和“宁静原则”存在的不合理性,针对该问题,利用动态变化的主体敏感级v-max/a-min代替主体当前敏感级fC。为解决完整性保护问题,提出一个扩展的BLP模型,模型中引入主体的完整性和主客体的可信度,对于客体可信度,从完整性和可信性2个方面进行保护,同时对主体的可信度采用动态变化原则,并给出一个EBLP模型在操作系统中的应用实例。     

基于可信等级的BLP改进模型

BLP模型存在完整性保护缺失、可信主体定义不明确和未考虑平台环境因素等问题。为此,提出一种基于可信等级的BLP改进模型TL-BLP。该模型引入主客体和平台的可信等级,并对BLP模型安全特性、主客体的敏感标记和状态转移规则进行改进,从而实现可信度的动态度量,保证访问操作平台的安全性,通过对BLP模型“下读上写”的限制,保证信息的完整性。分析结果表明,TL-BLP在保证信息机密性的基础上,能提高系统的完整性和可用性,实现基于可信度的访问控制。     

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

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

A trusted subject architecture for multilevel secureobject-oriented databases

We address security in object-oriented database systems for multilevel secure environments. Such an environment consists of users cleared to various security levels, accessing information labeled with varying classifications. Our purpose is three-fold. First, we show how security can be naturally incorporated into the object model of computing so as to form a foundation for building multilevel secure object-oriented database management systems. Next, we show how such an abstract security model can be realized under a cost-effective, viable, and popular security architecture. Finally, we give security arguments based on trusted subjects and a formal proof to demonstrate the confidentiality of our architecture and approach. A notable feature of our solution is the support for secure synchronous write-up operations. This is useful when low level users want to send information to higher level users. In the object-oriented context, this is naturally modeled and efficiently accomplished through write-up messages sent by low level subjects. However, such write-up messages can pose confidentiality leaks (through timing and signaling channels) if the timing of the receipt and processing of the messages is observable to lower level senders. Such covert channels are a formidable obstacle in building high-assurance secure systems. Further, solutions to problems such as these have been known to involve various tradeoffs between confidentiality, integrity, and performance. We present a concurrent computation model that closes such channels while preserving the conflicting goals of confidentiality, integrity, and performance. Finally, we give a confidentiality proof for a trusted subject architecture and implementation and demonstrate that the trusted subject (process) cannot leak information in violation of multilevel security     

一种面向网络信息系统的TCP应用架构设计

针对可信计算平台在网络信息系统中的应用需求,提出了一种面向网络信息系统的TCP应用架构TCPAA。将该架构主要分为访问认证子系统和信息交互子系统两部分来进行设计。在访问认证子系统中,为了增强可信计算应用的灵活性,提出一种基于证明代理的可信验证机制PATAM,并对改进的访问认证模式进行了协议设计和流程说明。在信息交互子系统中,设计了内外网之间数据的可信传输流程,并提出了一种改进的金字塔可信评估模型PTAM。最后通过测试实验验证了该架构的良好性能。研究结果表明,该方案对于网络信息系统环境内可信计算平台的应用开发具有良好的通用性。     

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.     

基于Web操作系统的移动瘦终端多安全策略模型

高安全级移动办公对信息系统不断提出更高的安全需求,在此背景下出现了瘦终端(Thin-Client)解决方案。其采用云存储、分布式终端系统和集中管理,为用户提供了更好的安全性。当前的主要技术包括虚拟桌面和Web终端,其中前者是主流。近年来,Web操作系统(Web OS)的发展促使Web终端受到业界重视,但Web OS还存在机密性和完整性保护不足的问题。基于Web OS系统的特点抽象建模,提出了混合机密性模型BLP和完整性模型Biba的多安全策略模型。首先利用格将机密性标签、完整性标签和范畴集合相结合,解决了BLP与Biba信息流相反的问题;然后提出可信主体的最小特权原则来进一步约束可信主体的权限,并给予特定可信主体临时权限,以提高灵活性和可用性;最后分析模型的安全性和适用性。     

隐通道传递信息机理的研究

可信计算机系统中一些隐蔽数据流避开了安全机制的监控，造成信息的泄漏。本文通过对这种隐蔽流泄漏信息的机理进行分析和抽象，提出了一个通道元模型。将每一类通道元看成一个有限状态机，以Plotkin的结构化操作语义等为基础，计算出状态机的状态变化序列。通过对不满足隐通道定义的状态变迁序列的归纳，得到了抽象机中安全状态转移的约束条件，找出两个通道元通过共享客体泄露信息的工作机理，从而开发出一种基于操作语义的隐通道标识方法。对电梯调度算法模型进行实验，可有效地标识出存在的隐通道。     

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

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

基于可信密码模块的SoC可信启动框架模型

为满足嵌入式终端对信息安全的要求,设计了基于可信密码模块的SoC可信启动框架。该框架的特点在于对引导程序U-boot做功能上的分割,且存储在不同的非易失性存储器中,并增设了通信模块,使之在操作系统启动之前就具有发送和接收文件的功能。将引导程序的各部分与操作系统核心文件均作为可信实体,发送至可信密码模块进行完整性度量,若度量成功则可信密码模块返回下一阶段的启动信号并在其本地存储器中保存可信实体;若度量失败则禁止启动。实验结果表明,该框架是可行、有效的,可以满足现今嵌入式终端在信息安全方面的需要。