随着信息技术的飞速发展,信息安全显得越来越重要,然而传统的基于类型的安全方法无法实现信息流的安全检测。基于类型的方法是逐个语句考察的,它不能整体把握数据流信息,会将一些原本安全的程序判定为不安全的,具有不完备性。而基于语义的方法是通过分析程序的执行语义来实现验证的目的的,因此基于语义的方法检测结果更准确。　　本文在分析程序具体语义的基础上,提出了一种新的信息保密性检测方法:首先,构造具体语义和抽象语义的对应关系;然后根据待测程序性质构建抽象语义,同时在抽象基础上,采用限界思想来优化检测的效率。通过本文方法,降低了程序检测的复杂性,同时减少了时间和空间的浪费,提高了检测的效率和准确度。在研究中取得主要成果有:　　1.基于抽象解释和限界模型检测理论,对C程序句法结构的解析过程进行分析研究。　　2.本文根据C程序的句法结构得出其标准语义。由于多级安全系统的复杂性,在标准语义的基础上,加入安全等级信息,再根据程序的变量和安全等级信息及相应的附属函数,得到C程序的具体语义。在对具体语义的解析过程中发现其只能表述简单的程序,对于庞大的程序,则会出现状态空间爆炸问题。因此,本文又将抽象解释和限界模型检测理论引入进来,对程序的变量、状态和内存进行抽象,尤其是在if和while语句分支和循环较多的程序里,其生成状态减少的幅度会很明显。这样,大大提高了检测效率。　　3.用时序逻辑公式描述C程序信息流保密性和完整性特性。首先对C程序信息流保密性和完整性进行分析,给出其相应的语义定义。之后,根据定义要求将保密特性和完整特性转化为时序逻辑公式,提高了检测的准确性。