기술 요약: 정량적 심볼릭 패치 영향 분석

문제 제기

전통적인 동등성 검증은 프로그램을 동등하거나 비동등한 것으로 이분법적으로 분류합니다. 이러한 이분법적 분류는 취약점을 해결하기 위해 패치된 버전이 원래 (취약한) 코드와 비동등할 것으로 예상되는 패치 영향 분석에는 불충분합니다. 비동등성이 예상되지만, 핵심적인 과제는 프로그램이 어떤 조건 하에서 서로 다른지, 그리고 입력 도메인의 어떤 비율이 영향을 받는지 결정하는 데 있습니다.

현재의 접근 방식은 대부분의 입력에 대해 기능을 유지하면서 취약점을 수정하는 "좋은" 패치와, 입력을 과도하게 제한함으로써 (예: 안전한 값을 하드코딩하거나 모든 입력을 거부함으로써) 입력 도메인의 훨씬 더 큰 부분에 걸쳐 비동등성을 도입하는 "나쁜" 패치를 구분하는 데 실패하는 경우가 많습니다. 이러한 행동적 차이를 정량적으로 측정할 수 있는 기법이 부족합니다.

방법론

저자들은 입력 도메인 전반에 걸친 행동적 차이의 정도를 측정하여 비동등성을 세분화하는 정량적 부분 동등성 분석 (Quantitative Partial Equivalence Analysis) 프레임워크를 제안합니다. 이 방법론은 다음 세 가지 주요 구성 요소로 이루어집니다:

1. 부분 동등성의 형식화

이 논문은 프로그램 $P$를 입력 도메인 $D_{IP}$에서 출력 도메인 $D_{OP}$로의 전 함수 (total function) 로 정의합니다. 동일한 입력 도메인을 가진 두 프로그램 $P_1$(원본) 과 $P_2$(패치된 버전) 가 주어졌을 때:

• 동등 집합 ($D_{eq}$): $P_1(\vec{I}) = P_2(\vec{I})$인 입력들의 집합.
• 비동등 집합 ($D_{neq}$): $P_1(\vec{I}) \neq P_2(\vec{I})$인 입력들의 집합.
• 패치 영향 표면 (Patch Impact Surface): $D_{neq}$로 정의됨. 목표는 동등 조건 ($F_{eq}$) 과 $D_{eq}$가 성립하는 입력 도메인의 비율을 계산하는 것입니다.

2. 심볼릭 분석 및 요약

이 접근법은 확장된 심볼릭 실행을 활용하여 두 프로그램 모두에 대한 **심볼릭 요약 ($S_P$)**을 생성합니다. 심볼릭 요약은 모든 실행 경로에 대한 입력과 출력 간의 관계를 나타내는 논리 공식입니다.

• 알고리즘 1 (EqChecker): $S_1 \Leftrightarrow S_2$와 $S_1 \land S_2$의 만족 가능성을 확인함으로써 프로그램을 동등 ($T_{eq}$), 완전히 비동등 ($T_{neq}$), 또는 부분적으로 동등 ($P_{eq}$) 으로 분류합니다.

3. 정량적 기법 (범위 탐색 휴리스틱)

수치 도메인에서 $D_{eq}$와 $D_{neq}$의 크기를 효율적으로 정량화하기 위해, 저자들은 범위 기반 탐색 휴리스틱을 제안합니다. 이는 모든 입력을 열거하거나 대규모 도메인에 대해 비용이 많이 드는 모델 카운팅을 사용하는 계산적 비실용성을 피합니다.

• 관계적 범위 탐색 (알고리즘 2): 입력 도메인을 부분 도메인으로 재귀적으로 분할 (반복적으로 범위 반감) 하고, 이러한 부분 도메인 내에서 동등성 또는 완전한 비동등성을 확인합니다. 이는 여러 변수 간의 관계적 조건을 포착하지만 $O((2^N)^{LIMIT})$의 지수적 복잡성을 가집니다.
• 반복적 범위 탐색 (알고리즘 3): 확장성을 개선하기 위해 한 번에 하나의 입력 매개변수를 처리하여 복잡도를 $O(N \times 2^{LIMIT})$로 줄입니다. 그러나 변수 간의 관계적 제약 조건을 포착할 수는 없습니다.
• 반복적 우선순위 범위 탐색 (알고리즘 5): 프로그램이 절대값이 작은 값에 대해 더 동등할 가능성이 높다는 직관에 기반하여, 영 (zero) 을 중심으로 한 우선순위 (음수, 영, 양수 분할) 로 도메인을 분할합니다.
• 결합 범위 탐색 (알고리즘 6): 반복적 접근과 우선순위 접근을 통합하여 각 입력 매개변수에 대한 동등성의 최상위 하한을 선택함으로써 견고한 분석을 제공합니다.

