Abstract: This paper summarizes two strategies of software security flaw detection, named static analysis and program verification. Several static detection methods such as lexical analysis, rule checking, type theory deduction, model checking, theorem proving, and symbol execution are also synthetically reviewed. It discusses the advantage, applicability and tendency of static detecting techniques.

Key words: software flaws security, static analysis, program verification

摘要： 软件安全漏洞问题日益严重，静态漏洞检测提供从软件结构和代码中寻找漏洞的方法。该文研究软件漏洞静态检测的两个主要方面：静态分析和程序验证，重点分析词法分析、规则检查、类型推导、模型检测、定理证明和符号执行等方法，将常用的静态检测工具按方法归类，讨论、总结静态检测技术的优势、适用性和发展趋势。

关键词: 软件安全漏洞, 静态分析, 程序验证

CLC Number: 

• TP309