"Software Vulnerability"의 두 판 사이의 차이

Cslab
이동: 둘러보기, 검색
 
(같은 사용자의 중간 판 14개는 보이지 않습니다)
1번째 줄: 1번째 줄:
'''Symbolic Execution'''
+
== '''BOF (Buffer OverFlow)''' ==
 +
 
 +
 
 +
버퍼 오버플로(buffer overflow) 또는 버퍼 오버런(buffer overrun)은 메모리를 다루는 데에 오류가 발생하여 잘못된 동작을 하는 프로그램 취약점이다. 컴퓨터 보안과 프로그래밍에서 이는 프로세스가 데이터를 버퍼에 저장할 때 프로그래머가 지정한 곳 바깥에 저장하는 것이다. 벗어난 데이터는 인접 메모리를 덮어 쓰게 되는데 다른 데이터가 포함되어 있을 수도 있는데, 손상을 받을 수 있는 데이터는 프로그램 변수와 프로그램 흐름 제어 데이터도 포함된다. 이로 인해 잘못된 프로그램 거동이 나타날 수 있으며, 메모리 접근 오류, 잘못된 결과, 프로그램 종료, 또는 시스템 보안 누설이 발생할 수 있다.
 +
 
 +
버퍼 오버플로가 코드를 실행시키도록 설계되거나 프로그램 작동을 변경시키도록 설계된 입력에 의해 촉발될 수 있다. 따라서 이는 많은 소프트웨어 취약점의 근간이 되며 악의적으로 이용될 수 있다. 경계 검사로 버퍼 오버플로를 방지할 수 있다.
 +
 
 +
버퍼 오버플로는 보통 데이터를 저장하는 과정에서 그 데이터를 저장할 메모리 위치가 유효한지를 검사하지 않아 발생한다. 이러한 경우 데이터가 담긴 위치 근처에 있는 값이 손상되고 그 손상이 프로그램 실행에 영향을 미칠 수도 있다. 특히, 악의적인 공격으로 인해 프로그램에 취약점이 발생할 수도 있다.
 +
 
 +
흔히 버퍼 오버플로와 관련되는 프로그래밍 언어는 C와 C++로, 어떤 영역의 메모리에서도 내장된 데이터 접근 또는 덮어쓰기 보호 기능을 제공하지 않으며 어떤 배열에 기록되는 데이터가 그 배열의 범위 안에 포함되는지 자동으로 검사하지 않는다.
 +
 
 +
<출처 : http://ko.wikipedia.org/wiki/%EB%B2%84%ED%8D%BC_%EC%98%A4%EB%B2%84%ED%94%8C%EB%A1%9C>
 +
 
 +
Stack은 메모리 구조의 일부분이다. Stack은 보통 FILO(first in last out)혹은 LIFO(last in first out)이라고 불리운다. 나중에 입력된 값이 먼저 호출되는 방식이다
 +
 
 +
[[파일:Bof1.jpg | center]]
 +
 
 +
Stack segment는 지역 변수와 프로시저 호출, data segment는 정적변수와 동적변수를, text segment는 프로그램 명령어를 저장한다. Stack를 악용하는 형태가 스택 오버플로우이다. 다음 그림과 같은 코드가 존재할 때 스택에 RET,SFP가 생기고 그 위에 코드의 정보가 쌓이게 된다.
 +
 
 +
[[파일:Bof2.jpg | center]]
 +
 
 +
RET는 return address라 불리기도 하는데 프로그램 실행도중 반복문이나 함수를 호출하여 그 부분이 실행되고 난 후 복귀를 하기 위하여 정해놓은 주소값이다. 즉 실행되었던 함수가 종료를 하고 원래 코드의 나머지 부분을 실행하기 위하여 돌아올곳을 알기위해서 기억하는 주소이다.(=EIP)Sfp는 스택 포인터라고 불리기도 한다. 스택은 유동적이기 때문에 일정한 기준점(EBP)를 만들고 EBP를 기점으로 찾고자 하는 data의 위치를 주소 값으로 찾기 위하여 필요하다. 다음 그림과 같은 코드가 존재할 때 스택에 RET,SFP가 생기고 그 위에 코드의 정보가 쌓이게 된다.
 +
 
 +
[[파일:Bof3.jpg | center]]
 +
 
 +