4. 베이스라인 비교

저자들은 범위 탐색 접근 방식을 다음과 비교합니다:

• 열거적 모델 카운팅: SMT 솔버를 통해 만족하는 해를 반복적으로 찾는 방법.
• 투영 및 모델 카운팅: 양자 제거 및 모델 카운팅 도구 (SearchMC, Ganak, qCoral, ABC) 를 사용하여 동등성 비율을 계산하는 방법.

주요 기여

1. 형식화: 이 논문은 부분 동등성과 패치 영향 표면 개념을 형식화하여, 동등성/비동등성 조건과 해당 비율을 포함하도록 동등성 분석을 확장합니다.
2. 기법 개발: 수치 입력 도메인의 효율적인 정량적 분석을 위해 특별히 설계된 범위 기반 탐색 기법을 제안하며, 동등성에 대한 견고한 하한을 제공합니다.
3. 패치 영향 분석: 이 기법은 입력 도메인에 최소한의 영향을 미치는 패치 (좋은 패치) 와 입력을 과도하게 제한하는 패치 (나쁜 패치) 를 구분하여 패치 영향을 평가하는 데 적용됩니다.
4. 벤치마크 평가: 이 접근 방식은 다음에서 평가되었습니다:
   • PatchBench: Linux, Qemu, FFmpeg 의 90 개 CVE 패치.
   • JulietBench: 좋은 패치와 나쁜 패치 (LLM 생성 나쁜 패치 포함) 가 포함된 50 개 프로그램.
   • EqBench: 47 개 C 프로그램으로, 이 도구는 정수 오버플로우로 인해 "동등"으로 잘못 레이블링된 5 건을 식별했습니다.

실험 결과

• 패치 구분: JulietBench 데이터셋에서 나쁜 패치는 평균 패치 영향 표면이 **96.65%**였으며, 반면 좋은 패치는 입력 도메인의 **29.03%**만 영향을 받았습니다.
• 실제 환경 변동성: PatchBench 에서 36.25% 의 패치는 입력 도메인의 90% 이상에서 비동등했으며, 20% 는 10% 미만에 영향을 미쳤습니다. 이는 실제 환경의 패치 영향에 상당한 변동성이 있음을 보여줍니다.
• 정확도 및 효율성:
  • 결합 범위 탐색 접근 방식은 알려진 기준truth (ground truth) 를 가진 정확한 동등성 결과를 산출하는 데 PatchBench 에서 81.8%, EqBench 에서 **95.2%**의 정확도를 달성하여, 다음으로 좋은 방법보다 30.7% 더 높은 성능을 보였습니다.
  • 이는 모델 카운팅 접근 방식보다 기준truth 에 더 가까운 근사치를 제공했으며, 평균 편차가 두 번째로 좋은 접근 방식보다 약 29.4% 낮았습니다.
  • 실행 시간: RangeSearch 는 PatchBench 에서 SearchMC 보다 약 8 배, EqBench 에서 2 배 빠르게 실행되었습니다.
• EqBench 발견 사항: 분석은 EqBench 에서 동등으로 잘못 레이블링된 5 건을 식별했으며, 도구는 정수 오버플로우 조건으로 인해 이를 부분적으로 동등한 것으로 올바르게 식별했습니다.

중요성 및 주장

이 논문은 정량적 부분 동등성 분석이 패치 영향을 효과적으로 특징짓고 정량화하여 이분법적 동등성 검증보다 더 세련된 통찰력을 제공한다고 주장합니다.

• 보안적 함의: 이는 (예: 입력 도메인의 큰 부분을 영향을 미치는 패치 등) 추가 검토가 필요한 패치를 식별하는 데 도움이 되며, 기능을 유지하는 안전한 패치와 입력을 과도하게 제한하여 기존 가정이나 CI/CD 파이프라인을 파괴하는 패치를 구분합니다.
• 방법론적 기여: 이 작업은 패치 영향 분석의 맥락에서 기존 심볼릭 실행 및 모델 카운팅 기법의 한계를 해결하는 확장성과 정밀도의 균형을 맞춘 새로운 범위 탐색 휴리스틱을 도입합니다.
• 한계: 저자들은 이 접근 방식이 차분 심볼릭 실행에 의존하며, 심볼릭 요약을 생성할 수 없는 경우 분석이 진행될 수 없다고 인정합니다. 또한 현재 범위 탐색 휴리스틱은 수치 도메인에 초점을 맞추고 있지만, 저자들은 문자열과 같은 다른 도메인으로의 확장 가능성을 언급합니다.

저자들은 모든 패치 분석 문제를 해결한다고 주장하지는 않지만, 그들의 정량적 접근 방식이 소프트웨어 패치의 행동적 결과를 이해하기 위한 필요한 세분화 계층을 제공한다고 주장합니다.