随着国家、社会对计算机和网络技术的依赖程度日益增长,信息安全问题越来越重要。访问控制机制是保护信息机密性、完整性的重要手段,但即使实施了强制访问控制机制的安全系统中仍然会发生高安全级信息向低安全级用户泄漏的隐通道问题。信息的泄露本质上是信息的非法流动,因此信息流分析技术一直被用来寻找系统中潜在的各种信息泄露问题。该技术定义信息流安全属性刻画信息的合法流动,通过验证系统是否满足信息流安全属性来判断系统中是否存信息泄露,从而防止信息流向未被授权的用户。传统的信息流分析技术采用“展开方法”来验证信息流安全属性,但该方法仅适用于确定型系统,而对非确定型系统,该方法是可靠的,但不完备。本文以Petri网作为安全系统的模型,对安全属性设计了一套完备的验证算法。该算法主要通过计算Petri网的可达图实现,为了降低可达图的计算量,设计了Petri网上保持安全属性的化简规则。进一步针对系统均由很多个子系统组成,给出了保持安全属性的组合模式,从而只需分析子系统是否满足安全属性即可。本文的具体研究内容包括：1.提出Petri网上信息流安全属性的可靠完备的验证算法。首先以Petri网作为安全系统的模型,对信息流安全属性进行形式化定义,然后基于Petri网的可达图开发完备的安全属性验证方法。该方法从初始状态出发,计算Petri网中所有可执行变迁所引发的状态集合,通过分析变迁序列的执行对结果状态集的影响,来判断安全属性是否成立。完备的算法使我们既能判断属性成立,亦能判断属性不成立。2.提出Petri网的化简规则,并给出化简规则保持安全属性不变的证明。针对基于可达图的验证算法存在状态空间爆炸问题,提出三种Petri网的化简规则：库所化简规则,变迁化简规则,综合化简规则。这些规则剔除了Petri网中对验证安全属性没有影响的库所和变迁,从而使系统需要进行验证的可达图得到精简。为了说明化简规则的正确性,我们证明了对信息流安全属性,精简后的系统与原系统是等价的。3.提出Petri网上保持信息流安全属性的可组合模式,并给出证明。分析了在现有的Petri网组合方式下信息流安全属性的可组合性,提出了保持信息流安全属性的可组合模式,使得只要系统的组合方式满足给定的组合条件,组合后的系统也满足相应的属性。最后我们开发了基于Petri信息流安全属性验证系统原型。该系统用于验证系统是否满足信息流安全属性,并且在不满足的情况下给出信息泄漏的路径。