스택 버퍼플로우의 원리는 주어진 버퍼의 용량을  초과하는 값을 넣어 EIP까지 덮어씌우게 만들어서 EIP의 주소를 알아내어 임의의 영역으로 점프 뛰게 만들어 자신의 shellcode를 실행시키는 것이다.
 +
 
 +
(1) 스택 오버플로우 예제
 +
오버플로우를 일으키기 위해 Perl script로 다음과 같은 파일을 만든다. 버퍼에 “A”를 가득 메우는 코드이다. 프로그램을 실행시켜 방금 만든 코드의 결과를 불러온다. 20000byte의 문자열을 입력하였지만 오버플로우가 일어나지 않았다.
 +
 
 +
my $file = “crash.m3u”;
 +
my $junk = “A” * 20000;
 +
open($FILE, “>$file”);
 +
print $FILE $junk;
 +
close($FILE);
 +
 
 +
[[파일:Bof4.jpg | center]]
 +
 
 +
코드를 고쳐 30000byte의 문자를 입력하여 보면 오버플로우가 발생하여 프로그램이 죽는 현상을 볼 수 있다. 오버플로우가 발생한 것이다.
 +
 
 +
my $file = “crash.m3u”;
 +
my $junk = “A” * 30000;
 +
open($FILE, “>$file”);
 +
print $FILE $junk;
 +
close($FILE);
 +
 
 +
[[파일:Bof5.jpg | center]]
 +
 
 +
 
 +
Windbg를 이용하여 버퍼오버플로우가 발생한 상태를 확인해보자. EIP가 0x41(A)로 채워진 것을 볼 수 있다. 다음 할 일은 EIP를 덮어쓰기 위하여 Buffer 사이즈를 알아낼 필요가 있다.
 +
 
 +
[[파일:Bof6.jpg | center]]
 +
 
 +
다음과 같이 A를 25000으로 변경하고 B를 5000개로 변경한 후 다시 프로그램을 실행시킨다. 오버플로우가 발생하며 Windbg로 EIP가 “42”로 채워져 있으면 있다는 것을 알 수 있다. 즉 EIP는 25000~30000사이에 존재한다는 것을 알 수 있다.
 +
 
 +
ESP, 즉 스택에도 “B”로 채워진 것을 알 수 있다.
 +
 
 +
[[파일:Bof7.jpg | center]]
 +
 
 +
정확한 buffer크기를 알기위하여 metasploit을 실행하여 다음 그림에서와 같이 패턴을 생성한 후 만들어진 패턴을 Perl 코드의 junk2에 복사 해 넣는다.
 +
 
 +
[[파일:Bof8.jpg | center]]
 +
 
 +
my $file = “crash.m3u”;
 +
my $junk = “A” * 25000;
 +
my $junk2 = “pattern”
 +
open($FILE, “>$file”);
 +
print $FILE $junk.$junk2;
 +
close($FILE);
 +
 
 +
 
 +
EIP에 다음과 같이 저장된 것을 볼 수 있고 metasploitl에서 다음과 같이 실행한다. 2787이 리턴주소를 덮어쓰기 위한 사이즈인 것을 알 수 있다. 그러므로 25000+1062 이후가 리턴 주소란 것을 짐작 할 수 있다.
 +
 
 +
[[파일:Bof9.jpg | center]]
 +
<br />
 +
[[파일:Bof10.jpg | center]]
 +
 
 +
$junk의 크기를 재수정한 후 $eip를 BBBB로 채운 후 $esp에 “C”로 채워 본다. 해당 결과를 입력으로 타켓 프로그램을 실행하면 Windbg에서 EIP에 0x42424242와 ESP에 0x43으로 채워져 있는 것을 확인할 수 있다.
 +
 
 +
[[파일:Bof11.jpg | center]]
 +
<br />
 +
[[파일:Bof12.jpg | center]]
 +
 
 +
Shellcode를 삽입하기 위해서 ESP(stack pointer)의 주소도 알아야한다. 다음과 같이 perl코드를 변경하여 테스트하여 본다. 타켓 프로그램을 실행해서 Windbg를 확인하면 ESP의 첫주소를 알 수 있다. 이로써 EIP에 원하는 코드의 주소를 넣을 수 있고 (control flow hijacking), ESP에 Shellcode를 넣을 수 있다.
 +
 
 +
