Ponce(2016, IDA Plugin) - symbolic execution

출처 : https://github.com/illera88/Ponce

Ponce IDA Plug-in(2016)

Ponce는 2016 IDA Plug-in Contest에서 1등을 차지한 프로그램이다.

이 플러그인에 대해 차근차근 알아보자.

Definition

Ponce는 바이너리 기반의 직관적인 taint analysis 및 symbolic execution을 수행하는 기능을 제공하는 IDA Pro 플러그인이다. 

Ponce를 사용하면 클릭 한 번을 통해 최신 symbolic execution 기능을 모두 사용할 수 있다. 전체 코드는 C/C++로 작성되었다.

Why?

Symbolic execution은 새로운 컨셉의 보안 개념은 아니다. 이미 몇 년 전부터 Triton이나 Angr과 같은 오픈소스 프로젝트로 이러한 개념의 필요성이 대두되었다. 그럼에도 불구하고, 이러한 프로젝트를 활용하기 위해서는 end users가 세부 유스케이스를 스스로 구현해야 한다.

우리는 IDA 플러그인 형태의 Ponce를 제작하고 발표함으로써 symbolic execution과 tatint analysis를 디스어셈블러/디버거 내에서 리버스 엔지니어들이 활용할 수 있도록 구현했다.

Installation

Ponce는 IDA 6.8 및 IDA 6.9x에서 x86 및 x64 바이너리 기반으로 동작한다. 플러그인을 설치하기 위해서 적절한 파일을 IDA가 설치된 디렉토리의 plugin\ 폴더에 복사하면 된다.

OS Support

Ponce는 윈도우 및 Linux, OSX에서 기본적으로 동작한다!

Use Modes

- Tainting engine: Tainting engine은 사용자의 입력(메모리와 레지스터)에 의해 제어 가능한 모든 바이너리 실행 단계를 결정하는데 사용된다.

- Symbolic engine: Symbolic engine은 메모리와 레지스터 영역을 심볼릭 상태로 유지하여 바이너리의 실행 경로를 탐색하는데 사용된다.

Examples 1

crackMe를 해결하기 위한 심볼릭 수행 사용

심볼릭 엔진의 사용과 제약조건 해결자를 사용하는 방법은 다음과 같다:

- 단순한 aaaaa 와 같은 인자를 전달한다.

- 먼저 심볼릭 엔진을 선택한다.

- argv1이 가리키는 메모리를 심볼릭으로 변환한다.

- 문제를 해결할 수 있는 심볼릭 조건을 확인한다.

- 솔루션을 테스트한다.

다음은 테스팅에 사용할 crackme_hash.cpp의 소스코드다.

#include <stdio.h>
#include <stdlib.h>
 
char *serial = "\x31\x3e\x3d\x26\x31";
 
int check(char *ptr)
{
    int i;
    int hash = 0xABCD;
 
    for (i = 0; ptr[i]; i++)
        hash += ptr[i] ^ serial[i % 5];
 
    return hash;
}
 
int main(int ac, char **av)
{
    int ret;
 
    if (ac != 2)
        return -1;
 
    ret = check(av[1]);
    if (ret == 0xad6d)
        printf("Win\n");
    else
        printf("fail\n");
 
    return 0;
}

먼저 동적 디버깅을 위해 'aaaaa' 파라미터를 전달(Debugger -> Process Options)한다.

앞에서 언급한 것처럼 Ponce는 Symbolic과 Taint 두 개의 엔진을 가지고 있는데, crackme를 해결하기 위한 파라미터를 얻는 것이 목적이므로 Ponce Configuration에서 심볼릭 엔진을 선택한다.

동적 디버깅 상태에서 파라미터가 위치하는 메모리 영역을 심볼릭 설정하고, 실행하면 연두색과 초록색으로 Tainted Instruction 및 Tainted Condition 영역이 마킹된다.

제약조건 해결자(Constraint solver)를 이용해 Tainted Condition에서 실행되지 않은 Instruction 영역('win' 문자열이 출력되는 블록)에 도달하는 솔루션을 획득해보자. 해당 영역에서 우클릭을 하면 SMT Solver를 선택할 수 있다.

실행하면, 다음과 같은 결과를 얻을 수 있다.

[+] Solving condition at 7
[+] Solving formula...
[+] Solution found! Values:
 - SymVar_0 (argc):0x000002
 - SymVar_1 (argv[1][0]):0x53 (S)
 - SymVar_2 (argv[1][1]):0x58 (X)
 - SymVar_3 (argv[1][2]):0x37 (7)
 - SymVar_4 (argv[1][3]):0x40 (@)
 - SymVar_5 (argv[1][4]):0x59 (Y)
 - SymVar_6 (argv[1][5]):00 ( )

즉, 'SX7@Y' 문자열이 'win'이 존재하는 블록에 도달할 수 있는 솔루션이다.

최고의 디스어셈블러인 IDA에서 Symbolic execution과 Taint Analysis 기술을 바로 적용시킬 수 있다는 점이 정말 마음에 든다!