SymCC Fuzzing - 1 ( Symbolic executor )

오늘 포스팅 주제는 Hybrid Fuzzing에서 SymCC라는 툴입니다.

원래는 Driller를 주제로 포스팅하려고 했는데, Driller가 좀 오래된 툴이다 보니 의존성 문제도 좀 있고, 환경 구성하는것도 너무 쉽지 않더라고요. 또 최근에 Driller의 단점들을 보완한 툴들이 있기 때문에 최신 툴인 SymCC를 가져와서 포스팅하게 되었습니다.

 

Driller부터 시작한 hybrid fuzzer의 개발 과정이 있는데 간단하게만 살펴보겠습니다.

 

Driller : 최초의 하이브리드 퍼저로 AFL + Angr의 형태입니다. 구현 원리가 비교적 직관적이지만, 파이썬 기반의 Angr을 구동하는 오버헤드가 크고, 의존성 문제가 발생하여 설치가 어렵습니다.

 

이러한 오버헤드 문제와 속도 문제를 해결하기 위해 2018년에 나온 툴은 QSYM입니다.

 

QYSM : 분석 엔진을 파이썬 대신 C++로 만들었습니다. AFL + QYSM의 형태이고, AFL이 멈출 때 까지 기다렸다 심볼렉 엔진을 쓰는게 아니라 동시에 같이 돌아갑니다. Dynamic Binary Translation이라는 기술을 써서 프로그램 시작과 동시에 분석을 수행해 Angr보다 약 10배정도 빠릅니다. 설치 환경 의존성 문제가 존재하지만 바이너리 없어도 분석이 가능하다는 장점이 있습니다.

 

그 후로, 속도를 조금 더 올리기 위해 2020년 SymCC라는 툴이 나왔습니다.

 

SymCC : 실행 중 분석이 아닌 컴파일 할 때 심볼릭 코드를 프로그램 안에 심어서 컴파일 합니다. 따라서 실행 실행시 별도의 가상머신(QEMU)나 분석기가 필요하지 않고, 순수 바이너리 실행 속도에 가까운 퍼포먼스를 냅니다. 압도적인 퍼징 속도를 가지고 있고, AFL++라는 최신 퍼징 툴에 호환성이 좋으나, 컴파일이 필요하므로 소스코드가 있을 때만 성능이 나옵니다.

 

가장 최신으로는 LibAFL이라는 Rust 기반의 모듈형 프레임워크가 존재해 원하는 퍼저를 커스터마이징 가능한 툴이 있고, 또 AI를 활용하여 symbolic engine을 ai로 대체하는 툴도 연구되고 있습니다. 뒤에 서술한 AI를 활용한 symbolic engine은 나중에 또 깊게 공부를 해볼 생각입니다.

 

오늘은 SymCC에 대해서만 실습을 진행해보고, 하이브리드 퍼저에 대한 전반적인 공부를 해보겠습니다.

 

SymCC 설치

SymCC는 공식 이미지를 제공하지 않지만, 연구자들이 만들어둔 안정적인 이미지가 있습니다.

도커파일을 새로 생성해서 만들어주겠습니다.

# 1. SymCC 저장소 복제
git clone https://github.com/eurecom-s3/symcc.git
cd symcc

# 2. Docker 이미지 빌드
docker build -t symcc-lab .

 

설치하는덴 한 10분~ 정도 걸린 것 같습니다.

설치는 완료 됐고, 이제 퍼징을 돌릴 바이너리를 만들겠습니다.

//target.c
#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>

int main(void) {
    int a, b;
    // 8바이트(정수 2개)를 입력받음
    if (read(0, &a, 4) < 1) return 0;
    if (read(0, &b, 4) < 1) return 0;

    // a + b가 정확히 0x12345678 (305419896)이 되어야 함
    if (a + b == 0x12345678) {
        printf("CRASH!!\n");
        abort(); 
    }
    return 0;
}

 

a + b의 산술 연산과 magic number 연산이 필요한 간단한 코드입니다.

해당 코드를 컴파일 해주는데 gcc 대신 symcc라는 컴파일러를 써서 심볼릭 변수를 넣어주겠습니다.

처음에 이런 에러코드가 나왔는데 SymCC 실행 스크립트에서 사용하려는 Clang버전은 12버전인데 실제 컨테이너 안에 설치된 버전은 달라서 그렇습니다.

위의 명령어로 libm의 버전을 확인해준 뒤

export SYMCC_CLANG=/usr/lib/llvm-14/bin/clang
export SYMCC_CLANG_PLUS_PLUS=/usr/lib/llvm-14/bin/clang++

해당 명령어로 환경변수를 변경해줍니다.

 

이제 컴파일을 마저 해준 뒤, 심볼이 잘 박혔는지 확인해보겠습니다.

nm target

_sym으로 들어가있는 심볼들이 보이는데, 이건 SymCC가 프로그램 안에 심어놓은 것으로, sym_build_add는 더하기 연산,  _sym_build_equal은 똑같은지 비교하는 연산 등의 도구들입니다.

 

이제 실행시켜보겠습니다.

SYMCC_OUTPUT_DIR=/tmp/symcc_out ./target < seed

위의 명령어로 실행을 해줬고, 저는 환경변수 설정에 계속 문제가 생겨서 SYMCC_OUTPUT 을 통해 환경변수로 출력위치를 설정해뒀습니다.

다음과 같이 실행이 됐습니다.

symcc_out에 생긴 파일들을 확인해보겠습니다.

000000이라는 파일이 생성됐습니다.

