A Value Set Analysis Refinement Approach Based on Conditional Merging and Lazy Constraint Solving

둘기비·2024년 2월 20일

IEEE Access IEEE Access 2019

analysis :: paper

목록 보기

3/5

배경지식

Numeric-analysis

수학적 분석 문제에 대해 수치 근사를 사용하는 알고리즘에 대한 분석
대략적인 해를 찾으려고 시도하는 수치적 방법에 대한 연구

Pointer-analysis

어떤 포인터 또는 힙 참조가 어떤 변수 또는 저장 위치를 가리킬 수 있는지를 설정하는 정적코드 분석 기술

Memory corruption

버그로 인한 메모리 오염. 즉, 예상되지 않은 메모리 값 변경, 참조 등에 의해서 발생함
원인은 다양함. 안전하지 않은 함수의 사용, 잘못된 함수 사용, 잘못된 포인터 사용 등 프로그래밍 실수로 인해서 발생
실수로 사용중인 메모리를 다른 엉뚱한 곳에서 메모리 덮어쓴다거나, 들어가지 말아야한 메모리 주소에 데이터가 들어가는 것을 의미

제약 조건 해결 관련 개념들

Lazy constraint

solver가 문제를 해결할 때, 필요한 제약 조건들을 처음부터 모두 고려하지 않고, 해결 과정 중에 필요할 때마다 점진적으로 추가하는 방식
특히 제약이 매우 많거나, 복잡한 문제에서 유용하고, solver가 더 빠르게 해를 찾도록 도와줌
초기에 모든 조건이 고려되지 않기 때문에, solver는 비교적 '가벼운' 문제부터 시작하여 점차 필요한 제약 조건들 추가하면서 해 좁혀감

Under-constraint

주어진 시스템이나 모델에서 필요한 제약 조건이 충분하지 않아, 해결책이 불분명하거나 여러 개가 될 수 있는 상태를 의미
문제에 대해 너무 적은 제약 조건이 적용되어 해가 과도하게 많아지는 상황
모호함 초래할 수 있고, 결정적인 해결책 찾는 데에 방해될 수 있음

User cuts

최적화 문제, 특히 integer linear programming 같은 분야에서 사용되는 기법
문제의 해결 공간을 줄이기 위해 사용자가 추가적으로 정의하는 제약 조건
이런 cuts는 솔루션이 속해야하는 공간을 좁히고, 불필요한 검색 공간을 제거하여 문제를 더 효율적으로 해결할 수 있도록 도움
문제를 더 빠르게 해결하기 위해 사용자가 사전 지식이나 통찰력을 바탕으로 수동으로 추가하는 제약 조건

Reserved space

본문에서는 reversed space라고 되어있는데, 오타인 것 같음
프로그래밍에서 변수나 데이터 구조체에 할당된 메모리 영역을 의미
해당 변수나 데이터가 사용할 수 있는 메모리의 범위가 정해져 있으며, 이 범위를 초과하는 메모리 접근은 오류나 보안 취약점 발생 가능

Out-of-bounds access

프로그램이 프로그래머가 지정해 놓은 배열이나 메모리 범위를 넘어선 범위를 뜻함

Httpd

HTTP 데몬
웹 서버의 백그라운드에서 실행되어, 들어오는 서버 요청을 대기하는 소프트웨어 프로그램
자동으로 요청에 응답하며 http를 사용하여 인터넷을 경유, 하이퍼텍스트, 멀티미디어 문서들 서비스함

Lightweight algebraic solver

단순하거나 제한된 기능을 가진 대수적 문제를 해결하기 위한 소프트웨어 도구
소프트웨어 분석, 특히 정적 분석 도구 내에서 path constraints 해결하는 데 사용됨
정적 분석에서 프로그램의 가능한 모든 실행 경로 고려해서, 오류 찾거나 프로그램 행동 예측
- 이 과정에서, 프로그램의 조건문이나 루프 같은 구조들로 인해 복잡한 path constraint 발생할 수 있는데, 이런 path constraint를 해결하기 위해 대수적 solver 사용함.
이 solver들은 변수들 사이의 관계를 해석하고, 가능한 입력 값들의 범위 좁혀서 오류 가능성 평가
lightweight: solver가 비교적 '간단한' 문제에 초점을 맞추거나, 리소스 사용을 최소화하기 위해 최적화되었음을 말함. 전체 기능을 갖춘 solver에 비해 빠른 성능 제공하지만, 더 복잡한 대수적 구조나 비선형 문제 해결하는 데는 덜 효과적일 수 있음

Abstract interpretation theory

추상 해석 이론
프로그램의 동작을 수학적으로 모델링하고 분석하는 방법론 중 하나
프로그램 실행하지 않고도 프로그램의 가능한 상태와 행동을 이해하기 위해 고안됨
프로그램의 execution 동작을 더 단순한 형태의 abstract한 동작으로 변환하여 분석하는 과정
프로그램의 실행에 대한 정확한 정보를 포기하고(예를 들어, 모든 가능한 입력값과 모든 실행 경로를 고려하는 대신), 더 간단하고 관리 가능한 추상적 모델을 사용하여, 프로그램의 실제 동작에 대한 '안전한 근사치'(safe approximation)를 제공
- 실제 프로그램의 모든 가능한 동작을 포함하지만, 그 중 일부는 실제로 발생하지 않을 수도 있음

Indirect jump

프로그램이 실행 시점에서 결정되는 주소로 점프하는 것
- jump 명령어가 실행될 때 점프 대상 주소가 고정되어 있지 않고, 런타임에 의해 결정되는 주소(e.g., 레지스터의 값이나 메모리 내의 값)로 사용한다는 것을 의미
함수 포인터나 가상 함수 테이블(vtable) 등을 통한 동적인 함수 호출에 자주 사용됨
실행 중에 결정되는 주소로 프로그램의 제어 흐름을 이동시켜서, 고정된 위치가 아닌 다양한 위치로 jump할 수 있는 유연성을 제공하나, 이 때문에 공격자가 조작 가능한 jump 대상을 이용한 코드 실행 공격에 취약할 수 있음

예)

	```C
	#include <stdio.h>

	void functionA() {
	    printf("Function A called.\n");
	}

	void functionB() {
	    printf("Function B called.\n");
	}

	int main() {
	    // 함수 포인터 선언 및 초기화
	    void (*func_ptr)();

	    // 조건에 따라 함수 포인터가 가리키는 함수를 결정
	    int condition = 1; // 이 값에 따라 호출되는 함수가 달라짐
	    if (condition) {
	        func_ptr = functionA;
	    } else {
	        func_ptr = functionB;
	    }

	    // 함수 포인터를 통한 간접 호출
	    (*func_ptr)(); // 실제 호출되는 함수는 런타임에 결정됨

	    return 0;
	}
	```
	- `func_ptr`는 함수 포인터로, `functionA` 또는 `functionB`를 가리킬 수 있음
	- `main` 함수에서 조건문을 통해 `func_ptr`가 어떤 함수를 가리킬지 결정하고, 마지막 line의 `(*func_ptr)()`를 통해 실제 함수를 간접적으로 호출
	- 이때, `func_ptr`에 저장된 주소로의 점프는 간접 점프에 해당

Loop unrolling(unwinding)

프로그램 실행 속도를 높이기 위한 컴파일러 최적화 기법 중 하나
반복문의 반복 횟수 줄이면서, 같은 연산을 더 적은 횟수의 반복으로 수행할 수 있도록 반복문의 본문을 여러번 복사하여 넣는 방식으로 작동

Use-Define Chain

