摘要： 在分析程序具体语义的基础上，提出一种信息保密性检测方法。构造具体语义和抽象语义的对应关系，根据待测程序性质构建抽象语义，同时在抽象基础上，采用限界思想来优化检测的效率。通过该方法降低程序检测的复杂性，减少时间和空间的浪费，提高了检测的效率和准确度。

关键词: 信息流安全, 模型检测, 抽象解释

Abstract: Based on the analysis of the concrete semantics of programs, this paper proposes a method to detect the information privacy. It establishes corresponding relation between concrete semantics and abstract semantics, then establishes abstract semantics according to the properties of the programs to be checked, and meanwhile adopts bound methods to optimize detecting efficiency on the basis of abstraction. By this method, the complexity of program detecting is reduced, and the efficiency is raised and accuracy of detection is improved.

Key words: information flow security, model checking, abstract interpretation

中图分类号: 

• TP311.5