Search

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 symbolic execution via type-unsafe pointer-guided Monte Carlo Tree Search (MCTS). 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 contain vulnerabilities. Vital drives a guided MCTS to prioritize paths in the symbolic execution tree that contain a larger number of unsafe pointers and to effectively navigate the exploration-exploitation trade-off. We built Vital on top of KLEE and compared it with existing search 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 37.50% 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 on automatically detecting known vulnerabilities without prior expert knowledge., Comment: 12 pages

Compiler bugs pose a significant threat to safety-critical applications, and promptly as well as effectively isolating these bugs is crucial for assuring the quality of compilers. However, the limited availability of debugging information on reported bugs complicates the compiler bug isolation task. Existing compiler bug isolation approaches convert the problem into a test program mutation problem, but they are still limited by ineffective mutation strategies or high human effort requirements. Drawing inspiration from the recent progress of pre-trained Large Language Models (LLMs), such as ChatGPT, in code generation, we propose a new approach named LLM4CBI to utilize LLMs to generate effective test programs for compiler bug isolation. However, using LLMs directly for test program mutation may not yield the desired results due to the challenges associated with formulating precise prompts and selecting specialized prompts. To overcome the challenges, three new components are designed in LLM4CBI. First, LLM4CBI utilizes a program complexity-guided prompt production component, which leverages data and control flow analysis to identify the most valuable variables and locations in programs for mutation. Second, LLM4CBI employs a memorized prompt selection component, which adopts reinforcement learning to select specialized prompts for mutating test programs continuously. Third, a test program validation component is proposed to select specialized feedback prompts to avoid repeating the same mistakes during the mutation process. Compared with state-of-the-art approaches over 120 real bugs from GCC and LLVM, our evaluation demonstrates the advantages of LLM4CBI: It can isolate 69.70%/21.74% and 24.44%/8.92% more bugs than DiWi and RecBi within Top-1/Top-5 ranked results. We also demonstrate that the LLMs component used in LLM4CBI can be easily replaced while still achieving reasonable results., Comment: Accepted by IEEE Transactions on Software Engineering