[하드웨어 해킹] 퍼징과 분석 기술 - 심볼릭 실행

퍼징

퍼징(fuzzing)은 가장 효과적으로 소프트웨어를 테스트하는 기술이다.

정의에 따르면 퍼징은 실행 중인 소프트웨어뿐 아니라 소스코드와 컴파일된 코드에도 적용할 수 있다. 하지만 실행 중인 프로그램이 아니라면 정적 분석의 영역이라고 봐야할 것이다.

 

퍼징과 동적 분석, 정적 분석을 합쳐 concolic testing이라고 할 수 있다. concolic은 concrete와 symbolic을 합친 말로, symbolic한 실행과 concrete 실행을 함께 사용하는 기술을 말한다. 다시 말해 주어진 소스코드를 기반으로 높은 커버리지를 달성하는 테스트 케이스를 자동으로 생성하는 테스팅 기법이다.

프로그램 시맨틱을 해석하는 법

프로그램 시맨틱(semantic)은 어떤 요소를 어떠한 위치에 두면 어떤 의미를 갖는지를 말한다.
프로토콜 설계 단계에서 상태 머신(state machine)은 코드를 작성하기 전 필수 단계로 복잡한 소프트웨어를 형식화하는 데 매우 유용하다.

보안 연구원으로서 본능적으로 이러한 다이어그램을 찾아봐야 한다. GSM 프로토콜의 오토마타(automata)를 분석해보자.

GSM call setup은 다음과 같다.

 

SETUP

1. RR connection establishment
2. Service request
3. Authentication
4. Ciphering mode setting
5. IMEI check

ASSIGNMENT

   6. TMSI-reallocation

CONNECT

   7. Call initiation

   8. Assignment of a traffic channel

   9. User alerting

SPEAK

   10. Call accepted

 

 

이전 상태 합성에는 기지국과 두 개의 종단점이 포함된다. 세 노드는 여러 메시지 교환을 포함하고, 메시지 처리 장치에는 고정 길이 또는 가변 길이 메시지 필드가 있을 수 있다. 프로토콜 명세서에서 바로 이해할 수 있는 것처럼, 버퍼 크기가 실제로 전송되어 일부 공간이 과도하게 할당되거나 버퍼가 손상되는 사례가 있다. 삼성 모바일 장치에서 베이스밴드 구성 요소에 비정상적인 setup 메시지를 통한 버퍼 오버플로가 발생한 CVE-2020-25279가 그 예시이다.

 

위 취약점은 퍼징과 에뮬레이션을 통해 발견했다. 이 이벤트는 엄청난 인내가 필요한 정적 연구가 최고라고 여겼던 보안 연구자에게 새로운 지평을 열었다.

심볼릭 실행(symbolic execution)

심볼릭 실행은 대상 프로그램을 실행할 때 구체적인 값(concrete value) 대신 기호로 표현된 값(symbolic value)를 사용한다. 코드 커버리지와 임의 실행 조건을 향상시킬 수 있다. 심볼릭 실행은 검색 공간을 줄이고 분석 속도를 높인다.

심볼릭 실행을 살펴보기 위해 다음 코드를 살펴보자.

#include <stdio.h>
#include <stdlib.h>

int main (int argc, char**argv) 
{ 
    int a = atoi(argv[1]); 
    int b = atoi(argv[2]); 

    if (a % b == 0)   
        printf("Your numbers are multiples\n"); 
    else 
        printf("Your numbers are not multiples\n");

    return 0; 
}

 

이 때 0은 올바른 입력값인가? 그렇다면, 어떤 변수에 대해서 옳은 값인가?

atoi가 호출된 후 변수가 어디에 저장되는지 알아야 한다. 문자열이 정수로 변환되면 레지스터에 저장될 것이다. 이 레지스터를 기호화(symbolize)해 모든 명령을 심볼릭 값(symbolic value)에 적용해야 한다. 이 명령이 SMT solver에 넣을 심볼릭 표현(expression)을 생성하고, solver는 한 경로 또는 다른 경로의 솔루션을 제공할 것이다.

 

해당 코드를 컴파일하고 ghidra로 분석을 실행하면 다음과 같은 위치에서 화면이 시작된다.

 

 

