기술 요약: 소프트웨어 보안 테스팅을 위한 경로 타당성 분석용 지향적 심볼릭 실행 (Directed Symbolic Execution)

문제 정의

정적 분석은 실행 없이 코드를 분석하여 소프트웨어 취약점을 식별하는 확장 가능한 기법이다. 그러나 정적 분석기의 주요 한계점은 허위 보고(false-positive)를 생성한다는 것이다. 이러한 보고는 대개 실행 불가능한 제어 흐름 경로(infeasible control flow paths)의 분석에서 비롯된다. 이는 인터프로시저 제어 흐름 그래프(ICFG) 상에서는 유효해 보이지만, 의미론적 제약 조건으로 인해 런타임 시에는 실행될 수 없는 기본 블록(basic blocks)의 시퀀스를 의미한다.

심볼릭 실행은 경로 제약 조건을 구축하고 해결함으로써 이러한 경로의 타당성을 이론적으로 결정할 수 있지만, 실제 적용에는 "경로 폭발(path explosion)" 문제로 인해 어려움을 겪는다. 표준 심볼릭 실행은 도달 가능한 모든 경로를 탐색하려고 시도하므로 지수적인 자원 소비를 초래한다. 또한, 기존 도구들은 수동 개입이나 특정 인스트루멘테이션 없이 미초기화 메모리, 외부 함수 호출, 심볼릭 포인터, 루프와 같은 실제 세계의 복잡성을 처리하는 데 필요한 자동화 기능이 부족한 경우가 많다.

방법론

저자들은 사전에 정의된 ICFG 경로 세트의 타당성을 검증하기 위해 특별히 설계된 지향적 심볼릭 실행(Directed Symbolic Execution) 방법을 제안한다. 전체 상태 공간을 탐색하는 전통적인 심볼릭 실행과 달리, 이 접근 방식은 검증 목표를 향해 실행을 엄격하게 유도하며, 목표와 무관한 분기를 가지치기(pruning)한다.

핵심 알고리즘

알고리즘은 허용된 기본 블록의 집합($S_{allowed}$)과 타겟 블록($B_{target}$)에 도달하기 위해 반드시 통과해야 하는 필수 마일스톤의 집합($S_{req}$)을 기반으로 작동한다.

1. 지향적 가지치기 (Directed Pruning): 모든 분기점에서 엔진은 후속 블록이 $S_{allowed}$에 속하는 경우에만 해당 블록을 탐색한다. 이를 통해 무관한 프로그램 영역의 탐색을 제거한다.
2. 루프 바운딩 (Loop Bounding): 루프에서의 비종료를 방지하기 위해, 본 방법은 루프 반복 횟수($C_{max}$)를 제한한다. 루프가 이 제한을 초과하면, 엔진은 가용한 탈출 엣지(exit edges)를 통해 루프를 강제로 종료시키며, 루프 실행 중에 기록된 메모리 위치만을 심볼릭화한다. 이를 통해 분석이 루프에서 멈추지 않고 루프 이후의 코드로 계속 진행될 수 있도록 한다.
3. 검증 (Verification): 경로가 $S_{allowed}$ 내에 머물면서 $S_{req}$의 모든 블록을 방문한 상태로 $B_{target}$에 도달하면 해당 경로는 타당한 것으로 간주된다.

자동 심볼릭화 전략 (Automatic Symbolization Strategies)

수동 설정 없이 완전 자동화된 분석을 가능하게 하기 위해, 본 논문은 다음과 같은 심볼릭화 접근 방식을 도입한다.

• 진입점 파라미터 (Entry-Point Parameters): 경로 분석이 시작되는 함수의 모든 파라미터는 해당 함수가 프로그램의 main 진입점이 아니더라도 심볼릭화된다.
• 미초기화 메모리 (Uninitialized Memory): 미초기화된 지역 변수와 동적 할당된 메모리 영역은 제약이 없는 값을 가진 심볼릭 객체로 취급되어, 정의되지 않은 동작(undefined behavior)에 의존하는 경로가 조기에 폐기되지 않도록 보장한다.
• 외부 함수 (External Functions):
  • 반환 값: 외부 함수(예: 동적 라이브러리)의 반환 값은 심볼릭화된다.
  • 포인터 인자: 외부 호출의 비상수(non-constant) 포인터 인자가 참조하는 메모리 영역은 잠재적 부수 효과를 고려하여 재심볼릭화된다.
  • 특수 전역 변수: errno(외부 호출 후 재심볼릭화) 및 environ(environ 조작 함수에서의 비종료를 피하기 위해 고정된 길이를 가진 고정된 심볼릭 변수 집합으로 모델링)에 대한 특수 처리가 적용된다.
• 함수 포인터 및 가상 함수: 시스템은 시그니처 매칭을 통해 심볼릭 함수 포인터를 해결하며, 가상 함수의 경우 가상 테이블을 분석하여 가능한 모든 파생 클래스의 오버라이드(override)를 식별하고 각 후보에 대해 상태를 포크(fork)한다.

메모리 모델

본 논문은 크기가 알려지지 않은 심볼릭 포인터(예: 함수로 전달된 배열)를 위한 유연한 메모리 모델을 제안한다. 고정 크기 배열을 할당하는 대신, 이 모델은 첫 번째 역참조(dereference) 시점에 메모리 객체를 **온디맨드(on-demand)**로 생성한다.

