Vital：基于漏洞的符号执行技术——通过类型不安全的指针引导的蒙特卡洛树搜索实现

《ACM Transactions on Software Engineering and Methodology》：Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search

如何有效检测符号执行树中的内存安全漏洞？本文提出Vital方法，通过引入type-unsafe指针指标优化路径探索，结合改进的MCTS算法提升漏洞检测效率。实验表明该方法可覆盖90.03%更多不安全指针，检测57.14%额外内存错误，速度提升30倍且无需专家标注，并发现1个新CVE漏洞。

　　

摘要 总结

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多 登录

摘要

摘要

在处理存在路径爆炸问题的符号执行树时，我们如何有效地发现新的内存安全漏洞？现有的解决方案要么采用路径搜索启发式方法来最大化覆盖率，要么通过截断符号执行来跳过不感兴趣的代码（即手动标记为与漏洞无关的代码）。然而，大多数现有的搜索启发式方法并不针对漏洞，而手动标记需要跳过的无关代码在很大程度上依赖于专家的先验知识，这使得在实际中难以有效检测漏洞。

本文提出了一种新的、以漏洞为导向的符号执行路径探索方法 Vital，该方法包含两项创新。首先，我们提出了一种新的指标（即 类型不安全 指针）来近似表示潜在的漏洞路径。一个被标记为 类型不安全 的指针无法被静态证明可以安全地解引用而不会导致内存损坏。我们的核心假设是，包含更多 类型不安全 指针的路径更有可能存在漏洞。其次，我们实现了一种新的 类型不安全 指针引导的蒙特卡洛树搜索算法，以引导路径探索到包含更多 不安全 指针的区域，从而提高检测漏洞的可能性。我们在 KLEE 的基础上构建了 Vital，并将其与现有的路径搜索策略和截断符号执行方法进行了比较。实验结果表明，Vital 能够多检测到 90.03% 的不安全指针，并多发现 57.14% 的独特内存错误。在截断符号执行方法中，Vital 的执行速度提高了 30 倍，内存消耗减少了 20 倍，且无需专家的先验知识即可自动检测已知漏洞。在实际应用中，Vital 还发现了一个之前未知的漏洞（已分配新的 CVE 编号），该漏洞已被开发者修复。

总结

要查看此由人工智能生成的简单语言摘要，您必须具有高级访问权限。