프로그램 분석에서 사용되는 개념
프로그램 내의 각 변수 use 지점과 해당 변수에 값을 할당하는 정의(define) 지점 사이의 관계를 나타내는 데이터 구조
이 체인은 변수가 어디서 정의되고, 어디서 사용되는지 추적함으로써 프로그램의 데이터 흐름을 이해하는 데 도움 줌
이 체인 사용하면, 쓰이지 않는 변수 할당을 제거하는 dead code elimination 최적화 수행 가능하고, 정적 분석 도구는 이 체인 사용해서 잠재적인 버그나 코드 문제점 발견 가능

예

	```c
	int x = 0;    // Definition of x
	x = x + 1;    // Use of x followed by a redefinition
	printf("%d", x); // Use of x
	```

Dispatch table

ABSTRACT

기존의 VSA 기반의 memory corruption 탐지 분석 기술은 high FP <- VSA의 부정확성 때문
VSA의 부정확성에 대한 주요 두가지 이유 및 본문의 해결법
- merge operation -> conditional merging
- 프로그램 경로를 서브셋으로 나누고, 같은 서브셋으로부터의 state들이 있는 조건을 만족하는 state들만 병합하기 위해, variable dependence analysis 알고리즘 사용
- failed branch conditions tracking -> lazy constraint solving
- path predicate를 path constraint로 수집하고, 변수의 refine이 필요할 때, 변수의 수 범위를 줄이기 위해 lazily하게 SMT 솔버를 사용하여 path constraint를 해결한다.
프로토타입 RVSA 구현 및 효과 입증
- state-of-the-art 접근법과 비교해서, FP가 12.9% 줄어든 것 증명
- Netgear httpd 바이너리에서 25개 제로데이 취약점 발견

1. INTRODUCTION

동적 분석과 정적 분석 장단점
- 정적 분석은 바이너리 프로그램을 어셈블리 코드나 중간 언어로 lift하고, 프로그램 속성을 모델링해서 specialized한 모델을 사용하고, 취약점 찾기 위해 보안 전략을 사용해서 속성을 탐지함
VSA
- abstrac interpretation theory기반의 정적 분석
- 고정된 point의 계산을 간소화하고 근사화하며, 균형적인 효율성과 정확성 달성
- VSA는 프로그램 내 주어진 어떠한 point에서 프로그램 state의 tight한 과대 근사화(i.e., 메모리와 레지스터의 값)를 식별하고자 함
- 가능한 타겟의 indirect jump 또는 메모리 read/write operation을 이해하는데 사용됨
Original design of VSA
- CoderSufer/x86이라는 바이너리 프로그램 정적 분석 플랫폼으로 통합됨
Angr
- angr-VSA: angr에 VSA-based memory corruption detection analysis 구현함
- 메모리 read/write operation의 타겟 주소를 확인함으로써 버퍼 오버플로우 취약점 탐지를 위함
- DARPA CGC dataset을 사용해서 평가
- angr-VSA는 130개 FP를 발생시켰고, 27개의 실제 취약점 식별함(FP rate=82.8%) => 수동으로 다 검사하기에 unacceptable
![[Pasted image 20240119121815.png|200]]
VSA의 결과는 over-approximate, 부정확함
- Challenge1: fully merging strategy
- 같은 기본 블록으로 도달하는 두개의 state에 대해, VSA는 그 두 state들을 하나의 새로운 state로 병합하고, 이 merge operation은 precision loss 발생시킴
- Challenge2: tracking branch conditions
- conditional exit 후, state에서 변수를 제약할 수 있어서, 보다 정확한 분석 결과 얻을 수 있음
- conditional exit(조건부 출구): 프로그램의 분기문(조건문)에서 특정 조건에 따라 실행 흐름이 나눠지는 지점
```
				```c
				if (condition) {
				    // 조건이 참일 때 실행될 코드
				} else {
				    // 조건이 거짓일 때 실행될 코드
				}
				```
				- 위 예에서, if (condition)  부분이 conditional exit
	- 새로운 path predicate이 나타나면, VSA는 solver를 이용해서 해결하는데
		- solver가 너무 heavyweight하면, time consuming하고, impractical함.
		- 너무 lightweight하면, 복잡한 분기 조건문을 추적하는데 실패해서, precision loss 발생 가능
```
Goal: VSA의 precision 증가시키기
- Challenge1 sol: variable dependence analysis 알고리즘으로 프로그램 경로를 subset들로 나누고, 같은 subset들로부터 abstract한 state를 조건적으로 병합해서, merging operation으로 발생한 부정확성 줄임
- Challenge2 sol: heavyweight solver인 lazy constraint solving을 위한 SMT solver 사용. lazy constraint solving은 VSA 수행 중에, path predicate를 state의 path constraint로 수집.
- 변수가 refine이 필요할 때, 변수의 tighter한 수 범위를 얻고자, path constraint를 해결하기 위해 SMT solver 사용해서, failed branch conditions tracking으로 발생한 부정확성 줄임
prototype system RVSA(Refined Value Set Analysis)
evaluate on DARPA CGC dataset, Netgear httpd binary
- result: angr-VSA 대비 FP 12.9%감소

Contributions

프로그램을 subset으로 나누는 variable dependence analysis algorithm 제안
conditional merging과 lazy constraint solving 기반의 value set analysis refinement approach 제안 ⇒ FP 감소
prototype system 구현 및 effectiveness 증명

2. BACKGROUND

A. VALUE SET ANALYSIS

VSA는 각 레지스터와 메모리 위치가 프로그램 포인트에서 보유하는 numeric 값 또는 주소들의 set의 과대 근사화를 결정하는 numeric-analysis와 pointer-analysis algorithm의 조합
아래 세가지는 VSA의 abstract domain

1) MEMORY REGION

실행 파일을 분석하는 동안, VSA는 주소 공간을 memory region이라고 하는 서로 다른 메모리 영역의 집합으로 분할합니다.
모든 메모리 영역에는 영역 식별자(RegionId)가 있음
- global-region: 전역 데이터에 해당하는 위치에 대한 정보 포함
- AR-regions(Activation Record): 특정 절차(procedure)의 activation record에 해당하는 위치에 대한 정보 포함. 함수나 절차의 스택 프레임 내에 있는 지역 변수들이 이 리전에 해당
- Malloc-regions(동적 할당 리전): 특정 malloc 사이트에서 할당된 위치에 대한 정보 포함. 동적으로 할당된 메모리 블록들이 이 리전에 해당
각 memory region은 유사한 런타임 특성을 갖는 abstract location의 그룹을 나타내며, abstract location은 a − loc이라고 하는 변수의 주소 나타냄.

2) VALUE SET

value set: 주소와 numeric 값들의 집합에 대한 safe approximation
프로그램 분석에서 value set 사용하면, 프로그램이 실행될 때 가능한 값의 범위 예측 가능
표현식
- 실행 파일 내의 n개의 region이 있으면, value set은 해당 리전의 주소 집합을 나타내는 튜플의 각 요소로, s[l, u]의 형태로 strided intervals의 n-tuple로 표현됨.
- strided intervals: s[l, u] 형식으로 표현되며, 정수 집합을 나타냄; s: stride(보폭), [l,u]: interval
- 정수집합 γ (s[l, u]) := {i |l ≤ i ≤ u, i ≡ l (mod s)} 나타냄
- l부터 u 사이의 모든 정수 중에서, l로부터 s 간격으로 떨어진 정수들의 집합
예) stride s가 0인 경우, 0[l, l]는 {l}이라는 단일 원소 집합 나타냄. 이는 주소나 값의 범위가 오직 하나의 값 l로 한정됨을 의미

