用于软件安全漏洞的静态检测技术

第34卷第12期ComputerEngineering 2008年6月安全技术文章编号: 1000-3428（2008）12-0157-03文档标识码: CLC编号: TP309用于软件安全漏洞的静态检测技术南京大学新计算机软件状态密钥技术实验室，南京210093； 2.南京大学计算机科学与技术系，南京210093）重要提示: 软件安全漏洞越来越严重. 静态漏洞检测提供了一种在软件结构和代码中查找漏洞的方法. 本文研究软件漏洞静态检测的两个主要方面: 静态分析和程序验证，重点在于词法分析，规则检查，类型推导，模型检测，定理证明和符号执行方法的分析. 常用的静电检测工具按方法分类，讨论并总结了静电检测技术的优点，适用性和发展趋势. 关键字: 软件安全漏洞；静态分析；程序验证静态检测技术软件安全漏洞张琳1,2曾庆凯1,2南京大学NovelSoftware技术国家重点实验室南京210093;南京大学计算机科学系，南京210093）[摘要]本文总结了成本分析软件证券化缺陷的统计分析程序验证方法. 还综合评估了几种静态检测方法: 词法分析，规则检查，类型理论推导，模型检查，改进算法，符号执行. 【关键词】软件缺陷；安全性；安全性；安全性逻辑分析程序验证概述漏洞是指在软件设计和实施过程中引入的缺陷，例如数据访问或行为逻辑，攻击者可能会使用这些缺陷来使程序行为违反某些安全策略. 根据在检测过程中是否需要执行程序的标准，软件安全漏洞检测技术分为: （1）动态测试在程序运行过程中注入测试数据，观察程序是否正常运行，是否正常运行. 输出符合程序意图以发现程序漏洞的目的.

动态测试仅关注程序的外部性能，因此其定位不准确且漏报率很高. （2）静态检测注意程序代码，并从程序代码的内部结构和特征中检测漏洞，以适当地弥补此缺陷. 静态检测技术从早期的词法分析开始，出现了许多方法. 早期的静态检测主要是指静态分析. 随着形式验证方法的引入，静态检测的概念已扩展为: 1）静态分析扫描被测程序的源代码，从语法和语义的角度了解程序行为，并直接分析Measure程序特征和寻找可能导致错误的异常. 2）程序验证通过形式化的程序代码抽象，采用形式验证技术来证明程序是否符合特定的安全规则，从而确定程序是否具有安全漏洞. 本文总结了当前常用的检测技术和方法，对可以通过静态检测检测到的漏洞的类型进行了分类，描述和比较了各种技术，并期待着静态检测技术的发展前景. 检测漏洞的分类静态检测关注程序的内部特征，其技术特征与检测到的漏洞的特征密切相关. 因此，本节首先讨论静态检测到的漏洞的类型. 有许多方法可以对软件漏洞进行分类. 根据现有的分类方法，漏洞的区分更加细致. 大多数现有的静态检测技术所涵盖的漏洞类型是分散的，很难在漏洞类型中找到它们的共性. 为了便于比较，本文将这些漏洞分为以下几类: （1）与内存安全性相关的漏洞，着重研究数据流中的错误，这些错误通常是由于某些错误的内存存储状态或使用情况引起的.

（2）与内存相关的安全漏洞涉及数据和类型的正确性. 因此，检测此类漏洞的关键在于存储空间的建模. 与安全相关的顺序性漏洞集中于控制流中的错误，这些错误通常是由某些与安全相关的操作之间的错误执行顺序引起的. 与时间相关的安全漏洞涉及程序行为的时间关系. 因此，只能检测具有偏序特性的方法. 按照此划分，由于静态检测方法的技术特性不同以及对漏洞的理解不同，因此某些方法只能检测一种类型的漏洞，而某些方法可以检测两种类型的漏洞. 基金项目: 国家自然科学基金资助项目（60473053）；国家“ 863”基金资助项目（2006AA01Z432）；江苏省自然科学基金资助项目（BK2005074）作者简介: 张琳（1983-），男，硕，主要研究方向: 信息安全曾庆凯教授收稿日期: 2007-08-28电子邮件: nju_Ares @ hot mail.com静态检测技术始于早期的缓冲区溢出检测，近十年来出现了多种检测技术，以下是静态子程序介绍了分析和程序摘要验证. 3.1静态分析静态分析方法直接扫描程序代码，提取程序的关键语法系统漏洞检测程序，解释其语义，了解程序行为，并根据预设的漏洞特征和安全规则检测漏洞.

