기술 요약: 인터프로시저럴 제어 흐름 경로 타당성 분석을 위한 심볼릭 실행 강화

문제 정의

정적 분석은 소프트웨어 보안 및 신뢰성을 위한 확장 가능한 기술이지만, 종종 높은 오탐(false-positive)율로 인해 어려움을 겪습니다. 이러한 오탐은 정적 분석기가 인터프로시저럴 제어 흐름 그래프(ICFG) 상의 제어 흐름 경로를 보고할 때, 이론적으로는 가능하지만 런타임 시의 의미론적 제약(예: 상충하는 변수 값)으로 인해 실제로는 실행 불가능한 경로를 포함하기 때문에 발생합니다. 프로그램의 ICFG 내 특정 경로가 실행 가능한지 결정하는 것을 **경로 타당성 분석(path feasibility analysis)**이라고 합니다.

**심볼릭 실행(symbolic execution)**은 심볼릭 값과 SMT 솔버를 사용하여 경로를 탐색함으로써 경로 타당성을 검증하는 강력한 기술이지만, 이 특정 문제에 적용할 때 두 가지 주요 과제에 직면합니다:

1. 자원 요구량 및 경로 폭발: 표준 심볼릭 실행은 모든 도달 가능한 경로를 탐색하려고 시도하며, 이는 루프와 복잡한 분기가 존재하는 환경에서 지수적인 상태 증가를 초러합니다.
2. 자동화 격차: 기존 엔진은 알 수 없는 값을 가진 변수(예: 초기화되지 않은 메모리, 외부 함수 반환값, 포인터 인자 등)를 처리하기 위해 수동 설정이 필요한 경우가 많으며, 이는 정적 분석 도구와의 완전한 자동화 통합을 저해합니다.

방법론

저자들은 사전에 정의된 ICFG 경로 집합을 검증하기 위해 설계된 지향적 심볼릭 실행(directed symbolic execution) 방법을 제안합니다. 전체 상태 공간을 탐색하는 전통적인 심볼릭 실행과 달리, 이 접근 방식은 타겟 경로를 향해 실행을 엄격하게 유도하여 관련 없는 브랜치의 탐색을 제거합니다.

이 방법론은 네 가지 핵심 기술 구성 요소에 의존합니다:

1. 지향적 실행 및 가지치기(Pruning)

알고리즘은 허용된 기본 블록의 집합($S_{allowed}$)과 필수 마일스톤의 집합($S_{req}$)을 입력으로 받습니다. 실행 중:

• 가지치기: 모든 분기점에서 $S_{allowed}$에 속하지 않는 후속 기본 블록은 가지치기되어 엔진이 무관한 코드 영역을 탐색하는 것을 방지합니다.
• 검증: 실행이 타겟 블록($B_{target}$)에 도달하면서 $S_{req}$의 모든 블록을 방문하고 $S_{allowed}$ 내에 머물렀을 때만 해당 경로가 타당한 것으로 간주됩니다.

2. 자동 심볼릭화 전략

알려지지 않은 값을 가진 변수들을 자동화하여 분석할 수 있도록, 저자들은 표준 실행에서 구체적(concrete)이거나 알 수 없는 값들을 심볼릭화하는 전략을 도입했습니다:

• 진입점 파라미터: 경로 분석이 시작되는 함수의 모든 파라미터를 심볼릭화합니다.
• 초기화되지 않은 변수 및 메모리: 초기화되지 않은 지역 변수와 동적 할당된 메모리(예: malloc을 통한)는 구체적인 초기화 대신 제약이 없는 값인 심볼릭 객체로 취급됩니다.
• 외부 함수:
  • 반환 값: 본문(body)을 사용할 수 없는 외부 함수의 반환 값을 심볼릭화합니다.
  • 포인터 인자: 외부 호출의 비상수(non-constant) 포인터 인자가 참조하는 메모리 위치를 부수 효과(side effect)를 고려하여 재심볼릭화합니다.
  • 특수 전역 변수: errno(외부 호출 후 심볼릭화됨)와 environ(문자열 비교 시 비종료 문제를 방지하기 위해 고정된 길이를 가진 심볼릭 변수 집합으로 모델링됨)에 대한 특수 처리가 적용됩니다.
• 함수 포인터 및 가상 함수: 가상 테이블과 함수 시그니처를 분석하여 함수 포인터 및 가상 호출의 잠재적 타겟을 해결하고, 모든 유효한 후보에 대해 심볼릭 상태를 포크(fork)합니다.

3. 유연한 메모리 모델

본 논문은 고정된 크기의 배열 할당에 의존하지 않고 심볼릭 포인터를 지원하는 메모리 모델을 소개합니다.

• 지연 할당(Lazy Allocation): 심볼릭 포인터가 역참조될 때까지 메모리 객체는 생성되지 않습니다.
• 에일리어싱(Aliasing) 처리: 심볼릭 포인터가 역참조될 때, 엔진은 에일리어싱 시나리오를 고려합니다. 포인터가 기존 메모리 객체(일치하거나 다른 오프셋을 가짐)를 참조하는 경우와 완전히 새로운 메모리 위치를 참조하는 경우를 탐색하기 위해 심볼릭 상태를 포크합니다. 이를 통해 크기를 미리 정의하지 않고도 연결 리스트나 트리와 같은 복잡한 데이터 구조를 분석할 수 있습니다.

4. 루프 바운딩 전략