3) ABSTRACT STATE

memory region은 a-loc(abstract location)에서 값 집합(ValueSet)으로의 매핑으로 정의됨
- 이 매핑은 프로그램의 특정 메모리 주소(a-loc)가 취할 수 있는 값들의 범위(ValueSet)에 대한 정보 제공
- a-loc: 변수나 메모리 주소와 같은 구체적인 위치 추상화한 대표값
- ValueSet: 해당 a-loc에서 가능한 값들의 안전한 근사치. 주소 또는 숫자 값들의 집합
- Region := a-loc → ValueSet 정의. 각 추상 위치에 대응하는 가능한 값들의 집합을 나타내는 memory region
abstract state는 리전 식별자(RegionId)에서 리전으로의 매핑으로 정의됨. 이 매핑은 프로그램의 각 리전 식별자가 가리키는 메모리 리전의 상태 나타냄
- RegionId: 각각의 memory region을 구별하는 고유 식별자
- Region: a-loc에서 value set으로의 매핑
- State := RegionId → Region
VSA는 각 프로그램 포인트에서 abstract state 식별
알고리즘
- ![[Pasted image 20240117141840.png|350]]
- 프로그램 CFG를 분석해서 각 기본 블록의 abstract state 계산
- W: work-list with operation add and removeNext, 아이템을 추가하고 삭제함
- work-list는 topological order이고, 처음에는 entry 기본 블록을 포함하고, 이는 entry 기본 블록으로부터 forward analysis를 나타냄
- 각 while-loop iteration에서, Analysis함수는 선택된 기본 블록을 분석하기 위해 call됨(line 6)
- Analysis함수는 input state기반으로 여러개의 output state 생성. 이 변하는 output state들은 work-list에 추가됨
1. 초기 설정
- b0: CFG의 시작 기본 블록(EntryBlock)
- W: 작업 리스트(Work-list). 알고리즘이 처리해야할 기본 블록들을 담고 있음. 이 리스트는 topological order로 정렬, entry point는 b0로 초기화됨.
- S: abstract state 저장, b0에 대한 초기 상태(InitState)로 시작함
2. 작업 리스트 처리(line 4- 5)
- 작업 리스트 W가 비어있지 않은 동안, 알고리즘 계속 실행
- 작업 리스트에서 다음 기본 블록 b 제거(W.removeNext())
3. 기본 블록 분석(line 6)
- 선택된 기본 블록 b에 대해 Analysis 함수 호출해서 분석 수행
- Analysis 함수는 입력 상태 S[b]를 기반으로 여러개 출력 상태 생성
- 이 변하는 output state들은 work-list에 추가됨
4. 상태 업데이트 및 작업 리스트 관리(line 7)
- Analysis 함수가 반환한 각 상태 sn에 대해 반복문 수행
- sn이 나타내는 기본 블록을 bn이라고 할 때, 만약 bn이 abstract state S에 이미 존재하면
- sn과 S[bn]이 다를 경우에만, S[bn]과 sn을 Merge하고, bn을 작업 리스트 W에 추가(equation 1)
- 만약 bn이 S에 존재하지 않으면
- sn을 S에 추가하고, bn을 작업 리스트 W에 추가
- Merging operation equation of a variable
- 같은 기본 블록에서 두개의 input state가 있을 때, VSA는 두개의 input state를 새로운 input state로 병합(line 11)
- merging operation은 abstract state로 모든 변수의 value set을 병합함
- equation 1:
sm[lm, um] = s1[l1, u1] ∪ s2[l2, u2] = sm[min (l1, l2), max (u1, u2)]
- sm: s1, s2의 MCD(최대공약수),
프로그램이 메모리 read/write의 목적지 주소와 길이의 value set에 따라, 메모리를 읽거나 쓸 때, 대응하는 변수의 reserved space를 초과하는지 탐지
- 초과한다면, 잠재적 취약점으로 report
- VSA로부터 얻은 value set은 정확하지 않은 과대 근사화여서, high false postive rate 발생

B. MOTIVATING EXAMPLE

false positive 발생하는 motivating 예(왼-소스코드, 오-CFG w/기본블록)![[Pasted image 20240118122105.png|350]]

VSA가 발생시키는 두가지 false positive
1. 기본 블록 B4의 read function
- B4로 가는 방법은 B1 -> B2 ->B4, B1 -> B3 -> B4인데, 어떤 경로로 가던, B4의 v4는 30이어서, B4에서는 overflow 발생 안함
- 그러나, VSA에서는 B4의 입구에서 B2, B3의 output state가 병합돼서, v4의 값 집합이 확장되어, 오버플로우 발생 가능
- VSA는 path sensitivity(경로 감지)가 적용되지 않아, 병합 과정에서 각 변수의 value set이 과대 근사화됨. 이는, 변수의 가능한 값의 범위를 실제보다 넓게 추정해서 발생하는 문제임
- B2에서, v2는 value set 0[10,10], v3는 value set 0[20,20]을 갖고,
- B3에서, v2는 value set 0[15,15], v3는 value set 0[15,15]을 가짐
- B4에서 이런 상태들이 병합되면,
- v2의 value set 은 5[10,15], v3의 value set은 5[15,20]이 됨
- 여기서 5는 stride를 의미하고, 각 value set의 범위는 병합된 결과의 최소와 최대값을 나타냄.
- B4에서 v4의 value set이 5[25, 35]라고 하면, 이는 메모리 쓰기 작업을 수행하는 read 함수에 의해 사용됨. 이때, write target address는 str1이고, write length는 v4.
- str1의 예약된 크기는 30인데, v4의 최대값이 str1의 크기를 초과해서, VSA는 오버플로우가 발생할 수 있다고 report함
2. 기본 블록 B5의 memcpy function
- memcpy 함수가 str2를 목적지 주소로 해서, 크기 v1만큼의 memory write 작업 수행함
- B5에 도달하기 위해서는 입력이 경로 제약 v1*(v1+1)<100(line 14)을 만족해야하고, 이는 v1의 값이 10을 초과할 수 없음을 분명히 하고 있어서, overflow는 발생 X
- 그러나, VSA에서는 v1의 value set은 1[0, 232-1]로 추정돼서, 실제 가능한 값의 범위를 훨씬 초과하는 과대 근사치를 제시함.
- 이유: VSA에서 numeric abstraction domain이 사용되고, 변수들 간의 관계가 무시되기 때문
- 따라서, 이러한 분기 조건을 고려하면, v5의 value set을 1[0, 99]로 제한하는 방법만 있고, v5와 numeric 관계를 가지는 v1을 제한할 방법은 없음
변수 간의 관계를 고려하기 위해 제안된 기법
- Affine-Relation Analysis
- 이 기법은 변수 간의 관계를 파악해 더 정확한 value set을 도출할 수 있지만, 구현이 복잡하고 계산 비용이 많이 들어 실제 상황에서 적용하기 어려움
- Angr
- path predicate에 algebraic solver를 적용함
- algebraic solver는 path predicate에 관련된 변수들의 수 범위를 얻기 위해 path predicate을 단순화하고 해결하려 시도함
- 하지만, path predicate이 여러 개의 변수를 가지거나 non-linear 제약을 가지면, algebraic solver는 path predicate을 단순화하고 해결하는 것에 실패함.
- 위 예제에서는, v1*(v1+1)<100처럼 non-linear 제약을 가진 path predicate은 algebraic solver로 해결할 수 없으므로, v1의 수치 범위를 얻을 수 없음

3. DESIGN

A. OVERVIEW

