Quantitative Symbolic Patch Impact Analysis

TL;DR

This paper introduces a method for quantifying behavioral differences between original and patched programs using symbolic analysis, providing detailed impact assessment beyond simple equivalence classification.

Contribution

It presents a novel quantitative partial equivalence analysis approach that measures behavioral divergence, improving patch impact analysis with a range-based heuristic for numerical domains.

Findings

Effectively characterizes and quantifies patch impact on 90 CVE patches.

Identifies five C program pairs mislabeled as equivalent in benchmarks.

Provides input conditions where program behaviors diverge.

Abstract

Traditional equivalence checking classifies programs as equivalent or non-equivalent, providing insufficient information for tasks like patch impact analysis where it is expected the patched version of the program to be non-equivalent to the original program. When two program versions are non-equivalent, determining under what conditions they differ and what percentage of inputs are affected remains an open challenge. In this work, we introduce quantitative partial equivalence analysis, an approach for assessing software patches by quantifying behavioral differences between the original (vulnerable) code and the patched code. Using symbolic analysis, we identify input conditions under which patched and original programs exhibit identical or divergent behaviors. Our approach refines non-equivalence by measuring the extent of behavioral divergence across the input domain. For efficient quantitative analysis of numerical domains, we propose a range-based search heuristic that provides a sound lower bound on equivalence. We demonstrate our approach on 90 CVE patches from widely used open-source projects (Linux, Qemu, FFmpeg), as well as on a Juliet Test Suite-based dataset containing programs with CWEs. Our results show that quantitative partial equivalence analysis effectively characterizes and quantifies patch impact. Additionally, experiments on the EqBench benchmark reveal five C program pairs that are mislabeled as equivalent, and we identify the input conditions under which their behaviors diverge.