代码审计的主要方法
    如果想要在程序中寻找漏洞，或想找出目标程序中所有的漏洞，需要有明确的方法论来做指导。方法论的选择视目标程序和要寻找的漏洞而定。从方法论的角度出发，宏观来看代码审计的主要方法可以分为自顶向下、自底向上和两者相结合的三种方法。
    采用自顶向下(明确的)的方法，审计者不必深入了解目标程序。优点是效率较高，但缺点是可能会遗漏那些需要深入了解目标程序上下文才能发现的漏洞、跨越多段代码的漏洞等。该方法比较适合寻找那些只读一行代码就能识别的漏洞。
    采用自底向上的方法，审计者需要阅读大部分的源码来了解程序的内部工作机理。一般是从main 函数开始，从进入点一路读到退出点，从而对程序有一个全面的了解。会耗费大量时间，但由于全面地了解了程序有可能会发现更多、更复杂的漏洞。
    通常，任何代码库都有死代码(运行过程中基本或完全不会被执行的代码)，并占有相当大的比例。在死代码中寻找漏洞是劳而无功的，因为它们几乎不会被触发。因此审计那些最有可能包含安全问题而又可以被利用的代码段会更有意义。结合法中，审计者先通过输入定义的攻击者来定位可疑的代码，然后把大部分精力放在小范围代码段上。当然，全面了解代码的关键部分也非常有用。如果不知道正在审计的代码段在做什么或它适合于程序的哪个地方，那就应当了解它的上下文情况。
    在以方法论的角度了解当前代码审计的三种方法之后，从具体的实施方案来看，目前代码静态分析采用的方法主要有模式匹配、定理证明、模型检测等。
    (1)模式匹配
    模式匹配是静态分析最早采用的方法，主要步骤是依据统计及经验，定义和抽象缺陷及错误特征，对目标代码采用行走检查、模式匹配等方法过滤已知缺陷。如针对C 语言的LCLint1，针对Java 语言的FindBugs 、JLint 等。FindBugs 共定义了不良实现方法、正确性、实验性、国际化标准、恶意代码漏洞、多线程正确性、性能、安全等几大类缺陷，具体有300 多种缺陷模式，然后结合数据流分析技术，检测吕标代码中的缺陷。JLint的特点是基于数据流分析和内存使用情况，检测程序中可能存在的死锁情况，在句法检查方面和FindBugs 具有相同性，可以发现无效的指针、死锁、数组越界、除零错误、字符串相等判断、子类重写错误等。
    但是，模式匹配算法存在的根本性问题是模式固定且扩展困难，且然FindBugs 等工具具有一定的扩展性，允许自定义缺陷模式，但是自定义的缺陷模式仍然在编码规则、句法错误之类的缺陷范围之内，具有局限性。考虑到这种不足，后来的研究中基于模式匹配的检测方法更多应用于针对性的缺陷检测，如缓冲区溢出、程序不可达路径、程序忽视条件等，以及Web 程序里的SQL 注入、跨站脚本攻击等。将缓冲区是做一个整数对，分别为分配的内存大小和正在使用的字节数，然后规定分配的内存大小至少和正在使用的字节数一样大，以此来检测缓冲区溢出。分析得出大部分的程序不可达路径表现出相同的特征，而这些特征是由同一/补充决策、相互"专用决策、检测后执行、依据标签循环等四种模式引起的，通过识别源代码中的特征，能够精确检测程序不可达路径。
    基于模式匹配方法的静态检测在检测效率上具有优势，但是却导致了较高的误报率和漏报率，同时，不同检测依据的模式库不一样，也导致了不同检测工具的检测结果存在较大出入，检测结果的精确度不高，这在软件质量要求越来越高的发展中显然是不能满足需要。模式匹配方法的局限性其实可以归结为模式定义本身的不足，同时也决定了模式匹配方法只能用来检测具有固定模式的缺陷，不具有很好的普遍性。
    (2) 定理证明
    定理证明是代码形式化验证中的重要技术，也属于静态代码分析的范畴。定理证明技术是将软件系统和性质都用逻辑方法来规约，通过基于公理和推理规则组成的形式系统，以定理证明的方法来证明软件系统是否具备所期望的关键性质。从原理上讲，定理证明方法非常强大，能证明各种程序的正确性。基于定理证明方法的程序缺陷检测也有很多成果。轻量级定理证明，以灵活和高效的方式调试和验证需要管理指针，减少缺陷的来源。ESC/Java5 基于定理证明方法，首先给开发者提供了用于描述验证条件的简单语言，然后以此验证条件为准则，在运行时层次检测缺陷存在。在这项研究中，缺陷检测的实施离不开编程人员的参与，自动化程度不高，这也是定理证晓的不足之处。在ESC/Java 的基础上，静态检测器改进了自动化程度，结合了检测的精确性以及可扩展性可以在上千行规模的开源程序中找出了很多缺陷，并且误报率很低。
    从上述研究可以发现，定理证明虽然是一种强大的正确性证明方法，但定理证明的最大问题在于需要大量的人为辅助，自动化程度低。后来的研究中自动化程度的提高也以牺牲检测范围和检测精度为代价，可以片面理解为对己知缺陷模式进行形式化转换成验证条件，这种方法并不可取。同时，定理证明还需要用户具有经验和专业知识，比如要用户给出循环不变式等。另外，对于一个不算大的确定系统的证明可能会极长，而且产生的证明可能难以理解。定理证明的使用和推广还存在很大限制。
    (3)模型检测
    模型检测是近年来研究的热点。该技术是通过搜索待验证软件系统模型的有穷状态空间来检验系统的行为是否具备预期性质的一种有穷状态系统自动验证技术。
    在模型检测中，系统用有穷状态模型建模；其性质规约则通常是时序逻辑或模态逻辑公式，也可以用自动机语言描述；通过有效的搜索来检验有穷状态模型是否满足规约，如果不满足，给出使性质公式为假的系统行为轨迹。目前，模型检测方法在代码的形式化验证及缺陷检测方面都具有非常多的研究成果，这依赖于模型检测覆盖面广、自动化程度高的优势，但同时也可以发现模型检测的应用同样也存在多种问题，如针对大规模代码检测过程会产生状态约简问题、状态约筒后的检测精确度保持问题等，这些都需要结合代码检测的特点做进一步的研究。
    模型检测一开始是纯粹的静态分析方法，后续的研究中针对模型检测容易产生状态爆炸等问题，已经与程序动态切片、符号执行等结合起来，一方面利用了模型检测覆盖面广、自动化程度高等优势，另一方面又结合程序本身的特征进行了有效的状态约简，在缺陷监测方面取得了不错的成果。