VSA가 false positive를 일으키는 주요 원인은 VSA의 과대 근사화의 결과로 인해, 목적지 주소와 길이의 value set이 부정확해서임
그래서, 더 정확한 value set을 얻기 위해서 목적지 주소와 길이의 value set을 조정하는 건 FP를 효과적으로 줄일 수 있음
conditional merging과 lazy constratin solving으로 VSA 정제 접근법 제시
- ![[Pasted image 20240118132705.png]]

바이너리 프로그램 분석하고, 오버플로우가 일어날 수 있는 기본 블록과 변수들의 페어를 얻기 위해 전통적인 VSA 사용
- 바이너리 프로그램 분석할 때, 메모리 객체와 레지스터들을 변수로 간주하고, 변수의 주소는 a-loc으로 표현됨.
- figure 1에서 얻은 결과는 (B4, v4), (B5, v1)이 되고, 이건 B4의 v4와 B5의 v1이 취약점을 발생시킬 수 있다는 것임
- 그래서, 다음 단계에서 이러한 변수들을 refine함.
- 타겟 변수로써 refine이 필요한 변수와 타겟 기본 블록으로써 타겟 변수의 기본 블록을 call함.
프로그램 경로를 subset으로 나누기 위해 variable dependence analysis 를 위한 새로운 알고리즘 제안
- (B4, v4)의 variable dependence analysis는 두개의 subset을 얻음(*figure 3)
바이너리 프로그램을 분석하기 위해 conditional merging VSA 사용
- 같은 서브셋으로부터의 state들만 병합함
- 그래서, B2에서 B4로 가는 state와 B3에서 B4로 가는 state들은 다른 subset으로부터 오기 때문에, 병합되지 않음
- 그러므로, B4에는 두개의 state가 있고, 두개의 state 내 v4의 value set은 개별적으로 탐지됨. 두개 다 0[30,30]임. 그래서 (B4, v4)는 overflow가 되지 않음
path predicate는 VSA에서 abstract state의 path constraint로 수집됨
- 타겟 기본 블록에 도착한 후에, SMT solver를 사용하여, 해당하는 path constraint를 lazily하게 해결하고, 타겟 변수의 tighter한 수 범위를 얻음.
- 즉, B5에 도착했을 때, path constraint는 v1*(v1+1)<100이고, 따라서 SMT solver로 해결한 v1의 수 범위는 [0,9]임. 그래서, v1의 value set은 1[0,9]dlrh, qustn (B5, v1)은 overflow되지 않음

B. VARIABLE DEPENDENCE ANALYSIS

Definition 1 (Variable Dependence)
- 타겟 기본 블록에 도착한 execution path에 대해, 타겟 변수를 back tracking하는 것은 어떤 기본 블록이 타겟 변수의 최종 값 계산을 포함하고 있는지 아는 것임.
- 그래서, 이러한 기본 블록 set을 이 경로의 variable dependece로 정의함
Definition 2 (Variable Dependence Subgraph)
- variable dependence subgraph는 CFG의 서브 그래프임.
- variable dependence subgraph에서의 모든 경로는 같은 variable dependence를 갖고 있고, variable dependence의 첫번째 기본 블록에서 시작하고, 타겟 기본 블록에서 끝남.

만약, 두 실행 경로가 같은 variable dependence를 갖고 있으면,
- 타겟 변수의 value set은 같은 명령어로부터 영향을 받음. 그래서, 오직 같은 variable dependence subgraph의 state들만 병합됨.
- 그래서, variable dependence analysis 알고리즘을 제안해서, 타겟 변수에 대해 모든 variable dependence subgraph를 생성함.
만약, 프로그램에 loop가 있다면,
- 경로 폭발 문제 때문에, 모든 실행 경로를 얻는 건 불가능함.
- 그래서 이 문제를 해결하기 위해, loop unrolling을 사용함
- loop unroll의 수를 2로 설정되어, loop body가 한번 이상 실행된다는 것.
- variable dependency anlaysis는 모든 variable dependence들을 찾는 것인데, 이는 loop unroll을 두번하면 충분함.
- 그래서, loop unrolling 이후에, directed acyclic graph인 새로운 CFG를 얻게 됨.
Algorithm 2
- ![[Pasted image 20240120152054.png]]
- 타겟 변수 v0, 타겟 기본 블록 b0, loop unroll된 CFG를 인풋으로 받고, set W는 여기서 call된 work-list(아이템 추가와 삭제 연산 수행)
- 아이템은 4 요소를 갖는 튜플임(b, vs, d, g)
- b는 분석될 기본 블록, vs는 정의가 분석되지 않은 변수들 집합, d는 분석된 variable dependence, g는 해당하는 variable dependence 서브 그래프, W는 기본 블록의 topological order로 정렬되고, 처음에 타겟 기본 블록을 포함해서, 타겟 기본 블록부터 backward 분석 수행.
- while-loop의 각 iteration에서, 분석할 아이템 선택(line 7).
- line 8: GetDefineVar함수는 기본 블록 b에서 요소가 정의된 vs의 서브셋인 vsd를 얻음 <- Use-Define Chain으로 빠르게 얻을 수 있음
- Use-Define Chain은 프로그램 내의 각 변수 use 지점과 해당 변수에 값을 할당하는 정의(define) 지점 사이의 관계를 나타내는 데이터 구조
- vs 내 사용된 모든 변수 v에 대해, 변수 v를 정의하는 모든 기본 블록을 얻을 수 있음
- 이러한 기본 블록이 최근 기본 블록 b를 포함한다면, v는 기본 블록 b에서 정의되고, 집합 vsd에 추가됨
- line 10: 만약, 기본 블록 b가 변수 vsd를 정의했다면, 함수 AnalysisBlock은 reverse order에 따르는 기본 블록들의모든 명령어를 분석하고, 변수 vsd의 값 계산을 포함한 모든 변수 vsu를 얻기 위해 호출됨
- 그러면, vsd를 지우고, vsu를 추가함으로써 vs 업데이트함
- line 14: 만약, vs가 빈 집합이라면(이 경로에 포함된 모든 변수가 분석됐다는 의미), 최종 variable dependence subgraph인 g를 G로 저장함.
- G는 variable dependence에서 variable dependence 서브그래프로의 맵핑
- line 20: 만약 vs가 안 비어있으면(backward 분석을 지속할 필요가 있다는 의미), 이전 기본 블록을 work list인 W에 추가

C. CONDITIONAL MERGING

