Revisiting the Combination of Static Analysis Error Traces and Dynamic Symbolic Execution: A Potential Approach for True Positive Confirmation (Registered Report)

Revisiting the Combination of Static Analysis Error Traces and Dynamic Symbolic Execution: A Potential Approach for True Positive Confirmation (Registered Report)

연구 분야: Verification

학회: ISSTA Companion '25: Proceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis

Static analysis is a well-established method for detecting program defects and ensuring software security. However, developers often refrain from utilizing static analysis tools in production environments due to the significant time wasted on eliminating false positives. Effective techniques are missing for confirming the reports from static analyzers. This paper replicates and extends the work of Busse et al., who designed and evaluated a technique to automate the process of confirming potential bugs reported by static analysis using dynamic symbolic execution (DSE) to eliminate false positives. Our replication reveals that traces generated by static analysis reports still hold value in guiding DSE to confirm bugs. After making minor improvement modifications, we found that the performance of the technique was significantly improved and further studied the effects of false positives and inaccurate information on the performance. We also extend the benchmarks for the task by leveraging Software Verification Benchmarks (SV-benchmarks) which contain non-trivial injected bugs and is compatible with both static analysis and DSE. Our goal is to demonstrate and understand the potential of combining static analysis and symbolic execution techniques for accelerating the confirmation of true positives and the elimination of false positives.