xV4라는 글자가 출력되는데, 이건 SymCC가 저장한 정답이 글자가 아니라 바이너리 데이터이기 때문입니다.

덤프를 떠서 보겠습니다, hexdump가 안깔려있어 od로 확인해보겠습니다.

12 34 56 78이 리틀엔디언으로 박혀있습니다.

해당 값들을 아까 만들었던 target으로 직접 넣어보겠습니다.

정상적으로 abort함수를 찾아내는 모습입니다.

조금 더 어려운 바이너리랑 어려운 문제로 테스트를 해보고 싶은데, 제가 지금 노트북으로 보고 있어서, 나중에 본체로 여태까지 깔아둔 툴들로 리버싱 CTF 문제를 풀어보는 포스팅을 작성해보겠습니다.

근데 SymCC는 화려한 로그가 없고 바로 파일로 저장되니 뭔가 잘 되고 있는지 잘 몰겠네요. 다른 툴들과 비교를 해보고 싶은데, 환경구성이 쉽지 않아 일단 target을 조금 더 어렵게 해보겠습니다.

 

코드 설계는 complex_loop을 통해 angr로 풀 때 경로 폭발이 발생하도록 하였고, 루프를 조금 더 복잡하게 하여서 일반 퍼저로도 풀 수 없도록 만들었습니다.

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

void complex_loop(unsigned int *val, int iterations) {
    // 경로 폭발 유도: 반복문 내부에 조건부 연산을 넣어 
    // 정적 분석 도구가 탐색해야 할 경로를 기하급수적으로 늘림
    for (int i = 0; i < iterations; i++) {
        if ((*val) % 2 == 0) {
            *val = (*val >> 1) + 0x1337;
        } else {
            *val = (*val * 3) + 1;
        }
    }
}

int main() {
    unsigned int magic1, magic2;
    char buf[16];

    // 1단계: 4바이트 읽기 (Magic Value)
    if (read(0, &magic1, 4) < 4) return 0;
    
    // magic value check로 fuzzer의 연산을 방해
    if (magic1 == 0xdeadbeef) {
        printf("[1단계 통과]\n");

        // 2단계: 경로 폭발 구간
        if (read(0, &magic2, 4) < 4) return 0;
        unsigned int temp = magic2;
        // complex_loop로 경로폭발 유도
        complex_loop(&temp, 100); 

        // 루프를 돌고 난 결과값이 특정값이어야 함 (역산이 매우 힘듦)
        if (temp == 0x12345678) {
            printf("[2단계 통과]!\n");

            // 3단계: 문자열 비교
            if (read(0, buf, 4) < 4) return 0;
            if (memcmp(buf, "HACK", 4) == 0) {
                printf("[최종 성공]\n");
                abort();
            }
        }
    }
    return 0;
}

 

 

컴파일도 마저 해주고, 시드값도 맞춰 넣어주었습니다.

여기서 Seed값을 맞춰서 넣어주면 좋지만, 조금 더 성능을 확인하기 위해 시드를 A*20으로 넣었습니다.

 

결과를 확인해보겠습니다.



ㄽ?라는 문자열이 들어가 있고, 바이너리상 ef be ad de입니다.

이게 1단계 통과하는 코드이고, deadbeef입니다.

이제 2번째 단계를 통과해야되는데, deadbeef라는 입력을 기반으로 시드를 수정해줘야된다고 하네요.

 

일단 근데 반복문의 횟수를 100회로 했더니, 푸는데 너무 오래걸리고 로그가 너무 많더라고요. 그래서 일단 10회로 줄였습니다.

시드값도 deadbeef를 넣어줬습니다.

실행하면 위와같이 4개의 파일이 생성됩니다.

그 중 마지막으로 생성된 파일을 ./target의 입력값으로 넣어주겠습니다.

2단계까지 통과했습니다.

output/000004를 확인해보니 ㄽ?에 추가로 문자가 들어있더군요

내용을 읽어보니 2d 1b 7a bd가 추가되어있습니다.

이제 해당 내용을 seed값에 추가해주고 다시 마지막으로 돌려보겠습니다.

cat /tmp/output/000004 > seed_final
python3 -c 'print("A"*10)' >> seed_final

결과를 보면 최종 성공이 찍혀있습니다.

결과물을 출력해보면

이렇게 뒤에 HACK이라는 글자가 붙은걸 화인 가능합니다.

 

이렇게 해서 SymCC라는 하이브리드 퍼징 툴을 한번 사용해봤습니다.

아직 자동화하기 전 단계라 그런지 상당히 불편하고 번거로운 과정이 많다고 느껴졌습니다.

그리고 이게 symbolic execution을 사용중인건지, 좀 체감이 안되는 부분들이 있네요

 

그리고 다 하고 너무 답답해서 더 찾아보다 알게된건데, 지금까지 한건 하이브리드 퍼징이 아닌 그냥 Symbolic execution이었다고 하네요 ..

하이브리드 퍼징을 하려면 SymCC에 AFL같은 퍼저를 붙여서 AFL로 돌리다 안되는 부분을 SymCC로 푸는 구조를 만들었어야 된다고 합니다....

그래서 일단 포스팅 편수를 좀 나눠서 다음 포스팅에서 AFL을 붙여서 진짜 하이브리드 퍼징을 시도해보도록 하겠습니다.

진짜 하이브리드로 하려면 터미널 두개로 돌려야된다는데,, 다시 연구실로 가서 세팅을 하고 돌려봐야겠네요 ㅠ

읽어주셔서 감사합니다 ..