같은 variable dependence subgraph로부터 같은 기본 블록에 도달하는 두 state들만 병합됨 -> 그래서, 어떤 variable dependence subgraph로부터 state들이 오는지 알아야함
모든 기본 블록들이 어떤 state를 순회하는지 찾는 것은 쉬움
- 하지만, 각 병합 포인트들에서 모든 순회된 기본 블록들과 두개의 state들을 비교해야해서 expensive함
그래서, 기본 블록의 서브셋을 식별해야함(다른 variable dependence subgraph들은 차별성을 남기도록)
GOAL: CFG에 몇가지 기본 블록에 표시해서, 각 변수 의존성 하위 그래프 pair에 대해 표시된 기본 블록만 고려해서 구별할 수 있도록 하는 것
- 즉, 경로는 이제 모든 기본 블록 대신, 그것이 순회하는 표시된 기본 블록의 시퀀스로 표시됨
모든 변수 의존성 하위그래프는 타겟 기본 블록으로 끝나기 때문에, 임의의 두 변수 의존성 하위그래프는 타겟 기본 블록을 포함하는 가장 큰 공통 서브 그래프를 가짐.
- 모든 변수 의존성 하위그래프는 가장 큰 공통 서브 그래프에 하나 이상의 들어오는 edge를 가짐
- 이 edge들을 back tracking하면 ,가장 가까운 public parent 기본 블록을 얻을 수 있음.
- 이 기본 블록을 표시하면 이 변수 의존성 하위그래프를 다른 하위 그래프와 비교할 수 있음
algorithm of selecting marked basic blocks
- ![[Pasted image 20240120162220.png|400]]
- 변수 의존성 하위그래프의 갯수 n과 모든 변수 의존성 하위그래프 CFG0부터 CFGn-1를 인풋으로 가짐
- line 4: 어떠한 두개의 변수 의존성 서브그래프들 CFGi와 CFGj에 대해, 가장큰 공통 서브그래프인 CFGc를 얻기 위해 함수CommonSubGraph를 사용함
- 그리고, CFGi에서 CFGc로 들어가는 모든 edge를 얻고, 그 edge들의 가장 가까운 public parent 기본 블록 b를 얻고, 마킹된 기본 블록 MB에 b를 추가함
- 마킹된 기본 블록을 얻은 후에는, conditional merging VSA를 사용해서 프로그램을 재분석해야함
- conditional merging은 변수 의존성 하위그래프에서 오직 기본 블록의 state에만 영향을 미침. 그래서, 전체 프로그램을 재분석하지 않고, 모든 변수 의존성 하위그래프인 CFGu의 union(합집합)만 재분석함(equation 2)
- CFGu = CFG0 ∪ CFG1 ∪ . . . ∪ CFGn−1
conditional merging을 지원하기 위해 전통적인 VSA 알고리즘을 수정함
algorithm of conditional merging VSA
- ![[Pasted image 20240120164553.png]]
- 전통적인 VSA와의 비교
- line 1-6: work-list의 초기 값은 더이상 프로그램 entry 기본 블록이 아니고, in-degree가 0인 모든 노드들임. 이 노드들의 초기 state는 전통적인 VSA state인 S0로부터 얻은 state임
- line 9-10: 기본 블록의 state는 더이상 단일 state가 아니고, 다수의 state가 동시에 존재할 수 있음. 그래서, list는 기본 블록의 상태를 저장하는데 사용되고, output state들은 각 input state들에 대해 별도로 생성돼야함
- line 12-13: 기본 블록이 분석된 후에, 기본 블록이 마킹된 기본 블록인 MB에 있는지 확인하고, MB에 있다면, state의 mb set에 그 기본 블록을 추가함.
- line 21: 마지막으로, 병합이 필요할 때, 함수ConditionalMerge를 사용해서, conditional merging 진행. 이 함수에서는 오직 같은 mb 셋을 가진 state들만 병합됨

D. LAZY CONSTRAINT SOLVING

분기 조건을 tracking하는 것은 conditional exit을 취한 후에 stae내에서 변수를 제약하는 것을 도움. -> 분석 결과 더 정확하게 함
새로운 path predicate이 보일 때(i.e., 조건 분기를 따라갈 때), 전통적인 VSA는 path predicate 내에 포함된 변수의 수 범위를 얻기 위해 단순화하고 해결하려고 함
하지만, 많은 path predicate이 있어서, 전통적인 VSA는 ligthweight solver를 사용함(ability 제한됨)
그래서, heavyweight constraint solver를 적용함
- 새로운 path predicate이 보일때마다 해결하는 것이 아닌, path predicate를 state의 path constraint로 수집함
- 그리고나서, 변수의 value set이 refine이 필요할 때, path constraint를 단순화하고, SMT solver를 사용해서 이를 해결함

VSA 수행 중에 path predicate를 path constraint로 수집함.
- VSA 내 각 abstract state에 대해, σ를 사용해서 해당하는 path constraint를 표현함.
- 초기 state의 σ는 null
- 조건 분기(path predicate는 e)에 따를 때, VSA는 jump/not jump라는 두개의 output state를 가짐
  - jump state의 경우
  - path constraint를 σ ∧ e로 업데이트
  - not jump state의 경우
  - path constraint를 σ ∧ ¬e로 업데이트
- 두 상태가 병합될 때, paht constraint는 σm=σ1 |σ2로 업데이트됨
- 대부분의 경우, 병합된 state들은 이전의 조건 분기에서 분리된 두 state에서 발생함. 그래서 σ1과 σ2는 공통 path predicate들인 sigma0를 가짐
- 그래서, 병합된 path constraint들은 단순화됨(equation 3)
  - ![[Pasted image 20240120172844.png]]
v같은 변수를 refine 해야할 때, path constraint는 변수 v에 대해 더 단순화됨.
- 변수 v와 관련 없는 path predicate들은 삭제됨
- 이전의 변수 의존성 분석에 기반해서, 변수 v와 관련된 모든 변수들의 집합은 집합 vs로 얻을 수 있음
- 단일 path predicate σ에 대해, 만약 σ에 있는 모든 변수들이 vs에 있지 않으면, σ는 변수 v와 관계가 없다는 뜻임.
- path constraint가 연산자 ∧ (i.e. σ = σ1 ∧ σ2 ∧ . . . ∧ σn)와 연결된 여러 path predicate들을 갖고 있다면, 모든 path predicate σi에 대해, σi가 변수 v와 관련 없다면, σi는 path constraint에서 삭제됨
- path constraint가 연산자 | (i.e., σ = σ1|σ2| . . . |σn )와 연결된 여러 path predicate들을 갖고 있을 때, 변수 v와 관련없는 path predicate σi가 존재한다면, 전체 path predicate인 σ도 변수 v와 관련없다고 고려함
SMT solver를 사용해서 변수 v의 최대/최소값을 구함(as 변수의 수 범위)
- 새로 생성된 수 범위는 보통 원래의 value set의 범위 내에 있음
- 새로 생성된 수 범위는 오직 수집된 path constraint에 의해서만 결정됨
- 확장 연산자의 사용으로, path constraint가 완전하지 않을 수도 있음
  - 그래서, 새로 생성된 수 범위는 원래 value set 범위 내에 없을 수도 있음
- 그래서 변수 v의 새로 생성된 수 범위와 원래의 value set간의 교집합을 수행(equation 4)
  - ![[Pasted image 20240120173918.png]]

4. IMPLEMENATATION

RVSA 구현
- angr-VSA를 전통적인 VSA로 사용
- angr-VSA에서, VSA의 메인 인터페이스는 VFG(Value Flow Graph)
- VFG는 각 프로그램 위치에서 VSA fix-point를 나타내는 프로그램 state를 포함한 CFG임
- VFG에 포함된 프로그램 상태들은 메모리를 SimAbstractMemory 메모리 모델에 의해 제공되는 abstract 레이아웃으로 나타내는데, 메모리 내의 값들은 Claripy에 의해 제공되는 value set으로 표현됨
- 메모리 read/wirte 연산은 SimInspect로부터 hooked되고, 잠재적인 취약점을 찾기 위해, 변수가 메모리 read/write의 목적지 주소와 길이 value set으로부터 out-of-bounds access인지 탐지함
- angr-VSA로 타겟 기본 블록, 타겟 변수 찾고
- 각 변수에 대해 refine 적용하기 위해, angr의 VSA_DDG 분석 진행해서 use-define chain얻고, variable dependence analysis algorithm으로 Variable Dependence Subgraph 얻음
- conditional merging VSA 사용해서, 다른 Variable Dependence Subgraph에서 타겟 기본 블록의 여러 state 얻음
- 각 state에서 취약점 탐지 진행
angr는 바이너리를 VEX 중간 언어로 lift하고, SimEngineVex 엔진을 사용해서 VEX를 실행함
- 실행할때, path predicate를 얻을 수 있는데, 이건 claripy.ast.bool 타입임
- 각 state에 대해서 path constraint도 얻을 수 있음 -> SMT solver로 Z3을 사용함 -> Z3으로 path constraint를 얻고, 타겟 변수의 최대 최소를 얻음
- Z3의 주요 기능은 하나 이상의 이론을 논리적인 공식의 satisfiability를 검사하는 것임 -> Z3는 satisfiable한 공식을 위한 모델을 생성함. 또 SMT formula나 MaxSMT나 이들의 조합을 통해 최적화 문제를 풀 수 있음