（1）词法分析词法分析是最早的静态分析技术，仅执行语法检查. 词法分析将程序划分为多个部分，然后将每个部分与“可疑”进行比较. 如果属于怀疑，则进一步执行启发式判断. 词法分析可以检测到较少的漏洞，通常只能检测到已知的固定漏洞，而且漏报率很高. （2）规则检查可以通过安全规则来描述程序本身的安全性. 程序本身中有一些编程规则，即一些常规安全规则，也称为漏洞模式. 例如，程序应避免在root用户权限下执行exec调用. 规则检查方法以特定的语法描述这些规则，规则处理器将其接收并转换为分析器可以接受的内部表示形式，然后对程序行为进行比较和检测. （3）类型推导自动推断程序中变量和函数的类型，以判断变量和函数的访问是否符合类型规则. 静态漏洞检测的类型派生由构造型断言，派生规则和检查规则组成. 刻板印象断言定义变量的初始类型. 推导规则为推理系统提供了一组规则. 检查规则用于确定推断结果是否为“良好行为”. 基于类型推导的静态分析方法适用于控制流独立分析. 但是系统漏洞检测程序，对于与控制流有关的特性，需要引入类型限定符和子类的概念来扩展源语言的类型系统，以便新的类型系统扩展源语言的数据类型并表达两者之间的关系. 类型.

类型限定符将变量类型表示的值集划分为几个不相交的子类型），表示不同级别的安全性. 可以随时测试子类型变量（2）定理证明定理证明比模型检查的正式方法更严格，并且使用各种判断过程来验证程序的抽象公式是否正确. 判别方法取决于公式的形式，例如不等式的合取: 首先，由该合取构成一个图，该合取中的每个条件对应于图中的一个节点，然后使用相应的方程式比较相应的顶点合并. 在顶点合并过程中，检查连接中的不等式. 如果发现存在不令人满意，则不能满足连接. （3）符号执行符号执行的基本思想是将程序中变量的值逻辑转换为抽象符号，模拟对路径敏感的程序控制流，并通过该方法检测是否存在错误的可能性约束解决. 从条件程序中程序执行之前的某个程序点，可以得出约束条件c1 c2？cn，因此Pc1c2是程序结束后要满足的条件. 为了解决无命题的规定，如果存在一组满足条件的解决方案，则在此程序点处存在一组变量状态，这将导致程序运行的结果不一致. 约束条件的集合和符号执行解决方案工具的解决能力决定了其发现错误的能力. 从理论上讲，许多约束问题都无法在可接受的时间内解决，因此，符号执行方法仅适用于解决某些问题.

在[6]中提出的缓冲区模型实际上将符号模型限制为缓冲区数据，对程序进行仿真并尝试解决每一步的约束（缓冲区访问长度小于缓冲区长度），并且其效率为在验收时间内. 3.3检测方法的比较大多数静态检测方法通常不会单独使用，并且当前使用的许多检测工具经常同时使用多种检测方法. 例如，通常被称为“数据流分析”工具实际上是类型派生和规则检查这两种技术的常见应用，并伴随着符号执行的某些功能. 该表比较了适用于主要静态检测方法的漏洞类型，优缺点. 程序分析和检测检测漏洞优点缺点方法替换父类型变量，反之亦然. 通过使用类型限制关系，可以检测到超出权限的访问错误. 3.2词汇记忆的验证，程序验证的高效率，不准确的分析和分析，漏洞覆盖的漏洞覆盖率有限，程序验证方法通过抽象程序获取正式程序或模型，然后使用正式验证技术来验证和验证正确性. 检测与内存相关的大多数类型的漏洞；推导少量时序相关规则内存相关，时序相关可以处理大型程序，高效可以根据不同规则分析不同的系统，引入安全属性需要重新定义类型，这受到规则描述的限制机制它可以分析特定类型的漏洞. （1）模型检测模型检测状态机或有限状态程序的有向图等抽象模型，然后遍历模型以验证系统特性.

通常有多种验证方法: 有效的程序检测，较差的可伸缩性，程序验证检测，漏洞检测，优点，缺点，方法和符号方法. 将抽象模型中的状态转换为由语法树描述的逻辑公式，然后确定该公式是否令人满意. 将模型转换为自动机，将需要检查的安全定时属性转换为等效的自动机，然后对这两个自动机进行补充以形成新的自动机，并且确定问题可以接受以检查新的自动机. 语言模型检测需要枚举所有可能的状态，因为软件本身非常复杂，因此大多数时序模型都是相关的；少量的内部检测存储器相关定理，存储器相关性，证明与时序相关的符号存储器相关的执行可以严格检测程序时序漏洞. 漏洞放大是通过严格的系统检测，低误报率和准确的线路进行的. 它可以发现程序中的微妙之处可能导致状态空间爆炸. 它缺乏在某些领域进行公式推理的适用性，对于新漏洞，程序执行的可能性也不高. 路径随着程序规模的增加而增加. 对所有程序点进行建模可能会使模型规模巨大，因此通常只为程序的某个方面构建抽象模型. 最近出现的模型检测方法使得能够通过对存储器状态进行建模来检测与存储器相关的漏洞，使得最初用于检测与时序相关的漏洞的模型检测方法可以检测与存储器相关的漏洞. —158—逻辑错误呈指数增长. 程序验证比程序分析更为严格，但其运营成本也更高.