_start 함수는 libc로부터 _libc_start_main 함수를 호출한다. 함수 매개변수는 호출 전에 레지스터에서 전달되고, 호출 규칙(calling convention)에 따라 역순으로 전달되므로 LEA 명령어가 포함된 마지막 줄은 main 함수의 주소를 RDI 레지스터에 넣는다.

위의 대괄호 속에 있는 붉은 main을 더블 클릭하면 main 함수로 넘어갈 수 있다.

 

 

undefined main()을 클릭해 커서를 두고, F를 눌러 편집(edit) 창을 연다.

 

 

이를 아래와 같이 수정한다.

 

그러면 00101175의 EDI와 00101178의 RSI가 argc와 argv로 바뀐다.

 

 

이와 함께 함수는 변수에 접근할 복사본을 로컬 스토리지에 가지고, 이 레지스터들은 다른 함수의 인자(parameter)로 사용될 것이다.

 

main 함수의 프롤로그(prologue) 다음에 argv[1]과 argv[2]를 받고 atoi 함수에 넘기는 코드가 있다. atoi가 호출되면 문자열이 정수로 변환되고, 어떻게 EAX에 있는 값이 local_10, local_c라는 변수에 저장되는지 볼 수 있을 것이다.

 

ghidra의 명명 정책(naming convention)에 따라 local_10과 local_28은 RBP에서의 오프셋이 아니다.

gdb로 컴파일된 실행 파일을 실행하고, disas main을 입력해 디스어셈블해보면 0x8과 0x4에 저장된다. 이 스택으로부터의 오프셋이 atoi를 통해 변환된 정수가 저장되는 곳이다.

 

 

나눗셈의 나머지도 확인해보자. 0x001011ac가 나눗셈(IDIV)을 시행하는 단계다. 연산 후 나머지는 EDX에서 가져와진다. TEST 명령으로 체크하고, 프로그램은 나머지가 0이 아닌지 확인한 후 점프(JNZ, jump if not zero)한다. 점프 위치는 0x001011c6으로, "Your numbers are not multiples"가 출력될 것이다. 그렇지 않다면 "Your numbers are multiples"가 출력될 것이다.

 

 

이 부분은 atoi에 대한 호출을 피하면서 심볼릭하게 실행한다. 숫자가 저장된 주소를 기호화하고, 첫 번째 점프에 도달하면 조건을 기호식으로 추출하고 Z3 solver를 사용한다.

 

이제 심볼릭 실행을 적용한 코드를 보자.

https://github.com/PacktPublishing/Fuzzing-Against-the-Machine/blob/main/Chapter_4/symbolic_execution.py 에서 받을 수 있다.

이 파일을 실행하기 위해 다음 명령을 통해 패키지를 설치해야 한다.

 

python3 -m pip install pymaat

 

설치 후 파일을 실행한다.

 

python3 symbolic_execution.py

 

solver가 두 모델을 찾았다.하나는 프로그램이 가지(branch)를 가지게 하고, 다른 모델은 프로그램이 가지를 가지지 못하게 한다. arg1 = 0, arg2 = 0이라는 결과를 피하려면 제약 조건이 있어야 한다.

 

DSE(Dynamic Symbolic Execution)은 메모리를 흡수(drain)하므로 확장성이 없다. 두 경로를 모두 따라가면 경로 폭발(path explosion)이 바생할 수 있다. 이를 피하기 위해 colcolic execution이 사용되는데, 레지스터 또는 메모리에 전체 심볼릭 값을 주는 대신 값은 주어지지만 표현식(expression)을 심볼릭 값으로 사용한다.

 

심볼릭 실행은 가능한 한 많은 경로를 탐색해 퍼징의 커버리지를 높이고 코드의 잠재적 취약점을 찾아낼 수 있지만 항상 최고의 방법은 아니다.

참고자료

Antonio Nappa , Eduardo Blázquez - Fuzzing Against the Machine

Concolic Testing(https://testing-nick9.tistory.com/5)
프로그래밍 언어에서 말하는 의미론 (Semantics, 시멘틱) 이란?(https://jake-seo-dev.tistory.com/445)
기호 실행 원리(https://rond-o.tistory.com/311)