Angr_CTF

Đây là post ghi lại lời giải của những bài mình giải được trong Angr_CTF: https://github.com/jakespringer/angr_ctf. Ok, bắt đầu luôn nào.

Note: Bài này ở wordpress thì mình ghi khá chi tiết, tuy nhiên khi dời qua đây thì bệnh lười lại tái phát. Do đó mình sẽ không ghi lại đầy đủ mà chỉ viết những điểm chính thôi (thêm nữa là không có hình chụp IDA luôn nha). Để đọc bài viết chi tiết thì bạn có thể vào đây

01_angr_avoid

Bài này mình sẽ dùng .explore của Angr để giải. Khi dùng .explore() với tham số find, Angr sẽ tự động execute binary đến khi đạt được một state thỏa mãn điều kiện của find. Giá trị của find có thể là: – Một địa chỉ hoặc một list các địa chỉ. – Một hàm. Hàm này nhận tham số là một state và trả về điều kiện mà state đó cần thỏa mãn (cái này sẽ được minh họa ở bài tiếp theo) Các state thỏa mãn sẽ được đưa vào 1 stash tên là found (có thể hiểu stash là 1 list các state). Theo mặc định, khi tìm được 1 state thỏa mãn, Angr sẽ dừng việc tìm kiếm, tuy nhiên ta có thể thay đổi điều này bằng cách truyền thêm tham số num_found cho .explore().

Tương tự với find ta cũng có tham số avoid để chỉ ra những chỗ mà Angr cần “tránh”. Các giá trị mà avoid có thể nhận cũng tương tự như find. Khi gặp phải điều kiện khớp với tham số avoid, Angr sẽ bỏ state đang thực thi vào stash avoided, đồng thời dừng thực thi state đó.

1
2
3
4
5

import angr
proj=angr.Project("./01_angr_avoid")
main=0x08048602
state=proj.factory.entry_state(addr=main)
simgr=proj.factory.simulation_manager(state)

“Good job” chỉ được in ở hàm “maybe_good”, nên find sẽ mang địa chỉ của hàm này. Bên cạnh đó ta cũng có hàm “avoid_me”, hàm này đưa biến “should_success” về 0 (biến này về 0 thì luôn “try again”) nên ta sẽ tránh địa chỉ hàm này.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

import angr
 
proj=angr.Project("./01_angr_avoid")
main=0x08048602
state=proj.factory.entry_state(addr=main)
simgr=proj.factory.simulation_manager(state)
 
good=0x080485E0
bad=0x080485A8
 
simgr.explore(find=good,advoid=bad)
 
if (not simgr.found):
    print("Something is wrong!")
else:
    found=simgr.found[0]
    flag=found.posix.dumps(0)
    print(flag)

Note: simgr.found là một list gồm nhiều state, lấy một state trong đó giống như một list bình thường (simgr.found[0])

02_angr_find_condition

Mới đầu thì mình tưởng nó cũng giống chall trước, cơ mà nhìn vào mới thấy rắng có một đống địa chỉ in chữ “Good job.” 🙂 , do đó không truyền địa chỉ vô biến find được rồi.

Vậy phải truyền hàm vào thôi, hàm này sẽ kiểm tra xem “Good job.” có in ra màn hình không. Ta đưa thêm hàm kiểm tra “Try again” vào avoid luôn.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

import angr
 
proj=angr.Project("./02_angr_find_condition")
state=proj.factory.entry_state()
simgr=proj.factory.simulation_manager(state)
 
def good(state):
    return "Good Job." in (state.posix.dumps(1)).decode("utf-8")
def bad(state):
    return "Try again." in (state.posix.dumps(1)).decode("utf-8")
 
simgr.explore(find=good,avoid=bad)
import angr
 
proj=angr.Project("./02_angr_find_condition")
state=proj.factory.entry_state()
simgr=proj.factory.simulation_manager(state)
 
def good(state):
    return "Good Job." in (state.posix.dumps(1)).decode("utf-8")
def bad(state):
    return "Try again." in (state.posix.dumps(1)).decode("utf-8")
 
simgr.explore(find=good,avoid=bad)
 
if (simgr.found):
    result=simgr.found[0]
    flag=result.posix.dumps(0).decode("utf-8")
    print (flag)
else:
    print ("Something is wrong")

03_angr_symbolic_registers

Ở chall này, Angr không tự động inject symbol cho mình nữa. Lý do là bởi Angr chỉ có thể xử lý các format string đơn giản trong lệnh scanf. Với 3 chall trước, format string được dùng để lấy input là %8s , tuy nhiên chall này thì format string là “%x %x %x”, Angr không chèn symbol giùm được.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

import angr
 
#create a state
proj=angr.Project("./03_angr_symbolic_registers")
start_addr=0x08048980
state=proj.factory.blank_state(addr=start_addr)
 
