SymRadar: PoC-Centered Bounded Verification for Vulnerability Repair

In this paper, we tackle the problem of patch verification. While automated vulnerability repair (AVR) techniques are gaining traction, it is not sufficient to merely generate patches; providing evidence of their correctness is also essential. However, the current state-of-the-art patch verification methods are not sufficiently effective. To address this issue, we present SymRadar, a patch verification tool based on under-constrained symbolic execution (UC-SE). What distinguishes SymRadar from existing patch verification techniques is its use of function-level symbolic execution with inputs centered around the provided proof-of-concept (PoC) input. As demonstrated in our evaluation, this PoC-centered symbolic execution is effective, achieving the highest recall (100%) and specificity (78%) among all compared techniques.