[[파일:Bof13.jpg | center]]
 +
<br />
 +
[[파일:Bof14.jpg | center]]
 +
 
 +
EIP의 값 조작을 통해 (Control flow hijacking) 스택에 있는 쉘코드를 실행하여야 한다. 하지만 쉘코드가 저장된 스택을 바로 호출 할 수 없기 때문에 “jump esp” 코드를 이용하여 스택에 저장된 코드를 실행한다.
 +
 
 +
윈도우 프로그램은 하나이상의 DLL파일을 사용하고 이 DLL파일에는 많은 코드 지시자들이 있고 주소도 대부분 정적이다. 그러므로 ESP로 점프하는 DLL파일의 코드를 찾아 EIP에 이 주소를 써주면 ESP로 점프할 것이다. 그러기 위해선 jmp esp의 opcode를 알아야한다. 타겟 프로그램을 불러들인 후 다음과 같이 기입한다. 그 후 ‘U’로 확인해본다. Opcode는 ffe4이다.
 +
 
 +
[[파일:Bof15.jpg | center]]
 +
<br />
 +
[[파일:Bof16.jpg | center]]
 +
 
 +
적당한 DLL을 찾기 위해 windbg에서 Debug->Modules를 선택한다. 타겟 프로그램의 DLL파일의 주소에서 ff e4(jmp esp)코드를 찾는다.
 +
 
 +
[[파일:Bof17.jpg | center]]
 +
<br />
 +
[[파일:Bof18.jpg | center]]
 +
 
 +
test.pls의 $eip의 값을 “jmp esp” 변경한다. 타겟 프로그램을 오버플로우 시키면 “cc” 에서 브레이크가 걸리는 것을 확인 할 수 있고 “90”값도 변경된 것을 확인 할 수 있다. 이제 마지막으로 원하는 shellcode를 삽입시키면 된다.
 +
 
 +
[[파일:Bof19.jpg | center]]
 +
<br />
 +
[[파일:Bof20.jpg | center]]
 +
 
 +
다음은 계산기의 쉘코드이다. (해당 쉘코드는 운영체제 마다 다르기 때문에 해당 운영체제에 맞게 생성해줘야 한다. )
 +
 
 +
[[파일:Bof21.jpg | center]]
 +
 
 +
완성된 공격코드 파일을 생성하는 코드이다.
 +
 
 +
[[파일:Bof22.jpg | center]]
 +
 
 +
해당 코드를 실행하면 프로그램이 종료가 되면서 계산기가 실행이 된다.
 +
 
 +
[[파일:Bof24.jpg | center]]
 +
 
 +
 
 +
 
 +
== '''Symbolic Execution''' ==
  
 
심볼릭 실행은 실제 값 대신 Symbolic을 추적하는 프로그램의 분석을 나타낸다. 예를 들면, 이 그림과 같은 코드가 있을 때 read() 함수의 리턴 값을 symbolic variable로 정하고 s 라고 한다.  (여기서 s와 y는 동일하다.) 심볼릭 실행을 통해, y=2*y를 거치면 y=2*s 가된다. 다음 조건문에서 if(y==12)를 통과하는 데 조건문의 결과가 TRUE면 2s=12가 된다. 이와 같은 방식으로 symbolic variable s를 실행과정에서 추적하면서 프로그램을 분석을 한다. STP는 테스트 케이스를 생성하는 것에 도움을 주는 툴로 비트벡터(Boolean 시퀀스 변수)의 산술에 대한 결정 절차(decision procedure)이다. 심볼릭 실행을 바탕으로 구성이 되어 있고 조건식을 쿼리를 전달받아 테스트 케이스를 생성하는데 도움을 준다. 심볼릭 실행은 최근 프로그래밍 언어 학자들에 의해 개발된 방법이며, 특히 프로그램 테스팅 시 다양한 경로와 조건을 실행할 수 있는 입력 값 및 초기 값 생성을 가능케 한다.
 