#create some symbols
a=state.solver.BVS("a",32)
b=state.solver.BVS("b",32)
d=state.solver.BVS("d",32)
 
#write those symbols to registers
state.regs.eax=a
state.regs.ebx=b
state.regs.edx=d
 
#symbolic execution!!!
simgr=proj.factory.simulation_manager(state)
good=0x080489EE
bad=0x080489DC
simgr.explore(find=good,avoid=bad)
 
if (not simgr.found):
    raise Execption("Something is wrong!")
 
#print the result
result=simgr.found[0]
pass0=hex(result.solver.eval(a))
pass1=hex(result.solver.eval(b))
pass2=hex(result.solver.eval(d))
 
print ("%s %s %s" %(pass0, pass1, pass2))

04_angr_symbolic_stack

Lần này input không lưu trên thanh ghi nữa mà được để trong stack. Vậy thì ta sẽ đưa symbol vào stack thôi!

Sau khi tạo state rồi simgr các kiểu thì giờ ta bắt đầu xét đến stack. Mình chọn entry cho state là lệnh “mov eax, [ebp+var_C]”. Vì nhảy vào ngay giữa cái hàm nên chúng ta chưa có stack frame (do 3 lệnh “push ebp”, “mov ebp, esp”,”sub esp, 18h” để tạo stack frame nằm ở đầu hàm), ta phải tự tạo thôi

1
2

state.regs.ebp = state.regs.esp
state.regs.esp -= 0x18

Nhìn trong IDA thì thấy input được lưu trong 2 ô nhớ là [ebp-0xc] và [ebp-0x10], vậy giờ mình sẽ đẩy symbol vào 2 ô này.

1
2
3

