Patch presence test is critical in software security to ensure that binary files have been patched for known vulnerabilities. It is challenging due to the semantic gap between the source code and the binary, and the small and subtle nature of patches. In this paper, we propose REACT, the first patch presence test approach on IR-level. Based on the IR code compiled from the source code and the IR code lifted from the binary, we first extract four types of feature (return value, condition, function call, and memory store) by executing the program symbolically. Then, we refine the features of the source code and rank them. Finally, we match them with the features of the target to determine the presence of a patch with an SMT solver to check the equivalence of features at the semantic level.

To evaluate our approach, we compare it with state-of-the-art approaches, BinXray and PS3, on a dataset containing binaries compiled from different compilers and optimization levels. Our experimental results show that REACT achieves scores of 0.88, 0.98, and 0.93, in terms of precision, recall, and F1 score, respectively. REACT outperforms the baselines by 39% and 12% in terms of the F1 score, while the pure testing speed of our approach is 2x faster than BinXray and 100x faster than PS3. Furthermore, we conduct an ablation study to evaluate the effectiveness of each component in REACT, which shows that SMT solver and refinement can contribute to 16% and 10% improvement in terms of the F1 score, respectively.