정량적 심볼릭 패치 영향 분석

전통적인 동치성 검사 (Equivalence checking)는 프로그램을 동치 또는 비동치로 분류하며, 패치된 버전의 프로그램이 원본 프로그램과 비동치일 것으로 예상되는 패치 영향 분석 (Patch impact analysis)과 같은 작업에는 불충분한 정보를 제공합니다. 두 프로그램 버전이 비동치일 때, 어떤 조건에서 차이가 발생하는지, 그리고 입력값의 몇 퍼센트가 영향을 받는지 결정하는 것은 여전히 해결되지 않은 과제로 남아 있습니다. 본 연구에서는 원본 (취약한) 코드와 패치된 코드 사이의 행동적 차이를 정량화하여 소프트웨어 패치를 평가하는 접근 방식인 정량적 부분 동치 분석 (Quantitative partial equivalence analysis)을 소개합니다. 우리는 심볼릭 분석 (Symbolic analysis)을 사용하여 패치된 프로그램과 원본 프로그램이 동일하거나 상이한 행동을 보이는 입력 조건을 식별합니다. 우리의 접근 방식은 입력 도메인 전반에 걸친 행동적 발산 (Behavioral divergence)의 정도를 측정함으로써 비동치성을 정교화합니다. 수치 도메인 (Numerical domains)에 대한 효율적인 정량적 분석을 위해, 우리는 동치성에 대한 건전한 하한선 (Sound lower bound)을 제공하는 범위 기반 탐색 휴리스틱 (Range-based search heuristic)을 제안합니다. 우리는 널리 사용되는 오픈 소스 프로젝트 (Linux, Qemu, FFmpeg)의 90개 CVE 패치뿐만 아니라, CWE를 포함하는 프로그램이 담긴 Juliet Test Suite 기반 데이터셋을 통해 우리의 접근 방식을 입증합니다. 연구 결과, 정량적 부분 동치 분석이 패치 영향을 효과적으로 특징짓고 정량화함을 보여줍니다. 또한, EqBench 벤치마크에 대한 실험을 통해 동치로 잘못 라벨링된 5개의 C 프로그램 쌍을 발견하였으며, 이들의 행동이 갈라지는 입력 조건을 식별하였습니다.