ebp=state.solver.eval(state.regs.ebp)
first=state.solver.BVS("first",32sstate.solver.BVS("second",32state.mestate.memory.store(ebp-0xc,first,endness=proj.arch.memory_endness)
state.memory.store(ebp-0x10,second,endness=proj.arch.memory_endness)

**Note: ** Theo mặc định thì lệnh memory.store sẽ lưu giá trị theo kiểu “big-endian”, do đó ta cần phải chỉnh lại chỗ này cho đúng bằng cách thêm tham số endness (chỗ này mình ngồi cả buổi mới phát hiện ra 🙂 , rút kinh nghiệm lần sau phải đọc document cho kỹ)

Và phần còn lại chỉ là explore thôi

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

good=0x080486E9
bad=0x080486D7
simgr.explore(find=good,avoid=bad)

if (not simgr.found):
     raise Exception("Something is wrong!")

result=simgr.found[0]
first=result.solver.eval(first,cast_to=int)
second=result.solver.eval(second,cast_to=int)
print ("%d %d" %(first, second))

Note: Có một cách giải khác trong phần solution, cách này dùng lệnh “state.stack_push”. Dùng lệnh này thì ta không cần quan tâm endianess, đồng thời cách xử lý ebp và esp cũng hơi khác một chút. (Nhìn chung thì không khác nhiều, note lại để nhớ lệnh stack_push thôi 😀 )

05_angr_symbolic_memory

Cũng như bài trước, nhưng lần này dễ hơn vì input được lưu vào trong global variable, mà các biến này thì có địa chỉ xác định.

06_angr_symbolic_dynamic_memory

Lần này thì binary sẽ tạo 2 vùng nhớ động rồi lưu input trên đó, điều này khiến cho cách của bài 5 không làm được vì ta chỉ biết được địa chỉ của 2 vùng nhớ vào runtime.

Tuy nhiên nhìn vào IDA thì ta thấy rằng địa chỉ của 2 vùng nhớ động sẽ được lưu trong 2 biến global đã biết địa chỉ. Vậy ý tưởng giải bài này sẽ là lưu 2 địa chỉ do mình chọn vào các biến global: buffer0 và buffer1, tiếp đó đưa 2 symbol vào 2 địa chỉ trên.

Full script như sau:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

import angr
 
proj=angr.Project("./06_angr_symbolic_dynamic_memory")
entry=0x08048687
state=proj.factory.blank_state(addr=entry)
simgr=proj.factory.simulation_manager(state)
 
 
#initialize stack frame
state.regs.ebp=state.regs.esp 
state.regs.esp -=0x10
 
#set the address of 2 buffer
buffer0=0x10000000
buffer1=0x20000000
state.memory.store(0x0ABCC8A4,buffer0,endness=proj.arch.memory_endness)
state.memory.store(0x0ABCC8AC,buffer1,endness=proj.arch.memory_endness)
 
sym0=state.solver.BVS("sym0",64)
sym1=state.solver.BVS("sym1",64)
 
#the symbols are strings so no need for endness argument
state.memory.store(buffer0,sym0)
state.memory.store(buffer1,sym1)
 
good=0x08048759
bad=0x08048747
simgr.explore(find=good,avoid=bad)
 
if (not simgr.found):
    raise Exception("Something is wrong")
 
result=simgr.found[0]
flag0=result.solver.eval(sym0,cast_to=bytes).decode("utf-8")
flag1=result.solver.eval(sym1,cast_to=bytes).decode("utf-8")
print ("%s %s" %(flag0,flag1))

08_angr_constraints

Binary lấy input, encode, sau đó cho vào hàm để check.

Vào hàm đó xem thì thấy nó so sánh từng char của input sau khi encode với từng chữ trong string “AUPDNNPROEZRJWKB”. Vậy là ta có một vòng lặp 16 lần, nếu để angr thử hết tất cả các trường hợp thì hơi lâu, vì thế nên bài này ta sẽ dừng ngay trước lệnh call (tức không gọi hàm so sánh), sau đó add constraint vào bằng tay. (Lưu ý là sau khi dừng chương trình để thêm constraint thì ta không cho chạy tiếp nữa, do đó ở đây không có đoạn find với avoid)

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

import angr
 
proj=angr.Project("./08_angr_constraints")
entry=0x08048625
state=proj.factory.blank_state(addr=entry)
simgr=proj.factory.simulation_manager(state)
 
#add symbol to buffer 
password=state.solver.BVS("password",16*8)
buffer_addr=0x0804A050
state.memory.store(buffer_addr,password)
 
#stop before the check function 
check_addr=0x08048673
simgr.explore(find=check_addr)
if (not simgr.found):
    raise Exception("Wrong!")
 
result=simgr.found[0]
complex_pass=result.memory.load(buffer_addr,16)
result.solver.add(complex_pass=="AUPDNNPROEZRJWKB") #add 1 constraint
password=result.solver.eval(password,cast_to=bytes)
print (password)

09_angr_hooks

Bài này cũng giống như bài trước, tuy nhiên có một điểm khác khiến cho việc add constraint bằng tay trở nên kém hiệu quả hơn

Sau hàm check string dài dài kia thì chương trình còn 1 lần check nữa. Nếu ta dừng lại trước hàm “check_equal…” rồi thêm constraint bằng tay thì sẽ bỏ mất đoạn sau. Chính vì thế ta sẽ dùng đến hook, một công cụ của Angr cho phép ta thay một hay nhiều câu lệnh trong binary bằng một hàm trong python do người dùng viết.

Cấu trúc lệnh:

1
2

@proj.hook(<addr>,length=<>)
hooker(state): #hàm được thay

Tác dụng như sau: khi chương trình thực thi tới lệnh ở địa chỉ , nó sẽ dừng lại và chạy hàm ( 🙂 ) của chúng ta, sau đó sẽ bỏ qua byte kế tiếp (lưu ý là bỏ n byte chứ không phải bỏ n lệnh)

Với bài này thì mình muốn chương trình không thực hiện hàm check_equal mà sẽ chạy hàm của mình. Do dó mình nhập tham số addr là địa chỉ ngay chỗ gọi hàm check_equal, length thì có thể mở ida lên là tính được. Vậy giờ chỉ cần quan tâm xem hàm hooker sẽ làm gì thôi.

Nhìn vào IDA một lần nữa, ta thấy giá trị trả về của hàm check_equal được lưu vào eax. Ok, vậy đây sẽ là hooker của mình

1
2
3
4

@proj.hook(0x080486A9,length=15)
def hooker(state):
    passwd_buffer=state.memory.load(0x0804A054,16)
    state.regs.eax = state.solver.If(passwd_buffer=="XYMKBKUHNIQYNQXE",state.solver.BVV(1statstate.solver.BVV(0, 32))

Note: Đây là một số điều mình rút ra sau khi viết hàm này: – Lệnh state.solver.If(….) thể hiện một mệnh đề if-then-else và nó không tương đương với việc viết

1
2

if state.solver.is_true(passwd_buffer=="XYMKBKUHNIQYNQXE"):
   state.regs.eax=state.solver.BVV(1, 32)

• Không thể thay thế state.solver.BVV(1,32) và state.solver.BVV(0,32) bằng 1 và 0 được. Lý do thì mình chưa biết 🙂 (chắc phải nghía qua claripy một chút)

12_angr_veritesting

Veritesting là một thuật toán dùng để gộp các nhánh rẽ trong luồng thực thi, giúp cho symbolic execution đỡ tốn thời gian hơn. Để enable veritesting thì khi tạo simulation manager, ta chỉ cần:

1

simulation = project.factory.simgr(initial_state, veritesting=True)

Bài này thực ra y hệt như bài trên. Tuy nhiên nhờ veritesting gộp nhánh và làm đơn giản hàm nên ta không phải code hàm để hook nữa.