FoobarCTF 2021 reversing Write-up (Z3)

서 론

한 2주만에? CTF문제를 다시 풀어보는 것 같다. 

오랜만에 감도 잡을겸 ctftime에 있는 대회중 대충 집어서 문제를 풀어봤다.

---

 

Child_rev

---

upx패킹이 되어있어 패킹을 풀고 분석을 진행하였다.

 

이 함수가 메인 코드이다. for문을 34번 돌면서 비교를하는데 항상 참이어야한다.

 

if문을 보면

v6[34] == v6[0], v6[35] ==v6[1]..... 이런식일 것이다.

 

잘 생각해보면

10째줄을 xor한번더 해주면된다. v7(고정값)을 가지고 말이다.

 

l = [ 0x012F78,  0x012F30, 0x012F72,  0x012F5F, 0x012F61,  0x012F6E, 
      0x012F64,  0x012F5F, 0x012F6C,  0x012F30, 0x012F67,  0x012F31, 
      0x012F63,  0x012F40, 0x012F6C,  0x012F5F, 0x012F73,  0x012F68, 
      0x012F31,  0x012F66, 0x012F74,  0x012F5F, 0x012F65,  0x012F40, 
      0x012F73,  0x012F79, 0x012F5F,  0x012F72, 0x012F31,  0x012F67, 
      0x012F68,  0x012F38, 0x012F3F,  0x012F3F ]
      
KEY = 0x12F00

flag=''
for i in l:
    flag +=chr(i^KEY)

print(flag)

 

 

---

NET_DOT

---

문제파일은 dll이고 C#으로 컴파일 되어있다.

 

(일부 코드 생략)

이 부분이 핵심인데.........

역연산으로 푸는 것이 정석인 것 같은데

 z3도 공부할겸 z3로 끄적여봤다.

 

sum_all<- 값은 쉽게 구할 수 있다. 

(플래그가 G로 시작할 것이고, 이를 이용해 ord('G') ^ 2410;

 

from z3 import *

s= Solver()

flag = [BitVec('flag{}'.format(i),64) for i in range(26)]
arr = [2410,2404,2430,2408,2391,2381,2333,2396,2369,2332,2398,2422,2332,2397,2416,2370,2393,2304,2393,2333,2416,2376,2371,2305,2377,2391]

    
#for i in range(0, 26):
#    s.add(flag[i] >= 48)
#    s.add(flag[i] <= 122)


for j in range(0,26):
    s.add(flag[j]-(j%2*2 + j%3) ^ 2349 == arr[j])


if s.check() == sat:
    m = s.model()
    w=''
    for i in range(26):
        w +=chr(m[flag[i]].as_long())
    print(w)

 

---

Numerical Computing

---

 

메인 코드이다.

 

이것 또한 역연산을 하면 될 것 같지만....

z3로 해결하였다.

from z3 import *

s= Solver()

flag = [BitVec('flag{}'.format(i),64) for i in range(18)]

table=[0x160,0x6c,0x100,0x54,0x2f0,0xa0,0x670,0x1e0,0x7b0,0xcc,0x250,0x194,0x700,0x1c8,0x240,0xa8,0x7b0,0xd8]


    
#for i in range(0, 18):
#    s.add(flag[i] >= 48)
#    s.add(flag[i] <= 122)

enc = "QWERTYUIOPASDFGHJK"
for j in range(0,18):
    if j %2 == 0: # if odd
        s.add((16*(ord(enc[j])^flag[j])) == table[j])
    else:
        s.add((4*(ord(enc[j])^flag[j]) == table[j]))


if s.check() == sat:
    m = s.model()
    w=''
    for i in range(18):
        w +=chr(m[flag[i]].as_long())
    print(w)

 

 

---

Not_Only_z3

---

아.. Z3그 자체이다...코드가 너무길다.