静态检测技术(Static Detection)

静态检测技术是指对被测软件的源程序或者二进制代码进行扫描，从语法、语义上理解程序的行为，直接分析被检测程序的特征，寻找可能导致错误的异常。具体的扫描过程可以使用采取形式化验证技术的程序扫描，或者手工测试的方法。

二进制对比技术(Binary Contrast)和词法分析(Lexical Analysis)是针对软件代码进行审查的检测技术，这类技术具有简单高效的优势，但是只针对代码本身特征的检查并不能很好的检查出具有逻辑关联的复杂漏洞，虽然可以对其中引入模式识别来加强检查时特征的匹配类型，也只能略微加强其检查特征；规则检查(Rule Check)是检测已知漏洞的一种代码扫描技术，对于已知类型漏洞，该技术具有高效且准确率高的特点，但是并不能检测未知类型的漏洞；类型推导(Type Inference)是针对编程语言本身的检测技术，自动化程度高，但是这种检查只能针对控制流不相关的漏洞；模型检测(Model Detection)是一种较为成熟的形式化检测方法，主要检测与时序相关的漏洞，但是这种检测方法对内存相关漏洞类型支持度不高，且检测时资源消耗大；定理证明(Theorem Proving)与符号执行(Symbolic Execution)检测方法偏重于理论证明，使用严格的数学推理进行，但是目前并没有与实际应用契合度高的算法出现。