云计算通过网络提供各种服务,这种开放式的模式在方便用户访问和使用的同时,也带来了潜在的安全隐患,导致来自云计算内部或者外部的攻击日益增多。云计算中,虚拟机或者用户之间存在数据泄露的危险,不管是直接的或间接的数据泄漏,都可以看作是信息的非法流动。访问控制等方法可以控制显式信息流,无法控制隐式信息流,需要使用无干扰模型检测云计算架构中是否存在非法信息流,典型的无干扰模型不适用于云计算架构中的信息流验证。云计算架构的设计,是一个由简单到复杂的过程。简单的云计算架构便于形式化的验证其安全属性,复杂的云计算架构便于具体实现。复杂的云计算架构由简单的云计算架构细化得到。安全是制约云计算发展的瓶颈之一,在云计算架构设计时,就要考虑其安全属性,并在云计算架构的细化过程中保持架构的安全属性。在云计算架构细化的过程中,云计算架构的安全属性是否保持,典型的细化方法不解决这方面的问题。针对上述问题,本文研究无干扰模型的特性、无干扰模型间的关系,在此基础上,提出保持云计算架构细化中的安全属性的方法以及适用于云计算中信息流安全的模型。主要内容和创新点如下：(1)研究传递无干扰模型和非传递无干扰模型,分析这些无干扰模型具有的特性,对特性进行理论推导。无干扰模型的特性是研究云计算中信息流安全的基础。传递无干扰模型包括P安全模型；非传递无干扰模型包括IP安全模型、TA安全模型等。它们既有相似的特性,也有不同特性。P安全模型、IP安全模型和TA安全模型都存在最小动作序列,而P安全模型和IP安全模型的最小动作序列是唯一的,TA安全模型的最小动作序列不唯一。P安全模型和IP安全模型具有幂等性,即动作序列经过函数一次处理的结果与经过函数多次处理的结果相同,TA安全模型一般没有这个特性。本文通过提取算法(其作用是提取函数处理结果中对应原动作序列的子序列),这样再通过函数处理,TA安全模型也能具有与幂等性相似的特性。另外,对这些无干扰模型的特性进行了深入的分析和理论验证。(2)研究非传递无干扰模型IP安全和TA安全的关系,提出IP安全模型转化为TA安全模型的条件,证明了条件的充分性和完备性。无干扰模型间的关系是研究云计算中信息流安全的基础。IP安全模型和TA安全模型是非传递策略下两个重要的无干扰模型,其中TA安全模型隐藏了更多信息。通常情况下,如果系统满足TA安全模型,那么系统一定满足IP安全模型。反之,系统满足IP安全模型,但是系统不一定满足TA安全模型。本文分析了两种模型的内在关系,在系统满足IP安全模型的前提下,提出了限制系统的条件,在该条件的限制下,系统满足TA安全模型。另外,从理论上验证了该条件的充分性和完备性。(3)研究云计算架构细化中的安全属性的保持,提出架构细化中保持无干扰属性的方法。无干扰对于架构而言是一种安全属性,传统的架构细化方法不考虑安全属性的保持。本文提出的架构细化方法,包含细化函数和若干限制规则,细化函数细化架构中的安全域,若干限制规则限制细化后安全域间的信息流。使用该方法细化后的架构,当原架构满足无干扰属性,那么细化后的架构满足无干扰属性。另外,从理论上证明了该方法的充分性。给出了具体例子,说明方法的可用性。(4)研究云计算中的信息流安全模型,提出适用于云计算的无干扰模型。云计算是一个多用户并发访问和顺序访问共存的架构,用户可能并发访问云计算服务,也可能顺序访问云计算服务。传统的无干扰模型不能处理云计算并发访问产生的信息流的安全问题。本文提出了适用于云计算并发访问的无干扰模型,云计算中的并发访问动作执行时,安全域与安全域不会相互信息流,即安全域间没有信息流动;在此基础上,进一步提出了并发访问和顺序访问共存的云计算无干扰模型,在顺序访问动作执行时,安全域之间信息可以按既定规则流动,而并发访问动作执行时,安全域间不应该有信息流动。另外,给出了模型的扩展定理和判定算法,可以判定云计算架构是否满足给定的无干扰模型。综上所述,本文以解决云计算中信息流安全问题及云计算架构细化中安全属性保持问题为目标,分析无干扰模型的特性及无干扰模型间的关系,给出无干扰模型的转换条件,确定无干扰模型间的区别所在,解决无干扰模型间转换问题。在此基础上,提出了细化方法和适用于云计算的无干扰模型,解决架构细化中无干扰属性保持问题以及云计算架构中的隐式信息流安全问题。