심볼릭 실행은 실제 값 대신 Symbolic을 추적하는 프로그램의 분석을 나타낸다. 예를 들면, 이 그림과 같은 코드가 있을 때 read() 함수의 리턴 값을 symbolic variable로 정하고 s 라고 한다.  (여기서 s와 y는 동일하다.) 심볼릭 실행을 통해, y=2*y를 거치면 y=2*s 가된다. 다음 조건문에서 if(y==12)를 통과하는 데 조건문의 결과가 TRUE면 2s=12가 된다. 이와 같은 방식으로 symbolic variable s를 실행과정에서 추적하면서 프로그램을 분석을 한다. STP는 테스트 케이스를 생성하는 것에 도움을 주는 툴로 비트벡터(Boolean 시퀀스 변수)의 산술에 대한 결정 절차(decision procedure)이다. 심볼릭 실행을 바탕으로 구성이 되어 있고 조건식을 쿼리를 전달받아 테스트 케이스를 생성하는데 도움을 준다. 심볼릭 실행은 최근 프로그래밍 언어 학자들에 의해 개발된 방법이며, 특히 프로그램 테스팅 시 다양한 경로와 조건을 실행할 수 있는 입력 값 및 초기 값 생성을 가능케 한다.
92번째 줄: 215번째 줄:
 
  |    |  |
 
  |    |  |
 
  +-----+---+
 
  +-----+---+
[[파일:maze3.gif]]
+
 
 +
[[파일:Maze3.gif]]
  
 
'#' 까지 도달하기 위한 결과 값이다.  
 
'#' 까지 도달하기 위한 결과 값이다.  
200번째 줄: 324번째 줄:
 
  * ssssddddwwaawwddddsddw
 
  * ssssddddwwaawwddddsddw
 
  * ssssddddwwaawwddddssssddwwww
 
  * ssssddddwwaawwddddssssddwwww
 +
 +
<출처 : http://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ >

2012년 12월 27일 (목) 13:36 기준 최신판

BOF (Buffer OverFlow)

버퍼 오버플로(buffer overflow) 또는 버퍼 오버런(buffer overrun)은 메모리를 다루는 데에 오류가 발생하여 잘못된 동작을 하는 프로그램 취약점이다. 컴퓨터 보안과 프로그래밍에서 이는 프로세스가 데이터를 버퍼에 저장할 때 프로그래머가 지정한 곳 바깥에 저장하는 것이다. 벗어난 데이터는 인접 메모리를 덮어 쓰게 되는데 다른 데이터가 포함되어 있을 수도 있는데, 손상을 받을 수 있는 데이터는 프로그램 변수와 프로그램 흐름 제어 데이터도 포함된다. 이로 인해 잘못된 프로그램 거동이 나타날 수 있으며, 메모리 접근 오류, 잘못된 결과, 프로그램 종료, 또는 시스템 보안 누설이 발생할 수 있다.

버퍼 오버플로가 코드를 실행시키도록 설계되거나 프로그램 작동을 변경시키도록 설계된 입력에 의해 촉발될 수 있다. 따라서 이는 많은 소프트웨어 취약점의 근간이 되며 악의적으로 이용될 수 있다. 경계 검사로 버퍼 오버플로를 방지할 수 있다.

버퍼 오버플로는 보통 데이터를 저장하는 과정에서 그 데이터를 저장할 메모리 위치가 유효한지를 검사하지 않아 발생한다. 이러한 경우 데이터가 담긴 위치 근처에 있는 값이 손상되고 그 손상이 프로그램 실행에 영향을 미칠 수도 있다. 특히, 악의적인 공격으로 인해 프로그램에 취약점이 발생할 수도 있다.

흔히 버퍼 오버플로와 관련되는 프로그래밍 언어는 C와 C++로, 어떤 영역의 메모리에서도 내장된 데이터 접근 또는 덮어쓰기 보호 기능을 제공하지 않으며 어떤 배열에 기록되는 데이터가 그 배열의 범위 안에 포함되는지 자동으로 검사하지 않는다.

<출처 : http://ko.wikipedia.org/wiki/%EB%B2%84%ED%8D%BC_%EC%98%A4%EB%B2%84%ED%94%8C%EB%A1%9C> 

Stack은 메모리 구조의 일부분이다. Stack은 보통 FILO(first in last out)혹은 LIFO(last in first out)이라고 불리운다. 나중에 입력된 값이 먼저 호출되는 방식이다

Bof1.jpg

