고정 헤더 영역
상세 컨텐츠
본문
728x90
반응형
파일 정보
$ file 03_angr_symbolic_registers
03_angr_symbolic_registers: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=5eaf22d08b110b8badc7537a2d06d9160c157106, not stripped
Code Analysis
int __cdecl main(int argc, const char **argv, const char **envp)
{
int v3; // eax
int v4; // edx
int v5; // ST1C_4
int v6; // ST14_4
int v8; // [esp+8h] [ebp-10h]
int v9; // [esp+Ch] [ebp-Ch]
printf("Enter the password: ");
v3 = get_user_input();
v5 = v4;
v6 = complex_function_1(v3);
v8 = complex_function_2();
v9 = complex_function_3(v5);
if ( v6 || v8 || v9 )
puts("Try again.");
else
puts("Good Job.");
return 0;
}
int get_user_input()
{
int v1; // [esp+0h] [ebp-18h]
int v2; // [esp+4h] [ebp-14h]
int v3; // [esp+8h] [ebp-10h]
unsigned int v4; // [esp+Ch] [ebp-Ch]
v4 = __readgsdword(0x14u);
__isoc99_scanf("%x %x %x", &v1, &v2, &v3);
return v1;
}
- 3개의 사용자 입력을 받고, v1을 리턴해서 main의 v3에 저장한다. v3는 edx 레지스터이다.
- 그리고 v5에 v4 값을 할당하여 사용자 입력값이 저장된다.
- 이후 complex_function_1,2,3으로 연산 작업 후 리턴 값을 각각 v6, v8, v9에 저장 후, v6 || v8 || v9가 0이 아니면 “Try again.”을, 0이면 “Good Job.”을 출력한다.
unsigned int __cdecl complex_function_1(int a1)
{
return ((((((((((((((((((((((a1 - 420322684 + 1163254121) ^ 0x38BDBFFA) + 833994404) ^ 0xBB5BC0D3) + 818950291) ^ 0x26AE42F)
- 1308760604) ^ 0x908D2EB5)
+ 2040470327) ^ 0xB68D584C)
+ 257065541) ^ 0x7941018E)
+ 996809967) ^ 0x46C690C0)
+ 1331913891) ^ 0xC4882FAE)
+ 1144149218) ^ 0xD6E6AC7)
- 1841018320) ^ 0x7EDB252C)
- 2073398773
+ 216052059) ^ 0x2CD40F8)
+ 1842419477;
}
unsigned int __cdecl complex_function_2(int a1)
{
return (((((((((((((a1 + 919422334) ^ 0x125146CE) + 677602448) ^ 0x49DAABD3) + 346690412) ^ 0x67B450F) - 1602579177) ^ 0xF7EAD291)
- 23849406
+ 651630098) ^ 0x229C8487)
+ 1592767252) ^ 0x818058F0)
+ 2052667023) ^ 0x23DED7BE;
}
unsigned int __cdecl complex_function_3(int a1)
{
return (((((((((a1 ^ 0x946DC8AF) - 1972647488) ^ 0x9257991D) - 884025286 + 782999385) ^ 0x290002B2) - 122173832) ^ 0x3074172D)
- 2080333267) ^ 0x55B548D1)
+ 261491912;
}
Exploit
state
.entry_state() 바이너리 entry point에서 실행될 수 있도록 상태를 준비한다.
.blank_state() 데이터들이 초기화되지 않은 빈 상태를 만든다. 초기화되지 않은 데이터에 접근 시 unconstrained symbolic 값이 리턴될 수 있다.
.blank_state() 를 사용할 때 start_address를 지정해주는게 좋다.
text:080488A1 ; __unwind {
.text:080488A1 lea ecx, [esp+4]
.text:080488A5 and esp, 0FFFFFFF0h
.text:080488A8 push dword ptr [ecx-4]
.text:080488AB push ebp
.text:080488AC mov ebp, esp
.text:080488AE push ecx
.text:080488AF sub esp, 14h
.text:080488B2 sub esp, 0Ch
.text:080488B5 push offset aEnterThePasswo ; "Enter the password: "
.text:080488BA call _printf
.text:080488BF add esp, 10h
.text:080488C2 call get_user_input
.text:080488C7 mov [ebp+var_14], eax
start address 는 main 주소에서 scanf 이후 주소(0x080488C7)로 줬다.
state = p.factory.blank_state(
addr=0x080488C7,
add_options={angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
)
symbolic bitvectors
- angr에서 symbolic 값을 바이너리에 넣는데 사용하는 datatype이다.
- state.solver.BVS(name, size)
- name: angr에서 symbolic data 참조 시 사용하는 이름
- size: size in bits
int get_user_input()
{
int v1; // [esp+0h] [ebp-18h]
int v2; // [esp+4h] [ebp-14h]
int v3; // [esp+8h] [ebp-10h]
unsigned int v4; // [esp+Ch] [ebp-Ch]
v4 = __readgsdword(0x14u);
__isoc99_scanf("%x %x %x", &v1, &v2, &v3);
return v1;
}
scanf로 3개의 입력을 받기 때문에, 입력에 사용할 3개의 symbolic data를 만들어준다. 이때 각 데이터는 int 형이고 x86에서 int형은 32bit이므로 BVS에서 size는 32로 준다.
SIZE=0x20
input0 = state.solver.BVS('input0', SIZE)
input1 = state.solver.BVS('input1', SIZE)
input2 = state.solver.BVS('input2', SIZE)
set register: state.regs
angr에서는 scanf에서의 여러 입력을 지원하지 않는다. 따라서 scanf 호출 이후 register 값에 직접 symbolic 값을 넣어줘야 한다.
state.regs 는 register 이름을 지정하여 해당 레지스터에 값을 저장할 수 있다.
만약 eax 레지스터에 symbolic 값인 input0 값을 저장하고 싶으면, state.regs.eax = input0와 같이 사용한다.
.text:08048867 xor eax, eax
.text:08048869 lea ecx, [ebp+var_10]
.text:0804886C push ecx
.text:0804886D lea ecx, [ebp+var_14]
.text:08048870 push ecx
.text:08048871 lea ecx, [ebp+var_18]
.text:08048874 push ecx
.text:08048875 push offset aXXX ; "%x %x %x"
.text:0804887A call ___isoc99_scanf
.text:0804887F add esp, 10h
.text:08048882 mov eax, [ebp+var_18]
.text:08048885 mov edx, [ebp+var_14]
.text:08048888 mov ebx, edx
.text:0804888A mov edx, [ebp+var_10]
어셈블리 코드를 보면, scanf로 ebp+var_10, ebp+var_14, ebp+var_18에 입력받은 값을 각각 edx, ebx, eax 레지스터에 저장하고 있다.
int v1; // [esp+0h] [ebp-18h]
int v2; // [esp+4h] [ebp-14h]
int v3; // [esp+8h] [ebp-10h]
따라서 eax, ebx, edx 레지스터 값을 input0, input1, input2로 지정해주면 된다.
state.regs.eax = input0
state.regs.ebx = input1
state.regs.edx = input2
반응형
get solve of given bitvector: state.solver.eval
.explore 로 find, avoid 주소를 지정해서 가능한 모든 경로를 찾은 후, 만약 found stash가 비어있지 않으면 solution이 있는 것이므로 해당 state에서의 solution을 구한다.
symbolic 값에 대한 해결을 eval로 얻을 수 있다. 여러 solution이 있으면 eval을 사용해서 그 중 하나만 얻을 수 있다.
simgr = p.factory.simgr(state)
# find possible path with given address
simgr.explore(find=lambda s: b'Good Job.' in s.posix.dumps(sys.stdout.fileno()), avoid=lambda s: b'Try again.' in s.posix.dumps(sys.stdout.fileno()))
if simgr.found:
solution_state = simgr.found[0]
print('solution state:', end=' ')
print(solution_state)
# pass eval the bitvector that we want to solve
solution0 = solution_state.solver.eval(input0)
solution1 = solution_state.solver.eval(input1)
solution2 = solution_state.solver.eval(input2)
이 이후부터는 앞선 예제들과 동일하게 avoid, find address를 지정하여 explore를 사용해서 solution을 찾을 수 있는 가능한 모든 경로를 찾고, 해당 상태에서 solution을 구하면 그게 구하는 입력들이다.
#!/usr/bin/python
import angr, sys
# create angr project
p = angr.Project('./03_angr_symbolic_registers')
# specify start address where symbolic execution engine should begin
state = p.factory.blank_state(
addr=0x80488C7,
add_options={angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
)
# create symbolic bitvectors
SIZE=32
input0 = state.solver.BVS('input0', SIZE)
input1 = state.solver.BVS('input1', SIZE)
input2 = state.solver.BVS('input2', SIZE)
# set register to a symbolic value
state.regs.eax = input0
state.regs.ebx = input1
state.regs.edx = input2
simgr = p.factory.simgr(state)
find_condition=lambda s: 'Good'.encode() in s.posix.dumps(sys.stdout.fileno())
avoid_condition=lambda s: 'Try'.encode() in s.posix.dumps(sys.stdout.fileno())
# find possible path with given address
simgr.explore(find=find_condition, avoid=avoid_condition)
if simgr.found:
solution_state = simgr.found[0]
print('solution state:', end=' ')
print(solution_state)
# pass eval the bitvector that we want to solve
solution0 = solution_state.solver.eval(input0)
solution1 = solution_state.solver.eval(input1)
solution2 = solution_state.solver.eval(input2)
print("%x %x %x" % (solution0, solution1, solution2))
else:
raise Exception('could not find the solution')
728x90
반응형
'SYSTEM HACKING > CTF, etc' 카테고리의 다른 글
| [angr_ctf] 05_angr_symbolic_memory (0) | 2022.05.14 |
|---|---|
| [angr_ctf] 04_angr_symbolic_stack (0) | 2022.05.14 |
| [angr_ctf] 02_angr_find_condition (0) | 2022.05.14 |
| [angr_ctf] 01_angr_avoid (0) | 2022.05.14 |
| [angr_ctf] 00_angr_find (0) | 2022.05.14 |