• 온디맨드 할당 (On-Demand Allocation): 심볼릭 포인터가 액세스될 때만 메모리 객체가 생성된다.
• 에일리어싱 해결 (Aliasing Resolution): 포인터가 역참조될 때, 엔진은 동일한 오프셋을 가진 기존 메모리 객체가 있는지 확인한다. 에일리어싱이 가능할 경우, 엔진은 포인터가 기존 객체를 참조하는 시나리오와 새로운 별개의 메모리 위치를 참조하는 시나리오를 모두 탐색하기 위해 심볼릭 상태를 포크한다. 이는 사전 정의된 크기 제약 없이 연결 리스트(linked list)나 트리와 같은 복잡한 데이터 구조의 분석을 지원한다.

주요 기여

1. 지향적 심볼릭 실행 알고리즘: 정의된 범위 내로 탐색을 제한함으로써 특정 ICFG 경로의 타당성을 결정하는 방법론.
2. 완전 자동화된 심볼릭화: 진입점 파라미터, 미초기화 변수, 외부 함수 반환값, 포인터 인자를 사용자 개입 없이 처리하는 전략.
3. 심볼릭 메모리 모델링: 심볼릭 포인터와 에일리어싱 시나리오를 지원하여 임의의 데이터 구조를 분석할 수 있는 메모리 모델.
4. 루프 바운딩 전략: 루프 반복을 제한하여 종료를 보장하면서도 심볼릭 실행이 후속 코드 블록으로 진행될 수 있도록 하는 알고리즘.
5. 실증적 평가: 실제 소프트웨어(GNU Coreutils) 및 NIST Juliet Test Suite를 사용한 종합적인 평가.

실험 결과

본 방법은 KLEE 심볼릭 실행 엔진(v3.1)의 확장 기능으로 구현되었으며, 세 가지 맥락에서 평가되었다.

1. 실제 경로에 대한 확장성 (Scalability on Real-World Paths):

   • GNU Coreutils에서 추출된 234개의 ICFG 경로(22개에서 1,218개의 기본 블록 범위)를 대상으로 테스트하였다.
   • **95.3%의 재현율(recall)**을 달성하여 223개의 경로를 성공적으로 검증하였다.
   • 49개의 경로는 루프 바운딩 전략(임계값 3으로 설정)이 필요했으며, 174개는 이를 필요로 하지 않고 검증되었다.
   • 실행 시간은 단순한 경로의 경우 1분 미만에서부터, 헤비한 심볼릭 포인터 산술이 포함된 복잡한 경로의 경우 약 30분에 이르기까지 다양했다.

2. MLH 정적 분석기와의 통합:

   • Juliet Test Suite(CWE-401: 메모리 누수 서브셋)를 대상으로 평가하였다.
   • 통합 결과, 허위 보고를 필터링함으로써 MLH 도구의 정밀도(precision)를 56.6%에서 100%로 높였다.
   • 재현율은 100%로 유지되어, 실제 취약점이 하나도 누락되지 않았음을 확인하였다.

3. KLEEF와의 비교:

   • Juliet 서브셋(CWE-415 및 CWE-416)에 대해 Infer와 Clang Static Analyzer(CSA)의 보고서를 사용하여 KLEEF(산업용 코드를 위한 KLEE 파생 버전)와 비교하였다.
   • KLEEF 성능: 성능이 현저히 저하되었다. Infer의 경우, KLEEF는 F1 점수를 1.0에서 0.0으로 감소시켰다(모든 참(true positive)을 실행 불가능하거나 크래시로 분류함). CSA의 경우, F1 점수가 0.766에서 0.074로 떨어졌다.
   • 제안된 방법의 성능: Infer의 베이스라인 F1 점수(1.0)를 유지하였고, CSA의 경우 약간 개선된 0.767을 기록하였다. 본 방법은 모든 참(true positive)을 성공적으로 검증하였으며, 허위 보고(추가적인 체크를 통해 필터링 가능한)에 대해서도 타당한 경로를 정확히 식별하였다.

의의 및 주장

본 논문은 제안된 방법이 심볼릭 실행의 높은 정밀도와 실질적인 소프트웨어 보안 테스팅에 필요한 확장성 사이의 간극을 효과적으로 메운다고 주장한다. 실행을 지향하고 심볼릭화를 자동화함으로써, 이 접근 방식은 실제 취약점 탐지를 희생하지 않으면서 정적 분석 보고서에서 실행 불가능한 경로를 성공적으로 필터링하여 허위 보고를 제거한다.

저자들은 루프 바운딩 전략이 완전성과 확장성 사이의 트레이드오프를 발생시켜 일부 논리적으로 도달 불가능한 경로를 탐색할 가능성이 있음을 인정한다. 그러나 이들은 정적 분석 보고서의 유효성을 검증하는 맥락에서는, 모든 루프 동작에 대한 철저한 탐색보다는 타겟 결함 위치의 도달 가능성을 보장하는 것이 우선순위이므로 이것이 수용 가능한 트레이드오프라고 주장한다. 본 방법은 기존 정적 분석 도구의 신뢰성을 높이는 강력한 후처리 단계로서 제시된다.