Stack segment는 지역 변수와 프로시저 호출, data segment는 정적변수와 동적변수를, text segment는 프로그램 명령어를 저장한다. Stack를 악용하는 형태가 스택 오버플로우이다. 다음 그림과 같은 코드가 존재할 때 스택에 RET,SFP가 생기고 그 위에 코드의 정보가 쌓이게 된다.

Bof2.jpg

RET는 return address라 불리기도 하는데 프로그램 실행도중 반복문이나 함수를 호출하여 그 부분이 실행되고 난 후 복귀를 하기 위하여 정해놓은 주소값이다. 즉 실행되었던 함수가 종료를 하고 원래 코드의 나머지 부분을 실행하기 위하여 돌아올곳을 알기위해서 기억하는 주소이다.(=EIP)Sfp는 스택 포인터라고 불리기도 한다. 스택은 유동적이기 때문에 일정한 기준점(EBP)를 만들고 EBP를 기점으로 찾고자 하는 data의 위치를 주소 값으로 찾기 위하여 필요하다. 다음 그림과 같은 코드가 존재할 때 스택에 RET,SFP가 생기고 그 위에 코드의 정보가 쌓이게 된다.

Bof3.jpg

스택 버퍼플로우의 원리는 주어진 버퍼의 용량을 초과하는 값을 넣어 EIP까지 덮어씌우게 만들어서 EIP의 주소를 알아내어 임의의 영역으로 점프 뛰게 만들어 자신의 shellcode를 실행시키는 것이다.

(1) 스택 오버플로우 예제 오버플로우를 일으키기 위해 Perl script로 다음과 같은 파일을 만든다. 버퍼에 “A”를 가득 메우는 코드이다. 프로그램을 실행시켜 방금 만든 코드의 결과를 불러온다. 20000byte의 문자열을 입력하였지만 오버플로우가 일어나지 않았다.

my $file = “crash.m3u”;
my $junk = “A” * 20000;
open($FILE, “>$file”);
print $FILE $junk;
close($FILE);
Bof4.jpg

코드를 고쳐 30000byte의 문자를 입력하여 보면 오버플로우가 발생하여 프로그램이 죽는 현상을 볼 수 있다. 오버플로우가 발생한 것이다.

my $file = “crash.m3u”;
my $junk = “A” * 30000;
open($FILE, “>$file”);
print $FILE $junk;
close($FILE);
Bof5.jpg


Windbg를 이용하여 버퍼오버플로우가 발생한 상태를 확인해보자. EIP가 0x41(A)로 채워진 것을 볼 수 있다. 다음 할 일은 EIP를 덮어쓰기 위하여 Buffer 사이즈를 알아낼 필요가 있다.

Bof6.jpg

다음과 같이 A를 25000으로 변경하고 B를 5000개로 변경한 후 다시 프로그램을 실행시킨다. 오버플로우가 발생하며 Windbg로 EIP가 “42”로 채워져 있으면 있다는 것을 알 수 있다. 즉 EIP는 25000~30000사이에 존재한다는 것을 알 수 있다.

ESP, 즉 스택에도 “B”로 채워진 것을 알 수 있다.

Bof7.jpg

정확한 buffer크기를 알기위하여 metasploit을 실행하여 다음 그림에서와 같이 패턴을 생성한 후 만들어진 패턴을 Perl 코드의 junk2에 복사 해 넣는다.

Bof8.jpg
my $file = “crash.m3u”;
my $junk = “A” * 25000;
my $junk2 = “pattern”
open($FILE, “>$file”);
print $FILE $junk.$junk2;
close($FILE);


EIP에 다음과 같이 저장된 것을 볼 수 있고 metasploitl에서 다음과 같이 실행한다. 2787이 리턴주소를 덮어쓰기 위한 사이즈인 것을 알 수 있다. 그러므로 25000+1062 이후가 리턴 주소란 것을 짐작 할 수 있다.

Bof9.jpg


Bof10.jpg

$junk의 크기를 재수정한 후 $eip를 BBBB로 채운 후 $esp에 “C”로 채워 본다. 해당 결과를 입력으로 타켓 프로그램을 실행하면 Windbg에서 EIP에 0x42424242와 ESP에 0x43으로 채워져 있는 것을 확인할 수 있다.

Bof11.jpg


