高保证系统指的是那些给出了确切证据证实该系统能够满足一系列重要安全属性的系统,主要体现在系统安全功能的可靠、完备以及可验证性等方面。高保证系统对系统的安全性有着严格的要求,因而该系统在设计和分析时也需要严格进行考虑。但是对高保证系统的具体设计和实现并不容易,面临的问题包括系统结构过于复杂导致对其进行形式化的描述和验证非常困难、系统的可信计算基(Trusted Computing Base, TCB)的规模会随着安全功能的增多而变得过于庞大、需要对当前的计算和网络环境进行改造以适应对信息进行安全标记的处理能力等。多独立安全级(Multiple Independent Levels of Security and Safety, MILS)的概念为高保证安全系统的设计提供了新的思路,MILS将传统的多级安全系统分割成了多个单级安全的组件域,通过少量的多级安全组件将这些安全域连接起来。多独立安全级基于隔离和信息流控制的概念,支持在一个系统中同时存在可信和不可信的组件,最终确保整个安全解决方案无法被旁路、可评估、总是被调用并且无法篡改。云计算技术与MILS的思想在很大程度上契合,结合MILS概念构建的私有云,能够利用云计算的硬件资源复用和动态资源的组织和分配机制等优势,可以快速、灵活地构建安全域,同时这些安全域也能够为不同语义环境的操作系统、应用、数据库、网络协议等提供高度的兼容性,从而使得诸如商用操作系统等不可信的组件可以得到应用,有效减小了TCB的规模。但是云计算自身的安全问题使得云计算技术与MILS和高保证系统相结合会让云计算的使用者无法完全信任云计算环境,这导致能否使用云计算技术构建满足高保证安全要求的系统尚存疑问；同时尽管基于MILS的满足高保证安全要求的云环境相对而言降低了系统的复杂度,但是仍然缺乏一个整体的形式化描述和验证,难以满足CC标准的EAL4级以上的要求；最后,基于MILS的云计算系统中,安全措施之间彼此的支撑和协调关系难以得到验证,是否能够满足系统整体的安全策略尚未可知。MILS思想的一个核心问题就是隔离,而恰恰隔离也是云计算所面临的关键问题之一,能否在租户之间形成可靠的隔离,决定了租户数据的安全,同时影响了租户对云计算的信任程度；能否有效隔离不同的应用(组),决定了不同级别的信息是否串流,或单一的安全缺陷是否能威胁到整个系统。本文针对云计算环境下高保证的隔离问题进行研究,主要的贡献包括：(1)在云计算环境中,由于基础设施的拥有者和维护者与基础设施的使用者并不相同,因此彼此之间存在一种对手关系。所以,为厂增强云计算便用者对云计算服务的信心,云计算服务提供者应当采取一定的措施向使用者证明其服务的可信,以赢取使用者的信任。关于可信云的研究探讨了这个问题,并指出增强服务的透明性是提高云计算服务可信度的有效方法,即允许使用者参与云计算平台的管理,使其能够自主制定与自己相关的安全策略,对自己的数据和业务进行控制,同时云服务提供者应当提供关于自身的可信证明,确保由提供者负责的部分符合使用者的安全预期。在这一思想的基础上,本文提出了一种多级管理机制,明确了云服务提供者和使用者的职责,使使用者能够参与到对自己的数据、应用以及资源的安全维护和管理中,提升了使用者的信心。在这一多级管理机制的基础上,本文提出了一种租户隔离模型,描述了租户与租户之间的隔离关系,包括租户的管理,以及租户对自身租用的资源的访问控制等。另外,由于云环境中用于承载应用的虚拟资源是动态分布的,同时与物理平台并不存在绑定关系,因此应用的边界往往会随着资源的变化而变化。这一特性使得租户的隔离必须以面向应用的抽象资源的隔离为基础,以确保租户之间的隔离不会因为抽象资源的隔离不当而失效。因此本文提出了一种应用的隔离模型,从租户应用的角度,描述了云环境中资源的分配和调度,确保了在云计算动态资源分配的前提下,不同应用能够保持隔离状态,为租户的隔离提供基础。(2)由于云计算系统过于庞大和复杂,因此对其进行整体的形式化描述和验证相当困难。而对于云计算系统来说,虚拟机之间的“感知”和“影响”可以用无干扰理论提供的信息流语义进行描述。信息流能够有效描述系统中的交互过程,因此可以用来分析复杂系统的安全属性。本文结合云计算自身的特性,从信息流的角度分析了云计算系统中的隔离问题,形式化描述了云计算系统中的信息流动过程,提出了相应的隔离规则,并证明了这些规则符合无干扰模型定义的信息流安全。(3)在进行复杂系统的设计时,往往采用自顶向下的方法,即从一个原始而抽象的体系结构出发,对其一步步细化,最终达到具体的、可实现的细节架构。但是在这一细化过程中,由于系统整体结构在不断变化,因此系统最初的安全性设计、安全功能之间的支撑关系能否得到保留,并不能得到保证。TCB层次化扩展是一种用于描述计算机系统中安全功能之间彼此支撑关系的概念,从一个TCB初始核心出发,经过逐层扩展,最终形成一个由可信管道连接起来的TCB子集组成的层次化结构。TCB层次化扩展与系统结构细化方法尽管在细节上存在诸多不同,但是仍然能够用TCB层次化扩展的思想来指导系统结构细化。通过在系统结构细化的过程中引入管道的概念,设计了一种新的自顶向下的结构化设计模型,确保安全功能之间彼此支撑的关系不会在细化过程中被破坏,同时系统原始的安全性能够得到保留。这一模型能够解决MILS系统设计中面临的安全功能之间缺乏联系的问题,同时这种模型对设计、实现原型系统具有指导作用。(4)实现了一种私有云环境的原型系统来对本文提出的部分关键技术进行了验证。其中构建了三个子网络的私有云环境；云中不同的应用(组)之间使用openflow技术彼此隔离,同时这种隔离具有灵活性以及动态响应等特征；用户的数据通过加密通道的方法进行存储和隔离,并使用单向传输进行在隔离基础上的共享：使用虚拟桌面分离了用户终端和操作平台,并使用基于中间人的虚拟桌面信息流控制机制来确保用户终端和操作平台之间信息流的可控。综上所述,本文着重讨论了高保证安全条件下的云计算环境中的隔离问题,包括租户隔离、应用隔离、信息流隔离等,对于能否真正运用云计算构建满足高保证安全要求的计算环境,以及云计算技术与MILS思想相结合能否推动高保证系统的进一步发展,具有十分积极的理论和现实意义。