5. EVALUATION

취약점 탐지 효율성: complex하고, real-world에서 FP rate를 효과적으로 줄이는지? 섹션5-B
design decision 정의: RVSA가 만든 design decision이 효과적인지? 섹션5-C,D
성능: running time, memory consumption에 대해 overhead 얼마나? 섹션5-E

A. EXPERIMENTAL SETUP

Lenovo desktop with an Intel(R) Core(TM) i7-7500U CPU @ 2.70GHz with 4 cores and 16 GB RAM
running: Ubuntu 18.04 TLS
angr-vsa와 RVSA 결과 비교 할 것임
- angr-vsa가 비교 대상인 이유: (1) angr는 바이너리 정적 분석 도구로 유명하고, VSA는 angr의 중요한 feature, (2) 저자가 아는 한, angr-VSA가 VSA 기반 메모리 corruption 탐지 툴 중에서 가장 낮은 false positive 달성함
angr-VSA와 비교하기 위해서, 같은 DARPA CGC 데이터셋 선택
131개의 서비스들이 이 데이터 셋 안에 있는데, 5개는 여러 바이너리 간의 통신을 포함하고 있어서, 126개 단일 바이너리 애플리케이션만 데이터셋으로 선택
- 이 데이터 셋의 각 바이너리들은 분석 시작점이 main 함수임
real-world의 취약점을 탐지하는 능력을 검증하기 위해서, Netgear R6400 Nighthawk Routers의 HTTP 서버를 데이터셋으로 골랐음
- 장비 펌웨어의 가장 최근 버전은 R6400-V1.0.1.46_1.0.32이고, http 서버 바이너리는 /usr/sbin/httpd, httpd 바이너리는 binwalk를 사용해서 펌웨어를 언팩킹함으로써 얻을 수 있음.
- httpd는 Netgear 벤더에서 개발됐고, 오픈소스가 아님
- httpd 바이너리 크기는 1.6MB라서, 바이너리는 더 복잡함
- 분석을 단순히 하기 위해서, main 함수부터 시작하지 않음
- 프로그램 예비 분석 결과, 메모리 주소 0x12299C에 디스패치 테이블이 있고, 이 디스패치 테이블에 174개의 핸들러 함수가 있다는 것을 발견함
- http post 요청을 통해서 다른 cgi로 접근하려면, 해당하는 핸들러 함수가 실행되야하고, http post 데이터는 핸들러 함수의 첫번째 인자여야함.
- 그래서, 분석은 이 핸들러 함수에서 시작하고, 첫번째 파라미터를 input content로 처리함

B. EFFECTIVENESS OF VULNERABILITY DETECTION

취약점 탐지 결과
- ![[Pasted image 20240121122545.png|350]]
- FPR=FP/(FP+Bugs)
in CGC
- RVSA는 19개 바이너리에서 27개 실제 취약점 찾아냄(주로 스택 오버플로우)
in Netgear httpd 바이너리
- 30개 취약점 발견 -> netgear 팀한테 보고 -> 이중 5개는 이전에 다른 연구자들한테 보고 받았음. 그래서 결국 25개의 zeroday 취약점 발견 -> 벤더의 취약점 ID 부여받았음 -> 아직 netgear가 새로운 패치를 release하지 않아서, 더 자세한 내용은 알려줄 수 없음
- ![[Pasted image 20240121123441.png|350]]
RVSA는 angr-vsa보다 낮은 false positive
- RVSA는 conditional merging과 lazy constraint solving을 통해서 약 절반의 FP를 줄임
- in CGC, FP가 60개나 줄었고; in netgear httpd 바이너리, 123개가 줄었음
- 결국, FP는 334개에서 151개로 줄었고, FP rate도 12.9%나 줄었음
- ![[Pasted image 20240121123749.png|350]]
- conditional merging으로 감소된 FP의 수는 121개고, lazy constraint solving으로 감소된 FP는 62개고, 비율은 2:1 정도 됨

C. CONDITIONAL MERGING

전체 334개 FP에 대해, 타겟 변수를 refine하기 위해 conditional merging 적용
- 결과![[Pasted image 20240121131105.png]]
- 각 FP에 대해, 변수 의존성 서브그래프의 개수를 얻었음
- 변수 의존성 서브 그래프는 최소1부터 30까지 였고, 만약 1개면, state는 분해할수 없어서, 이건 FP 감소를 못함
- red line은 FP의 수, blue line은 감소된 FP
- 변수 의존성 서브 그래프의 수가 증가할 수록, 감소되는 비율이 증가하고, 결과가 더 정확해짐

CASE STUDY

Netgear httpd의 프로그램에서, pppoe2.cgi요청을 핸들링할 때, 함수 sub_21D10이 실행됨
- 함수의 디컴파일된 슈도 코드의 일부분![[Pasted image 20240121131518.png]]
- 이 코드의 CFG![[Pasted image 20240121131543.png|350]]
- 변수 v10, v12, v15는 string 타입이고, 이 변수들의 길이는 len(v10), len(v12), len(v15)
- 변수 v15의 reversed size는 1024, 그래서 len(v15)의 최대값은 1024보다 크면 안됨.
- 문자열 v10이 '.'을 포함할 때, true 분기로 실행되고, 그렇지 않으면 false 분기로 실행됨. true/false 분기 둘다에서, v15와 v12는 각각 할당됨.
- true 분기에서, len(v15)의 value set은 1[198, 710]이고, len(v12)의 value set은 0[70,70]임
- false 분기에서, len(v15)의 value set은 0[198, 198]이고, len(v12)의 value set은 1[70,582]임
- 만약 두 state가 병합되면, len(v15)의 value set은 1[198, 710]이고, len(v12)의 value set은 1[70,582]임
- 그리고, strcat(v15, v12)는 메모리 write 연산을 갖게되고, 이건 타겟 주소가 v15+len(v15)이고, 크기는 len(v12)인 것임
- len(v15)+len(v12)의 최대 값은 1292이고, 이건 변수 v15로부터 할당된 1024 크기를 초과함
- 그래서, angr-VSA는 이것을 잠재적인 취약점으로 report
변수 의존성 분석 알고리즘은 true 분기와 false 분기를 두개의 다른 변수 의존성 서브그래프로 나눠서, 이 두개의 state는 병합되지 않음
각 state에 대해 len(v15)+len(v12)의 최대값은 각각 계산돼서, 변수 v15의 할당된 1024 바이트를 넘지 않음. => 논문은 이렇게 FP를 감소시킴

D. LAZY CONSTRAINT SOLVING