在程序的全局检测中，程序验证的效果更加突出，在程序的局部性检测中，程序分析更加有效. 在程序分析中，词法分析集中在程序的表面特征上，这太简单了. 类型派生和规则检查需要人工协助来定义类型和规则，这在可伸缩性和自动化性方面较差，并且可以检测到漏洞，但是检测效率更高. 在程序验证方面，模型检查的实用性已在实践中得到证明，但其计时特性决定了其漏洞类型的局限性. 定理证明用户需要具有良好的理论素质和较强的素养，并且尚未得到广泛的应用. 效率也有待提高；符号执行将程序验证的严格证明与程序分析的模拟扫描相结合，但是它也具有验证复杂和效率低的缺点. 静态检测只能检测已知类型的漏洞. 由于缺乏通用的漏洞描述机制，因此: （1）无法使用已知漏洞特征以标准化方式描述未知漏洞. （2）对于已知漏洞，当前很难拥有可以完全覆盖的检测技术. 静态检测的另一个缺点是性能不足. 静态检查的准确性与运行时间和空间消耗成正比. 因此，提高检查质量将增加运营成本. 通过静态检测技术测得的假率（假阴性率）； （2）误检率高（误判率始于2000年，大量的静态检测工具应运而生.

在此之前，有Li nt（1978），ES C（1995）和LCl nt（1994），它们为后来的大多数工具奠定了基础，但它们并没有太多实际用途. 值. （1）Li nt提供了原始的规则检查思想； （2）LCl int有所改进，但用户需要手动添加注释以描述意图； （3）ES提供了抽象数据流符号执行的早期想法. 在2000年，出现了词法分析工具ITS，符号执行工具BOON REfix和简单的模型检查工具Bandera. 此时的符号执行仅仅是数据的简单抽象，而模型检测Bandera只是为ava语言建立简单的有限状态模型. 从2001年到2002年，静态测试工具发展迅速. 词法分析可产生更准确的RATS分析，符号执行中更完整的抽象Mjolnir，模型检测中的经典工具（例如MOPS SLAM）和规则检查中的自动化MC Splint. 同时，也出现了定理证明工具Eau Claire和几种推导工具CQual，Cured，ES. 两年来，静态检测的主要技术已经成形. （1）2003年，BLAST RacerX出现了. BLAST已针对模型检测进行了优化，而RacerX为检测种族条件漏洞提供了一种更好的方法.

（2）Check’n’Crash于2005年出现，再次推动了符号执行技术的发展. （3）定理证明工具Cogent于2005年问世. 根据技术分类，对常用的静电检测工具进行了分类，其对应关系示于表中. 静态检测工具使用技术静态检测技术主要静态检测工具词法分析ts类型推导CCu规则检查MC，LCL int Lint，plint模型检测Band BLAST，SLAM定理证明Cog en auCl符号执行Mjolni OON，STLl修复了静态检测技术当前的发展趋势是结合各种静态检测技术来提高性能. 有几种方法可以组合使用这些方法: 提供一个框架，以使用不同的检测技术来测试程序，并在获得大量测试结果后进行分析. 从误报率来看，利用多种技术的检测结果相交做出脆弱性判断决策可以降低误报率；从误报率来看，对于同一漏洞，多种检测技术的结合结果可以降低误报率. （2）直接与检测技术相结合，可以通过技术的组合获得新的方法，例如在符号执行过程中增加类型推导技术，在变量仿真执行过程中增加其类型特征的推导. 高漏洞检测率. 除了多种静态检测技术的组合之外，还出现了动态与静态检测方法的组合.

The

p c-Dynami方法首先使用静态方法分析程序，以获取程序的内部特征，从而筛选测试数据集以指导下一轮动态测试. 在DS回合进行静态测试之前执行动态测试，以消除一些无法达到的输入条件并简化静态检测的复杂性. 结论静态检测技术试图理解该程序. 从检测技术本身来看，它具有一定的优势，但是由于软件本身的复杂性，也会增加其检测过程的复杂性. 检测精度的提高通常伴随着空间和时间消耗的增加. 尽管已经出现了大量工具，但是静态检测仍处于起步阶段，但是它还不够实用，需要进行更深入的研究. 鉴于静态检测的优势和功能，该领域在未来仍值得探索. 参考软件缺陷分类法: 瞄准工具ACMSoftware工程SecureSyst ems-建立值得信赖的应用程序. 美国密苏里州路易斯: 正式模型计算机安全ACM计算调查，1981，13（3）: 247-278. 夏一鸣关键词: 安全漏洞检测，离子分析计算机科学，2006，33（10）: 279-283. 福斯特类型限定词[J]. ACM SIGPLAN ices，1999，34（5）: 192-203. 程序验证[J]. 美国材料学会，2000，47（5）: 534-545. 首先针对自动检测到的BufferOverrun漏洞[C] // Proc. 网络分布式系统安全专题讨论会. 美国圣地亚哥: 2000. —159 —

本文来自电脑杂谈，转载请注明本文网址：
https://www.pc-fly.com/a/jisuanjixue/article-243795-1.html