Vital: 通过类型不安全指针引导的蒙特卡洛树搜索进行面向漏洞的符号执行
Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search
AI总结：
Vital通过类型不安全指针引导的蒙特卡洛树搜索，提高符号执行中漏洞检测效率和覆盖率。
摘要：
在导航符号执行树时，如何高效地发现内存安全漏洞？现有解决方案要么采用路径搜索启发式方法以最大化覆盖率，要么采用截断符号执行来跳过不感兴趣的代码（即手动标记为与漏洞无关）。然而，大多数现有搜索启发式方法并非面向漏洞，手动标记无关代码依赖于先验专家知识，这使得在实践中难以有效检测漏洞。本文提出了Vital，一种新的面向漏洞的路径探索方法，具有两个创新点。首先，提出一个新的指标（即类型不安全指针）来近似漏洞路径。一个类型不安全的指针无法在没有内存损坏的情况下被静态证明安全地解引用。我们的核心假设是，具有更多类型不安全指针的路径更可能具有漏洞。其次，实现了一种新的类型不安全指针引导的蒙特卡洛树搜索算法，以引导路径探索朝含有更多不安全指针的区域，旨在增加检测漏洞的可能性。我们基于KLEE构建了Vital，并将其与现有路径搜索策略和截断符号执行进行了比较。在前者中，结果表明，Vital可以覆盖多达90.03%更多的不安全指针，并检测多达57.14%更多的唯一内存错误。在后者中，结果表明，Vital可以实现高达30倍的执行时间加速和高达20倍的内存消耗减少，以自动检测已知漏洞而无需先验专家知识。在实践中，Vital还检测到一个此前未知的漏洞（已分配新的CVE ID），该漏洞已由开发者修复。
英文摘要：
How to find memory safety bugs efficiently when navigating a symbolic execution tree that suffers from path explosion? Existing solutions either adopt path search heuristics to maximize coverage rate or chopped symbolic execution to skip uninteresting code (i.e., manually labeled as vulnerability-unrelated) during path exploration. However, most existing search heuristics are not vulnerability-oriented, and manual labeling of irrelevant code-to-be-skipped relies heavily on prior expert knowledge, making it hard to detect vulnerabilities effectively in practice. This paper proposes Vital, a new vulnerability-oriented path exploration for symbolic execution with two innovations. First, a new indicator (i.e., type-unsafe pointers) is suggested to approximate vulnerable paths. A pointer that is type-unsafe cannot be statically proven to be safely dereferenced without memory corruption. Our key hypothesis is that a path with more type-unsafe pointers is more likely to be vulnerable. Second, a new type-unsafe pointer-guided Monte Carlo Tree Search algorithm is implemented to guide the path exploration towards the areas that contain more unsafe pointers, aiming to increase the likelihood of detecting vulnerabilities. We built Vital on top of KLEE and compared it with existing path searching strategies and chopped symbolic execution. In the former, the results demonstrate that Vital could cover up to 90.03% more unsafe pointers and detect up to 57.14% more unique memory errors. In the latter, the results show that Vital could achieve a speedup of up to 30x execution time and a reduction of up to 20x memory consumption to detect known vulnerabilities without prior expert knowledge automatically. In practice, Vital also detected one previously unknown vulnerability (a new CVE ID is assigned), which has been fixed by developers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
