⌘

[HACKING] Symbolic Execution(symbolic evaluation)을 이용한 취약점 분석

hahwul

이번 포스팅은 Symbolic Execution 정리차원으로 글 작성해봅니다. Symbolic Execution은 포통 취약점 분석에 많이 사용되는 방법 중 하나이머, 이 기법으로 굉장히 많은 노가다가 단축되어 간단한 분석에서 엄청난 효율을 자랑합니다.

Concrete Execution과 Symbolic Execution

일단 Symbolic Execution에 대해 알아보도록 하죠. 기법이기 전에 개념적으로 접근하는게 좋습니다. 이름 그대로 심볼을 이용한 실행이며 Concrete Execution과 대비되는 의미를 가지고 있습니다. 아래 2가지 코드를 비교해보겠습니다.


void concrete(int a)
{
 if(1)
 {
    return a;
 }
 else
 {
    return 0;
 }
}



void symbolic(int a)
{
 if(a > 0)
  {
    return 1;
  }
 else
  {
    return 0;
  } 
}

둘 다 분기문의 성격을 띄지만 Symbolic 함수는 인자값에 따라 분기가 틀어집니다. 이런 경우를 Symbolic Execution이라고 이야기합니다. 그래서 한쪽으로 방향이 틀어지는게 아닌 양쪽 모두 다 분기의 가능성이 있는 것이죠.

Vulnerability Symbolic Execution

취약점 분석에서도 이 개념을 사용합니다. 일단 대부분의 프로그램의 내부에는 분기문이 존재할 수 밖에 없습니다. (진리의 if) 이 분기문을 통해 입력에 따른 다른 출력을 보여줄 수 있지요. Symbolic Execution, 즉 반복적인 시뮬레이션을 통해 여러개의 분기를 타면서 프로그램의 흐름을 분석합니다.

이 흐름들에는 분명히 중요한 정보를 담고 있거나 아직 발견되는 않은 취약점이 있는 길로 넘어갈 수 있는 정보들을 가지고 있지요.

여기서 여러 분기로 넘어갈 수 있는 조건식을 Path Condition이라고 부릅니다. 위에 symbolic() 함수 코드를 예시로 든다면 a로 분기를 태울 수 있는 값들의 집합이되겠죠. 아마도 1 이상의 값들과 나머지 값, 이렇게 2가지로 나타낼 수 있겠죠.

물론 사람이 분석할때에도 Symbolic Execution 으로 분석하게 됩니다. 왜냐하면.. 우리도 안가본 미지의 영역이 궁금하고 거기서 얻어낼 수 있는게 많기 때문이죠. 이 과정은 매우 노가다이며 많은 테스팅이 필요합니다. 이를 소프트웨어로 극복하는거죠. 사실 이 개념은 해킹뿐만 아니라 소프트웨어 테스팅, 과학 등 여러가지 분야에 사용됩니다.

SMT Solver

Symbolic Execution을 쉽게 하기 위해선 자동화된 툴이 필요합니다. 많은 테스트를 하기 위해선 Path condition을 만들어주는 프로그램이 필요하죠. 이 Path Condition을 만들어주는 툴을 우리는 SMT Solver라고 부릅니다. 대표적으로 z3, yices 등 여러가지가 있습니다.

SMT Solver는 원래 연립식을 풀기 위한 프로그램입니다. z3로 대충 내용을 보면..


import z3
x = Int('x')
y = Int('y')
solve(x*y>50,x>5)

이런식으로 값을 주면.. 결과가 나타납니다. y의 값을 바로 찾을 수 있지요.

이 개념을 취약점 분석에도 적용할 수 있습니다. 물론 선구자들이 미리 만들어놓은 툴을 사용하는 것도 좋고 직접 구현해보시는 것도 좋을 것 같습니다.

angr python library

angr은 shellphish 팀에서 개발한 symbolic execution 툴입니다. 이 프로그램은 바이너리 파일에서 분석가가 입력한 특정 지짐을 찾은 후 마지막에 사용된 함수와 그 데이터를 보여줍니다. (http://angr.io/)

#> pip install angr

or

#> git clone https://github.com/angr/angr.git #> cd angr #> python setup.py install


#include <stdio.h>

void main(int argc, char* argv[])
{

    if(argv == 1)
    {

        printf("Error");
        exit(1);
    }
    if(argv[1] == 5564)
    {
        printf("yes");
    }
    else
    {
        printf("no");
    }
}

#> gcc -o test test.c test.c: In function ‘main’: test.c:6:10: warning: comparison between pointer and integer if(argv == 1) ^~ test.c:10:3: warning: implicit declaration of function ‘exit’ [-Wimplicit-function-declaration] exit(1); ^~~~ test.c:10:3: warning: incompatible implicit declaration of built-in function ‘exit’ test.c:10:3: note: include ‘’ or provide a declaration of ‘exit’ test.c:12:13: warning: comparison between pointer and integer if(argv[1] == 5564) ^~

#> ./test 1 no


import angr

proj = angr.Project('./test', load_options={'auto_load_libs':False}) # load binary
path_group = proj.factory.path_group(threads=4) # set thread and path
path_group.explore(find=0x40054, avoid=0x40065) # find & avoid
                                                                                                    # 여기서 find 값은 찾을 값 / avoid는 피할 값이겠죠.
print path_group.found[0].state.posix.dumps(1) # print dump

추가로.. PC 여러대에서 테스트하다 보니 동작안하던 이슈가 있었습니다.

ImportError: cannot import name operations

python 관련 프로그램들이 많다보니.. 약간 의존성 문제가 있는 것 같았습니다. angr 개발팀에 물어보니.. 아래와 같이 답을주어서

virtualenv로 쉽게 해결되었습니다. 추후에 virtualenv도 한번 포스팅하면 좋을 것 같네요.

#> pip install virtualenv #> angr/v_env/bin/python setup.py install

해당 virtualenv 경로의 python으로 실행 시 잘 실행됩니다.

Symbolic Execution

이 방법은 대표적으로 binary 분석에서 이야기됩니다. 다만 웹에서도 어느정도 적용할 수 있겠다는 생각이 드네요. 프로그램을 통해 DOM 영역과 JS 코드단에선 분명히 분기를 이용해서 넘나들 수 있고 그렇단 소리는.. 이런 분석 방식을 통해서 자동화된 테스트를 해볼 수 있단 것이 매력적으로 다가오네요.

Reference

https://en.wikipedia.org/wiki/Symbolic_execution http://ericpony.github.io/z3py-tutorial/guide-examples.htm http://secuinside.com/archive/2016/2016-2-6.pdf

#security