angr - (3) Solving CTF Challenges

angr를 이용하여 CTF 문제들을 풀어보자.

https://github.com/angr/angr-doc/tree/master/examples

[Codegate 2017] angrybird

우선 바이너리 패치를 하자. angr로 바이너리 수정을 하려했는데 적용이 안된다.. 애초에 writable하지 않아서 그런가..? 잘 모르겠다.

patch

• 0x40077b : jz(=0x0f84)를 jnz(=0x0f85)로 수정
• 0x606060 : 21로 값 수정 (4byte)
• 0x40071a : mov eax, [esp] 를 mov rax, [rsp] 로 수정. 0x67 -> 0x48
• 0x400721 : jnz(=0x0f85)를 jz(=0x0f84)로 수정
• 0x400752 : jz(=0x74)를 jnz(=0x75)로 수정
• 그냥 거슬리는 것들 NOP 처리했다.

https://l0z1k.tistory.com/entry/IDA-binary-patch

처음에 이것만 패치를 해줬는데 계속 풀리지가 않았다. 공식 solve에 따르면 angr 자체에서 got를 load한 것이 맞는지 체크를 해준다고 한다. 그래서 바이너리 자체적으로 got 값을 스택에 넣게되면 오류가 발생하고 어쩌고저쩌고... 사실 그런 느낌이고 확실히는 잘 모르겠다.

정말 싹다 패치했다. 그러고 나서야 main 함수 처음부터 시작해도 플래그를 찾는다. 0x404fbc 주소로 가는 것이 목표다.

from angr import *

p = Project('./angrybird_patch')

main = 0x400761
FIND = 0x404fbc

state = p.factory.entry_state(addr=main)

simgr = p.factory.simgr(state)
simgr.explore(find=FIND)
print(simgr.found[0].posix.dumps(0))

---

[Defcamp CTF 2015] r100

앵거로 날먹하기 딱 좋은 문제다.

from angr import *
p=Project('./r100')
state=p.factory.entry_state(addr=0x400811)
sm=p.factory.simgr(state)
sm.explore(find=0x400844)
print(sm.found[0].posix.dumps(0))

---

[Google 2016 CTF] Unbreakable

main 함수를 보면 argv로 인자값을 주어 수많은 함수를 거쳐서 마지막 함수인 0x400830에서 성공했다는 문자열을 출력하고 종료된다. 지금까지는 stdin으로 input을 주었다면 이번에는 argv로 인자값을 주는 방법을 알아보자.

Claripy(angr의 solver engine)의 BV(Bit Vector)를 사용한다.

>>> import claripy

# Create a 32-bit symbolic bitvector 'x'
>>> x = claripy.BVS('x', 32)
>>> x
<BV32 x_0_32>

# Create a 32-bit bitvector with the value '0xdeadbeef'
>>> y = claripy.BVV(0xdeadbeef, 32)
>>> y
<BV32 0xdeadbeef>

claripy - Solver Engine 을 참고하자.

또한 이 문제를 풀 때, 플래그의 시작이 CTF{ 인 것을 알려주지 않으면, 엉뚱한 답이 나온다.

add_constraints로 설정해두자. 또한 buf_symbolic_bytes를 따로 설정해주지 않으면, out of range 오류가 발생하게 된다. 따로 크게 잡아주자.

from angr import *
import claripy

FIND = 0x400830
AVOID = (0x400850, )

p=Project('./unbreakable', load_options={'auto_load_libs':False})

argv1 = claripy.BVS('argv1', 8*0x43)
state = p.factory.entry_state(args=[p.filename, argv1])

state.libc.buf_symbolic_bytes = 0x60
state.add_constraints(argv1.chop(8)[0]=='C')
state.add_constraints(argv1.chop(8)[1]=='T')
state.add_constraints(argv1.chop(8)[2]=='F')
state.add_constraints(argv1.chop(8)[3]=='{')

sm = p.factory.simgr(state)
sm.explore(find=FIND, avoid=AVOID)

print(sm.found[0].solver.eval(argv1, cast_to=bytes))

---