Patch Space Exploration using Static Analysis Feedback

TL;DR

This paper introduces a static analysis-guided approach for automatic memory safety repair that avoids test overfitting by classifying patches based on their effect on symbolic heaps, enabling scalable and effective patch synthesis.

Contribution

It presents a novel method that leverages Incorrectness Separation Logic feedback to guide patch generation and groups patches by effect to improve scalability in automatic repair.

Findings

Successfully repaired real-world memory errors in OpenSSL and Swoole.

Demonstrated scalability and high quality of generated patches.

Outperformed test-based repair approaches in avoiding overfitting.

Abstract

Automated Program Repair (APR) techniques typically rely on a given test-suite to guide the repair process. Apart from the need to provide test oracles, this makes the produced patches prone to test data over-fitting. In this work, instead of relying on test cases, we show how to automatically repair memory safety issues, by leveraging static analysis (specifically Incorrectness Separation Logic) to guide repair. Our proposed approach learns what a desirable patch is by inspecting how close a patch is to fixing the bug based on the feedback from incorrectness separation logic based static analysis (specifically the Pulse analyser), and turning this information into a distribution of probabilities over context free grammars. Furthermore, instead of focusing on heuristics for reducing the search space of patches, we make repair scalable by creating classes of equivalent patches according to the effect they have on the symbolic heap, and then invoking the validation oracle only once per class of patch equivalence. This allows us to efficiently discover repairs even in the presence of a large pool of patch candidates offered by our generic patch synthesis mechanism. Experimental evaluation of our approach was conducted by repairing real world memory errors in OpenSSL, swoole and other subjects. The evaluation results show the scalability and efficacy of our approach in automatically producing high quality patches.