Bof12.jpg

Shellcode를 삽입하기 위해서 ESP(stack pointer)의 주소도 알아야한다. 다음과 같이 perl코드를 변경하여 테스트하여 본다. 타켓 프로그램을 실행해서 Windbg를 확인하면 ESP의 첫주소를 알 수 있다. 이로써 EIP에 원하는 코드의 주소를 넣을 수 있고 (control flow hijacking), ESP에 Shellcode를 넣을 수 있다.

Bof13.jpg


Bof14.jpg

EIP의 값 조작을 통해 (Control flow hijacking) 스택에 있는 쉘코드를 실행하여야 한다. 하지만 쉘코드가 저장된 스택을 바로 호출 할 수 없기 때문에 “jump esp” 코드를 이용하여 스택에 저장된 코드를 실행한다.

윈도우 프로그램은 하나이상의 DLL파일을 사용하고 이 DLL파일에는 많은 코드 지시자들이 있고 주소도 대부분 정적이다. 그러므로 ESP로 점프하는 DLL파일의 코드를 찾아 EIP에 이 주소를 써주면 ESP로 점프할 것이다. 그러기 위해선 jmp esp의 opcode를 알아야한다. 타겟 프로그램을 불러들인 후 다음과 같이 기입한다. 그 후 ‘U’로 확인해본다. Opcode는 ffe4이다.

Bof15.jpg


Bof16.jpg

적당한 DLL을 찾기 위해 windbg에서 Debug->Modules를 선택한다. 타겟 프로그램의 DLL파일의 주소에서 ff e4(jmp esp)코드를 찾는다.

Bof17.jpg


Bof18.jpg

test.pls의 $eip의 값을 “jmp esp” 변경한다. 타겟 프로그램을 오버플로우 시키면 “cc” 에서 브레이크가 걸리는 것을 확인 할 수 있고 “90”값도 변경된 것을 확인 할 수 있다. 이제 마지막으로 원하는 shellcode를 삽입시키면 된다.

Bof19.jpg


Bof20.jpg

다음은 계산기의 쉘코드이다. (해당 쉘코드는 운영체제 마다 다르기 때문에 해당 운영체제에 맞게 생성해줘야 한다. )

Bof21.jpg

완성된 공격코드 파일을 생성하는 코드이다.

Bof22.jpg

해당 코드를 실행하면 프로그램이 종료가 되면서 계산기가 실행이 된다.

Bof24.jpg


Symbolic Execution

심볼릭 실행은 실제 값 대신 Symbolic을 추적하는 프로그램의 분석을 나타낸다. 예를 들면, 이 그림과 같은 코드가 있을 때 read() 함수의 리턴 값을 symbolic variable로 정하고 s 라고 한다. (여기서 s와 y는 동일하다.) 심볼릭 실행을 통해, y=2*y를 거치면 y=2*s 가된다. 다음 조건문에서 if(y==12)를 통과하는 데 조건문의 결과가 TRUE면 2s=12가 된다. 이와 같은 방식으로 symbolic variable s를 실행과정에서 추적하면서 프로그램을 분석을 한다. STP는 테스트 케이스를 생성하는 것에 도움을 주는 툴로 비트벡터(Boolean 시퀀스 변수)의 산술에 대한 결정 절차(decision procedure)이다. 심볼릭 실행을 바탕으로 구성이 되어 있고 조건식을 쿼리를 전달받아 테스트 케이스를 생성하는데 도움을 준다. 심볼릭 실행은 최근 프로그래밍 언어 학자들에 의해 개발된 방법이며, 특히 프로그램 테스팅 시 다양한 경로와 조건을 실행할 수 있는 입력 값 및 초기 값 생성을 가능케 한다.

동적 심볼릭 수행 도구(KLEE)

KLEE 는 LLVM bytecode 의 해석기를 기반으로, LLVM bytecode 로 컴파일 된 프로그램을 입력으로 받아서 명령어를 수행하고 심볼릭하게 표현된 프로그램의 상태 변경을 기록한다. 프로그램 수행 가운데 분기를 만나게 되면 현재 프로그램의 심볼릭 상태에 따라 분기할 수 있는 경우를 계산하고 가능한 실행 경로를 따라 계속해서 프로그램을 실행한다. 현재 프로그램의 심볼릭 상태가 특정 분기를 실행할 수 있는지 검사하기 위해 KLEE 는 bit-level 정확도를 갖는 조건식을 생성하고 bit-vector 로직을 지원하는 SMT solver 를 사용해서 조건식을 풀어낸다.

