程序语言信息流安全讨论如何保证拥有对机密数据访问权限的程序不会以不恰当的方式传播机密数据,或者验证出程序是否会以不恰当的方式将机密数据传播给未授权方。广义上的信息流策略定义了信息安全地通过系统(程序)并最终流向外部的流动方式。该策略可能基于数据的保密性或完整性进行定义,本文讨论限定于保密性信息流策略。　　 当前程序语言信息流安伞领域的研究可从目标程序的语言特征、安全策略、实现机制等多个侧面进行界定。在语言特征方面,目标程序从函数式语言程序、命令式语言程序到面向对象语言程序,从顺序、确定性程序到并发、概率程序,从批处理程序到含有输入输出信道的程序及交互式程序;在安全策略方面,由作为基准策略的非十扰性策略到多个目标维度上的密级解除安伞策略;在实现机制方面则分为静态程序分析(包括类型系统、抽象解释、自动程序验证及基于程序切片和程序依赖图的方法等)和运行时信息流监测。　　 本文以下推系统作为抽象模型,提出一种使用自动程序验证作为机制支持信息流安全策略的方法。方法属于基于标准语义的方法。从语言特征角度,讨论了三种目标程序上的非干扰性策略:1.含一阶过程调用和递归调用的命令式语言程序(第三章),2.面向对象的Java虚拟机字节码语言程序(第四章),3.含输出信道和发散执行的命令式语言程序(第5.1节)。从安全策略角度,对于命令式语言程序首先讨论了终止不敏感/终止敏感非干扰性(第三章),然后讨论了支持机密信息合法释放的定界释放、不严格非干扰性、局部定界释放、定界不披露性、渐进释放和条件渐进释放(第5.2节)。　　 作为程序信息流安全验证机制的创新和下推系统模型检测方法的新应用,本文在已有下推系统模型检测工作基础上实现了程序语言信息流安全验证工具,主要贡献如下:　　 1.对含递归过程调用的命令式语言程序的终止敏感/终止不敏感非干扰性进行自动程序验证,考虑了递归调用对终止信道的影响。针对过程调用提出了两种自合成改进形式,实验说明方法相对于其他自动验证方法的验证效率优势。　　 2.首次将自动程序验证应用于Java字节码程序的非干扰性分析,提出的低安全级记录自合成使得可达性分析方法可用于信息流安全分析。克服了字节码应用环境对自动程序验证的一些限制以及在处理指针混淆时类型系统引入的保守性。实验说明方法的可用性、可扩展性及相对现有分析方法的验证效率优势。　　 3.将自动程序验证用于含显式输出信道的程序的非干扰性分析。方法演化后支持对发散程序的终止不敏感非干扰性的验证。实验说明与现有基于抽象解释的方法相比的精确性和验证效率提升。　　 4.首次提出了完全基于自动程序验证的局部定界释放、定界不披露性、渐进释放、条件渐进释放策略的验证机制。实验说明方法相比现有基于类犁系统的机制的精确性提升,且相比已有的对不严格非干扰性的自动程序验证具有效率优势。