conditional merging이후에, 212개의 FP가 남아있음
남은 FP의 타겟 변수를 refine하기 위해 lazy constraint solving 사용
감소된 FP에 대한 lazy constraint solving 결과![[Pasted image 20240121134041.png]]
각 FP에 대해서, 변수 의존성 서브그래프에 따라 여러개의 state를 얻었음
모든 state는 path constraint를 갖고 있고, 그 path constraint는 claripy의 Abstract Syntax Tree(AST) 타입으로 표현됨
보통 path constraint가 복잡할 수록 AST의 depth도 커짐.
- 그래서, 논문에서는 AST의 depth를 이용해서, path constraint의 복잡성을 표현함.
- 만약 FP가 여러개의 state를 갖고있다면, 여러 state들의 평균 depth를 이용함
red line은 전체 FP의 수(기본적으로 균등하게 분포됨), blue line은 감소된 FP의 수. depth 범위가 3~13일 때 감소된 비율이 높음
depth가 클 때, 비율은 path constraint의 복잡성 때문에 감소됨
depth가 3보다 작을 때, 비율은 낮음
- 일부 간단한 path constraint는 lightweight algebraic solver로 해결되기 때문에, 전통적인 VSA는 이러한 경우 FP를 생산하지 못하기 때문임

CASE STUDY

DARPA CGC 데이터셋의 KPRCA_00035 프로그램에서, 함수 process_sys의 소스코드 일부![[Pasted image 20240121135105.png]]
저자는 직접 바이너리 실행 파일을 분석했고, description(설명)을 단순화하기 위해, 소스코드에 이를 설명해두었음.
machine->registers[2]의 값과 machine->registers[3]은 이전의 초기화 함수에서 유저 인풋으로 결정될 수 있어서, 변수 start(line 146)의 value set과 변수 len(line 147)는 모두 1[0,0xffff]임.
line 157에 도달하는 path constraint는 [start+len<0x10000, len! = 0].
- 첫번째 path constraint인 start+len<0x10000는 두개의 변수를 포함해서, angr-VSA의 대수 solver는 각 개별적인 변수의 수 범위를 알아낼 수 없어서, 변수 start의 value set은 1[0, 0xffff]이고, 변수 len의 value set은 1[1, 0xffff]임
sv.fp 함수 안에, 메모리 write 연산이 있음. 이는, 타겟 주소가 &machine->memory[start]이고, 크기는 len임.
- start+len의 value set은 1[1, 0x1fffe]임
- 최대 값은 machine->memory의 할당된 0x10000 바이트를 초과해서, angr-VSA는 이를 잠재적인 취약점으로 report함
In RVSA
- 논문에서 얻은 state의 path constratin는 start + len < 0x10000 ∧ len! = 0이고, SMT solver를 사용해서 얻은 start+len의 최대 최소값은 0xffff와 1이고, start+len의 refine된 value set은 1[1,0xffff]이 됨
- 그래서 overflow가 아니고, 이렇게 FP를 줄일 수 있었음

E. PERFORMING OVERHEAD

RVSA 성능 평가 위해, DARPA CGC 데이터셋에서 발견된 취약점을 가진 19개 프로그램 select함
러닝 타임이랑 메모리 소모량 기록하면서, 기본 블록의 수와 성능에 미치는 영향을 분석하기 위해 사용되는 루프의 개수도 기록
성능 평가 결과![[Pasted image 20240121141151.png]]
기본 블록 수가 많을 수록, 루프의 개수가 많을 수록, 러닝타임이 긴것 처럼 보임
- 일반적으로 기본 블록 수가 많을 수록, 더 많은 명령어가 분석되고, 실행시간이 길어질 거라는 상식에 부합함
- 루프 프로그램에서, 루프 내의 같은 기본 블록에서 여러 분석을 수행하는 건 중요함
- 이 실험에서, 루프 iteration의 최대 수는 128로 설정함
angr-VSA와 비교
- RVSA의 러닝타임은 angr-VSA의 855s에서 1107s로 증가(29.47%증가) (equation 6)
- ![[Pasted image 20240121141511.png]]
- 이 정도 증가는 상대적으로 분석 cost로써 수용가능함
- 시간 증가의 두가지 이유
- conditional merging: RVSA는 각 인풋 state에 대해 하나의 output state를 생성함. 만약 기본 블록이 병합되지 않은 여러개의 input state를 갖고 있다면, RVSA는 그 기본 블록을 여러번 분석함
- SMT solver에서 소요되는 시간: path constraint가 복잡할 때, 시간이 더 오래 걸림. SMT solver의 타임아웃은 60s로 설정함
- RVSA의 메모리 소요는 angr-VSA의 485MB에서 605MB로 증가함(24.74%) (equation 7)
- ![[Pasted image 20240121141830.png]]
- 이 실험 환경에서의 전체 16GB 메모리와 비교하면, 이정도는 완전히 수용가능한 분석 cost임

6. DISCUSSION AND FUTURE WORK

abstract domain의 선택
- strided interval인 VSA의 기본 데이터 타입은 기본적으로 수 집합의 추정치인데, 만약 변수의 value set이 불연속적이고 불규칙적인 값이라면, 예로 2,8,10 이라면, strided interval value set은 2[2, 10]이 된다.
  - 이 불가능한 값 4,6은 strided interval에 포함됨
- 그래서, power set interval domain[21], BDD-based value set domain[22], disjoint domain[23]과 같이 더 정밀한 abstract domain을 채택하면 성능 오버헤드를 addition하면서 정밀도를 향상시킬 수 있음
확장 연산자 사용
- 루프를 분석할 때, 정해진 시간 내에 수렴을 강제로하기 위해서, 확장 연산자를 사용하는 것이 일반적인 방법임
- RVSA에서, 확장 연산자는, 루프 분석의 수가 임계값에 도달했을 때 사용됨(이 실험에서 임계값은 128)
- 확장 연산자 equation(equation 8)
  - ![[Pasted image 20240121142756.png]]
  - +∞: 가능한 최대값(such as, 4바이트 unsigned integer 변수). +∞ = 232 − 1
- 그래서, 확장은 큰 부정확을 야기함.
- abstract interpretation에서의 몇 mitigation method(widening thresholds [24], abstract acceleration [25], intertwining widening and narrowing [26])이 적용될 수 있음
시스템 구현으로 생성된 정확성
- 변수 의존성 분석은 angr가 생성한 use-define chain에 의존하지만, use-define chain 생성은 pointer alias 문제를 만나면 에러를 발생시킬 수 있음
- constraint solver를 사용할 때, Z3의 타임아웃을 60s로 설정했지만, 여전히 타임아웃 될 수도 있음

A. VALUE SET ANALYSIS

2004년에 Balakrishnan et al.로 부터 제안됨.
바이너리 프로그램 정적 분석 플랫폼 CodeSurfer/x86으로 통합됨
- CodeSurfer/x86은 먼저, IDA Pro를 사용해서 바이너리 프로그램을 분석하고, 타입 복구와 indirect jump를 해결하기 위해, VSA와 Aggregate Structure Identification(ASI)를 병합함
바이너리 분석 플랫폼인 BitBlaze [28], Jakstab [29], BAP [30], angr도 VSA를 제공함

B. APPLICATION OF VSA