(1) KLEE 수행 예


int my_islower(int x) {
 if (x >= 'a' && x <= 'z')
   return 1;
 else return 0;
} 


KLEE를 이용하여 위와 같은 함수를 테스팅을 하기 위해서는 symbolic input으로 실행을 하여야한다. 따라서 klee_make_symbolicdmf 이용하여 값에 symbolic 마킹을 하고 이를 사용한다.

 int main() {
     char c;
     klee_make_symbolic(&c, sizeof(c), "input"); 
     return my_islower(c);
 } 


위와 같은 코드를 LLVM bitcode로 컴파일 파일을 한다.

$ llvm-gcc --emit-llvm -c -g demo.c
$ klee demo.o 
KLEE: output directory = "klee-out-0"
KLEE: done: total instructions = 69  
KLEE: done: completed paths = 3      
KLEE: done: generated tests = 3

컴파일을 통해 나온 결과를 다음과 같이 실행을 한다.

이와 같이 3가지의 testcase를 생성한 것을 볼 수 있다. 3가지의 testcase 내용은 다음과 같다.

$ ktest-tool klee-last/test000001.ktest 
 ktest file : 'klee-last/test000001.ktest'
 args       : ['demo.o']
 num objects: 1
 object    0: name: 'input'
 object    0: size: 1
 object    0: data: 'b'
$ ktest-tool klee-last/test000002.ktest 
 ...
 object    0: data: '~'
$ ktest-tool klee-last/test000003.ktest 
 ..
 object    0: data: '\x00'

이와 같이 3가지의 testcase를 이용하여 프로그램을 실행하여보면 다음과 같은 결과를 얻을 수 있다.

$ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
$ KTEST_FILE=klee-last/test000001.ktest ./a.out 
$ echo $?
 1
$ KTEST_FILE=klee-last/test000002.ktest ./a.out 
$ echo $?
 0
$ KTEST_FILE=klee-last/test000003.ktest ./a.out
$ echo $?
 0 

위의 결과를 보면 KLEE는 if (x >= 'a' && x <= 'z') 조건에 대하여 x를 symbolic value로 정하고 이에 대한 값 \x00, ‘b’, ‘~’를 만들어 낸 것을 확인 할 수 있다. 이는 'a'보다 작은 케이스, x >= 'a' && x <= 'z' 조건에 부합하는 케이스, ‘z’보다 큰 케이스를 생성하였다고 확인 할 수 있다.


(2) KLEE 수행 예 - Maze

다음은 KLEE를 사용하여 토이 프로그램인 maze를 자동으로 해결하는 예제이다. 토이 프로그램 maze의 소스코드는 http://pastebin.com/6wG5stht 에서 구할 수 있다.

먼저 maze예제를 KLEE를 사용하지 않고 수동으로 해결하여 본다.

gcc maze.c –o maze
( a : Left, d : Right, w : Up, s : Down )
Player pos: 1x4
Iteration no. 2. Action: s.
+-+---+---+
|X|     |#|
|X| --+ | |
|X|   | | |
|X+-- | | |
|     |   |
+-----+---+

Maze3.gif

'#' 까지 도달하기 위한 결과 값이다.

ssssddddwwaawwddddssssddwwww

KLEE를 사용하여 자동으로 해결하여 본다. 먼저 KLEE를 사용하기 위해서는 LLVM-gcc를 이용하여 LLVM bitcode를 생성하고 이를 KLEE로 실행하여야 한다. 일반적으로는 다음과 같이 LLVM bitcode는 LLVM bitcode interpreter를 이용하여 수행이 된다.

llvm-gcc -c –emit-llvm maze.c -o maze.bc
lli maze.bc

하지만 KLEE를 이용하여 Symbolic execution을 수행하여야 하기 때문에 LLVM bitcode interpreter 대신 KLEE를 사용한다. Symbolic execution을 위해서는 maze의 입력 값에 marking을 하여야 한다. 따라서 소스코드를 다음과 같이 수정하여야 한다.