루프에서의 경로 폭발을 완화하기 위해, 이 방법은 루프 바운딩 전략을 사용합니다:

• 최대 반복 횟수($C_{max}$)가 정의됩니다.
• 심볼릭 상태가 루프에 $C_{max}$ 번 이상 진입하면, 엔진은 사용 가능한 탈출 엣지를 통해 강제로 루프를 빠져나가도록 합니다.
• 결정적으로, 루프 실행 중에 기록된 메모리 위치는 강제 탈출 전에 심볼릭화됩니다. 이는 정확한 반복 횟수가 절단되더라도 엔진이 루프의 부수 효과에 의존하는 경로를 여전히 탐색할 수 있도록 보장합니다. 이는 완전성과 확장성 사이의 트레이드오프를 도입하며, 타겟 결함 위치의 도달 가능성을 우선시합니다.

주요 기여

본 논문은 다음과 같은 기여를 주장합니다:

1. 지정된 집합 내의 임의의 ICFG 경로의 타당성을 결정하기 위한 지향적 심볼릭 실행 알고리즘.
2. 알 수 없는 값을 가진 변수, 외부 함수 반환값 및 포인터 인자에 대한 완전 자동 심볼릭화 전략.
3. 고정된 크기 제약 없이 심볼릭 포인터 추론을 지원하는 메모리 모델.
4. 심볼릭 실행을 종료시키지 않으면서 반복을 제한하는 루프 바운딩 알고리즘.
5. 실제 소프트웨어 및 Juliet 테스트 스위트에 대한 경험적 평가.

실험 결과

이 방법은 KLEE 심볼릭 실행 엔진(v3.1)의 확장 기능으로 구현되었으며, 다음 데이터셋을 사용하여 평가되었습니다:

1. 실제 경로 검증 (GNU Coreutils)

• 데이터셋: 22개에서 1,218개의 기본 블록으로 구성된 234개의 고유한 GNU Coreutils ICFG 경로.
• 결과: 이 도구는 **95.3%의 재현율(recall)**을 달 প достижение하여, 234개 경로 중 223개를 성공적으로 검증했습니다.
• 관찰: 49개의 경로에서 루프 바운딩 전략이 필요했습니다. 연구에서는 DFS가 시간 제한 내에 상태에 도달하지 못하는 복잡한 루프 시나리오에서 타겟 상태를 찾기 위해 BFS 전략이 때때로 필요했음을 언급했습니다.

2. MLH 정적 분석기 통합

• 설정: 이 방법을 MLH 정적 분석 도구에 통합하고 Juliet Test Suite(CWE-401: Memory Leak)에서 테스트했습니다.
• 결과: 통합 결과, 도구의 정밀도(precision)를 56%에서 100%로 높이면서 100%의 재현율을 유지했습니다. 이 방법은 true positive를 버리지 않으면서 모든 false positive를 성공적으로 제거했습니다.

3. KLEEF와의 비교

• 설정: 제안된 방법은 Juliet Test Suite(CWE-415 및 CWE-416)에 대한 Infer 및 Clang Static Analyzer(CSA)의 보고서를 사용하여 KLEEF(특수화된 KLEE 파생형)와 비교되었습니다.
• 결과:
  • Infer: KLEEF는 F1-score를 1.0에서 0.0으로 감소시켰습니다(60개의 보고서에서 충돌이 발생하고 모든 true positive를 infeasible으로 분류함). 제안된 방법은 F1-score 1.0을 유지했습니다.
  • CSA: KLEEF는 F1-score를 0.766에서 0.058로 감소시켰습니다. 제안된 방법은 F1-score 0.767을 유지했습니다(일부 false positive를 필터링하여 정밀도를 약간 개선하면서 재현율 100%를 유지함).
• 분석: 저자들은 KLEEF의 실패 원인을 특정 외부 함수 호출과 심볼릭 포인터 산술을 처리하지 못해 조기에 종료되는 능력 부족으로 돌렸습니다.

의의 및 주장

본 논문은 정적 분석의 확장성과 심볼릭 실행의 정밀도 사이의 간극을 메우기 위한 실질적인 해결책으로서 이 연구를 포지셔닝합니다. 저자들은 심볼릭 변수를 수동으로 설정하지 않고 심볼릭 실행을 지향하고 심볼릭화를 자동화함으로써, 정적 분석기가 보고한 실행 불가능한 경로를 효과적으로 필터링할 수 있다고 주장합니다.

이 연구의 의의는 다음과 같습니다:

• 심볼릭 변수에 대한 수동 설정 없이 검증 프로세스를 자동화합니다.
• 고정된 크기 근사치를 요구하거나 실패하기 쉬운 복잡한 메모리 모델(포인터, 동적 할당)을 처리합니다.
• 정적 분석 지표 개선: 특히, 이 방법은 실제 취약점 탐지(재현율 유지)를 희생하지 않으면서 오탐을 제거하여 정밀도를 높이는 능력을 입증했습니다.

저자들은 루프 바운딩 전략으로 인한 완전성과 확장성 사이의 트레이드오프를 인정하지만, 정적 분석 보고를 검증한다는 특정 목표를 고려할 때 타겟 위치의 도달 가능성을 우선시하는 것이 수용 가능한 절충안이라고 주장합니다. 향례 작업으로는 효율성을 더욱 향상시키기 위해 분석을 병렬화하고 특화된 상태 선택 전략을 개발하는 것이 제안되었습니다.