ByteWeight[31]
- 자동으로 학습한 key feature를 통해 함수 start 식별
- 함수 start를 식별한 후에, ByteWeight는 incremental control flow 복구 알고리즘과 VSA를 사용해서 명령어 내의 함수 바디를 찾고, 함수 바운더리를 추출함
TIE[32]
- 정적 분석 기반 타입 재구성 시스템
- 변수 복구 단계에서, TIE는 VSA를 사용해서, 메모리 내 접근 패턴을 분석함으로써 high-level 변수 위치를 추론함
BITY[33]
- pre-learned classifier를 사용해서 바이너리의 타입 예상함
- VSA를 사용해서 바이너리 코드로부터 변수를 복구하고, 변수의 관련 대표적인 명령어와 그 특징으로 다른 유용한 정보 추출
MAYHEM[34]
- 온라인 버전의 VSA 사용해서, 심볼릭 index의 bound를 resolving할 때, solver load 줄임
- VSA는 주어진 심볼릭 index에 대해 strided interval를 return함.
- strided interval은 메모리 객체의 타이트한 상한/하한을 얻기 위해 solver로부터 refine됨
GUEB[35]
- VSA를 사용해서, 추상 메모리 모델 기반으로 할당/해제 명령어 내의 각 변수를 추론해서, 바이너리 프로그램 내 use-after-free 취약점을 찾음
- 실제 취약점인 CVE-2011-4130에 대해 평가됐음(ProFTPD에 나타남)
LoongChecker[36]
- semi-simulation 접근법
- 세미 시뮬레이션 접근법 사용해서 바이너리 코드 내의 잠재적인 취약점을 확률적으로 탐지함
- 세미 시뮬레이션 접근법: VSA를 사용해서 명령어와 연관된 주소를 정확히 simulate하고, 데이터 의존성 분석을 사용해서 다른 명령어에서의 데이터 의존만 추적함
- 3개의 real world 프로그램에서 평가됐음
- 알려진 취약점 3개, 제로데이 취약점 2개 발견
GUEB와 LoongChecker 둘 다 그들의 평가에서 FP 비율 언급 안함
Balakrishnan은 VSA를 windows driver API[37]의 특정 사용 구칙을 인코딩하는 속성 automaton과 결합
- 17개 디바이스 드라비어 실행 파일의 corpus에서 평가한 결과, 5개 FP와 함께, 2개의 실제 버그 발견함
이 접근법은 논문의 conditional merging과 비슷하게, attribute automaton의 state를 사용해서 프로그램 state를 분류하지만, 이 접근법은 automaton 속성의 수동 구성이 필요함
- 논문의 접근법은 변수 의존성 분석을 통해 자동적으로 프로그램 state 분류함
Angr는 VSA의 정확성을 올리기 위해 많은 개발을 했음
- strided interval의 불연속적인 집합 생성, path predicate에 대수 solver 적용, signedness-agonostic domain 적용 등...
- 대수 solver는 lightweight이나, 많은 한계가 있음
논문에서는 추가적으로 heavyweight인 SMT solver를 적용함. 모든 경로 분기에서 SMT solver를 call하는 대신, 변수를 refine할 때 lazily하게 constraint solver를 사용함

C. CONDITIONAL STATIC ANALYSIS

일부 정적 분석 기법들은 프로그램의 state 공간을 여러 서브 공간들로 분해하고, 각각에 대한 분석을 개별적으로 수행함으로써 분석 정밀도 향상을 목표로 함
- 부분 정적 분석은 요소에 대한 부분 분석을 수행하고, 이런 부분 결과를 구성해서 전체 결과 계산함
- 조건부 정적 분석은 허용된 state들이 논리식으로 표현되는 조건 θ에 의해 설명되는 것만을 탐색
- 조건 θ는 모든 프로그램 state에 θ가 적용가능한 분석 디자인에서 결정되거나 프로그램 분석 실행 중에 결정되며, 여기서 θ는 특정 state 집합에 대해 유지되는 것을 가정 조건으로 함
Elena Sherman은 프로그램의 제어 흐름 그래프 기반의 프로그램 state 공간을 여러 파티션으로 분해하기 위한 조건 θ를 자동으로 생성하고, 각 파티션은 CFG 분기들의 집합으로 표현되는 경로들의 집합에 해당함

D. SMT SOLVER

SMT solver는 satisfiability modulo theories에 기반하고, 복잡한 공식의 satisfiability를 예측하고 해결할 수 있음
유명한 SMT solver로는 Z3 [19], MathSAT [46], CVC4 [47], Yices [48] and Boolector [49]가 있음
SMT solver는 애플리케이션에서 넓은 범위를 갖고 있음
주로 바이너리 분석 필드에서 동적 심볼릭 실행에 사용됨
- 동적 심볼릭 실행헤서 SMT solver는 두가지 주요한 업무를 담당
1. path constraint의 satisfiability 확인
2. path constraint의 해당하는 state에 도달에 사용되는 concrete한 input 값들 얻기
논문에서는, lazy constraint solving을 위한 SMT solver를 사용해서 변수의 더 타이트한 수 범위를 얻음

8. CONCLUSION

VSA 기반의 메모리 corruption 탐지 분석은 높은 FP <- VSA의 부정확성 때문
- 논문에서는 conditional merging과 lazy constraint기반의 value set refinement 접근법 제시 -> 정확성 증가

제안한 변수 의존성 분석 알고리즘을 사용해서 프로그램 경로를 여러 변수 의존성 서브그래프로 나눔
전통적인 VSA(angr-VSA) 알고리즘을 수정해서 conditional merging 지원
- conditional merging을 함으로써, 어떠한 주어진 point에서 다른 변수 의존성 서브그래프로부터 여러 state들 식별하고, 각 state에서 개별적으로 취약점 탐지
lazy constraint solving을 함으로써, 분기 조건을 추적해서 변수를 제한하고, 변수의 더 타이트한 수 범위를 얻을 수 있었음

프로토타입 시스템 RVSA 구현하고, state-of-the-art 접근법인 angr-VSA와 비교
- RVSA: 취약점 탐지 FP 비율은 12.9% 감소(angr-VSA와 비교)
RVSA는 Netgear httpd 바이너리에서 적은 FP를 보이면서 30개의 취약점 탐지
- 25개는 제로데이 취약점
결론: VSA의 정확성을 상당히 향상시켰고, 약 절반의 fP를 줄임
이 접근법이 특히 동적으로 분석하기 어려운 IoT 장비 프로그램에 효과적이고 광범위한 바이너리 프로그램 취약점 탐지 접근법이길 바람

둘기비

보안 공부하는 둘기비 입니다. 틀린 내용은 댓글로 알려주세요🐯

A Value Set Analysis Refinement Approach Based on Conditional Merging and Lazy Constraint Solving

analysis :: paper

배경지식

Numeric-analysis

Pointer-analysis

Memory corruption

제약 조건 해결 관련 개념들

Lazy constraint

Under-constraint

User cuts

Reserved space

Out-of-bounds access

Httpd

Lightweight algebraic solver

Abstract interpretation theory

Indirect jump

Loop unrolling(unwinding)

Use-Define Chain

Dispatch table

ABSTRACT

1. INTRODUCTION

Contributions

2. BACKGROUND

A. VALUE SET ANALYSIS

1) MEMORY REGION

2) VALUE SET

3) ABSTRACT STATE

B. MOTIVATING EXAMPLE

3. DESIGN

A. OVERVIEW

B. VARIABLE DEPENDENCE ANALYSIS

C. CONDITIONAL MERGING

D. LAZY CONSTRAINT SOLVING

4. IMPLEMENATATION

5. EVALUATION

A. EXPERIMENTAL SETUP

B. EFFECTIVENESS OF VULNERABILITY DETECTION

C. CONDITIONAL MERGING

CASE STUDY

D. LAZY CONSTRAINT SOLVING

CASE STUDY

E. PERFORMING OVERHEAD

6. DISCUSSION AND FUTURE WORK

7. RELATED WORK

A. VALUE SET ANALYSIS

B. APPLICATION OF VSA

C. CONDITIONAL STATIC ANALYSIS

D. SMT SOLVER

8. CONCLUSION

Sensitive Information Tracking in Commodity IoT_SAINT

Your Firmware Has Arrived: A Study of Firmware Update Vulnerabilities

0개의 댓글