隐通道的危害在信息交流日渐重要的今天越来越突出,隐通道通过利用安全系统中具有较高安全级别的主体或进程根据事先约定好的编码方式,通过更改共享资源的属性并使低安全级别的主体或进程观察到这种变化,来传送违反系统安全策略的信息。因此,通过隐通道窃取机密信息的手段并不能被安全模型阻止,或者说,安全模型对于通过隐通道进行的信息攻击无能为力。由于一个大型多安全级软件系统的信息传递关系非常复杂,在信息流图的层面上直接进行信息流分析并搜索隐通道的工作量非常大,为进一步提高搜索和分析隐通道的效率,本文在已经提出信息流图的基础上提出一种将信息流图分割成信息流森林的算法,该算法首先选定一棵父树,然后通过边割集中的弧置换父树中的树枝得到新树,并能从理论上保证分割后得到的信息流森林正确继承原图的信息,即原图中信息流既未被割裂也未丢失。通过对每棵信息流树表示的信息流进行分析即可取代对整个信息流图的分析,从而有效降低了分析问题的规模。接着,本文引入PVS原型验证系统(Prototype Verification System)进行信息流的隐通道研究。首先,利用PVS的规约语言描述信息流,并提出相应的引理和定理。再用PVS定理证明器证明信息流中是否存在可能的隐通道。一个规约相当于一套公理系统,提出一系列关于此公理系统的定理,如果规约是正确的,那么这些定理即成立。因此,在本研究中如果信息流中存在可能的隐通道,则PVS的证明将不能通过,如果信息流中不存在可能的隐通道,则PVS将完成既定的证明。文中使用两个经典的隐通道案例来说明信息流森林的构造和体现本文完整的工作,同时展现了运用本文提供的模型、算法和原型验证系统可以大大减少隐通道分析时的人工工作量。