read(0,program,ITERS); 

소스코드에서 위와 같은 코드를 아래와 같이 변경한다.

klee_make_symbolic(program,ITERS,"program");

또한 해더파일의 추가도 필요하다.

#include <klee/klee.h>

다음과 같이 컴파일을 한 후 실행하면

llvm-gcc -c -Ipath/to/klee –emit-llvm maze_klee.c -o maze_klee.bc
klee maze.bc

다음과 같은 결과를 얻을 수 있다. KLEE는 321개의 다른 경로를 탐색하였다.

KLEE: done: total instructions = 112773
KLEE: done: completed paths = 321
KLEE: done: generated tests = 318

그리고 해당 케이스에 대하여 테스트 케이스를 생성한다.

$ls klee-last/
assembly.ll test000078.ktest test000158.ktest
info test000079.ktest test000159.ktest
messages.txt test000080.ktest test000160.ktest
run.istats test000081.ktest test000161.ktest
run.stats test000082.ktest test000162.ktest
test000001.ktest test000083.ktest test000163.ktest
test000075.ktest test000155.ktest warnings.txt

각 케이스는 ktest-tool을 이용하여 확인 할 수 있다. 위의 결과는 문제를 해결하기 위한 테스트 케이스가 아닌 모든 경로에 대한 테스트 케이스이다. 따라서 문제를 해결하는 테스트 케이스를 얻기 위해 소스코드를 수정을 한다. 다음과 같이 “You win!”이라는 메시지를 띄우는 코드 이후에 klee_assert()를 삽입을 한다. klee_assert는 C언어의 assert함수와 동일하다. ( assert는 주어진 조건이 거짓이면 오류 메시지 출력과 함께 코어 덤프를 출력하고 프로그램을 종료한다. )

printf ("You win!\n");
klee_assert(0);  //Signal The solution!!

위와 같이 소스코드를 수정하고 컴파일 후 실행하여 보면 다음과 같이 오류 메시지 및 코어덤프를 생성하는 테스트 케이스를 확인 할 수 있다.

$ls -1 klee-last/ |grep -A2 -B2 err
test000096.ktest
test000097.ktest
test000098.assert.err
test000098.ktest
test000098.pc

해당 테스트 케이스의 내용을 확인하여 보면 다음과 같다.

$ktest-tool klee-last/test000098.ktest
ktest file : ‘klee-last/test000098.ktest’
args : ['maze_klee.o']
num objects: 1
object 0: name: ‘program’
object 0: size: 29
object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00

해당 결과를 통해 maze를 실행하여 보면 다음과 같이 미로의 벽에 문제가 있음을 확인 할 수 있다. 이와 같이 프로그램의 오류 및 버그 등을 찾는데에도 도움이 될 수 있다. 최종적으로 다음과 같이 4가지의 테스트 케이스를 얻을 수 있다.

$ktest-tool klee-last/test000097.ktest
ktest file : ‘klee-last/test000097.ktest’
args : ['maze_klee.o']
num objects: 1
object 0: name: ‘program’
object 0: size: 29
object 0: data: ‘sddwddddsddw\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′
$ktest-tool klee-last/test000136.ktest
ktest file : ‘klee-last/test000136.ktest’
args : ['maze_klee.o']
num objects: 1
object 0: name: ‘program’
object 0: size: 29
object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′
$ktest-tool klee-last/test000239.ktest
ktest file : ‘klee-last/test000239.ktest’
args : ['maze_klee.o']
num objects: 1
object 0: name: ‘program’
object 0: size: 29
object 0: data: ‘ssssddddwwaawwddddsddw\x00\x00\x00\x00\x00\x00\x00′
$ktest-tool klee-last/test000268.ktest
ktest file : ‘klee-last/test000268.ktest’
args : ['maze_klee.o']
num objects: 1
object 0: name: ‘program’
object 0: size: 29
object 0: data: ‘ssssddddwwaawwddddssssddwwww\x00′

최초 수동으로 찾은 결과 이외에도 버그를 통해 maze를 해결하는 3가지의 케이스를 더 찾을 수 있다.

* sddwddddsddw
* sddwddddssssddwwww
* ssssddddwwaawwddddsddw
* ssssddddwwaawwddddssssddwwww

<출처 : http://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ >