2015 christmasCTF writeup

아쉽게 4등을 했다.

캡쳐 찍어논거를 보고 대강 writeup을 쓴다. 

---

이미 선물을 줬다고해서 받은게 없어서 뭔지 몰랐다.

근데 로그인 어쩌고 공지가 떠서 로그인할 때 패킷을 보니 플래그가 박혀있었다.

---

압축파일을 풀면 nonogram이 나온다.

이 노노그램을 풀면 인스타그램 모습이 나온다.

여기서 힌트가 rgb이다.

따라서 가로에 있는 숫자들을 색깔별로 더했다.

rgb는 10;11;12이런식으로도 표현하고 #0A0B0C 이런식으로 표현한다.

인스타에서 해당 해시태그를 검색해보았다.

해시태그를 검색하면 밑에 FLAG가 있다.

---

사진파일을 binwalk로 보면 zip파일이 들어있다.

BEAR일때의 스위치 상태를 차례대로 적어서 BASE64돌리면 바로 답이나온다.

---

반복되는 문자열을 \n으로 분류 해주고

각 문자열의 길이를 소문자알파벳 역순의 리스트의 인덱스에 넣어주면 된다.

a = '''ABCDEFG
abcdefghijklmnopqrs
abcdefghijklmnopqrstuv
ABCDEFGHIJKLMNOP
abcdefghijklmnopqrstuv
ab
abcdefghijklmnopqr
abcdefgh
ABCD
abcdefghijklmnopqrstuv
ABCDEFGHIJKLMNOPQRSTUVWXYZ
abcdefghi
abcdefghijklmnopqrstuv
ABCDEFGHIJKLMNOPQRSTU
abcdefghi
abcdefghijkl
a
abcdefghijklmnopqrstuv
abcdefghijklm
ABCDEFGHIJKLMNOPQRSTUVWXY
abcdefghijklmnopqrstuv
abcdefghijklmnopqrstuv
abcdefghi
'''
maps = "abcdefghijklmnopqrstuvwxyz"[::-1]
a = a.split( "\n" )
a = a[:-1]
k = ''
for i in a:
   j = len(i)
   if j != 0:
      k+= maps[j-1]

print k
#TheKeyisWeAreFrozenBeer

---

음악안에 뭐가 숨겨져있다고한다.

뭔가 삘이 스펙트럼이여서 바로 캐롤을 들으면서 스펙트럼을 살펴보았다.

스펙트럼에 플래그가 적혀있었다.

---

mp4파일을 binwalk로 보면 7-zip파일이 숨겨져 있다.

이를 dd로 추출했다.

압축을 풀어보니 안에 IKEYU.gif파일이 있는데

비밀번호가 걸려있어서 볼 수가 없다.

따라서 raw파일에서 key를 찾아서 이 압축파일을 풀어야한다고 생각했다.

raw파일을 imageinfo를 해보니 xp덤프파일이였다.

프로세스트리를 보니 특별한 프로그램은 안보이고 HwpViewer가 켜져있었다.

어떤 파일을 열고있는지 확인을 해보았다.

dlllist를 보니 perhaps_first.docx를 열고있었다.

이 파일을 추출을 했다.

위의 사진과 base64로 인코딩된 문자열이 있었다.

디코드해보니 Let's play CTF라는 글자가 나왔는데 이 문자열로 압축이 안풀렸다.

그래서 생각을 하다가 파일이름이 perhaps_first인걸 생각해서 second로 파일스캔을 해보았다.

찾아보니 maybe_second.hwp파일이 있었고 다시 이를 추출했다.

이런 그림과 base64로 인코딩된 문자열이있었다.

압축비밀번호가 나왔고 저 문자열로 압축이 풀렸다.

오른쪽 상단에 있는 I.SOLO.U가 flag이다.

---

밥먹고 와서 이거 풀다가 대회가 끝났다.

이거만 풀었어도 3등인데 ..

풀던거 마저 풀어서 flag는 얻었다.

각 자리수를 변수라고 생각해서 방정식을 2n개 만들었다.

그리고 smt solver인 z3를 이용해서 방정식을 풀었다.

from z3 import *
from pwn import *

global conn

def solver() :
	conn.recvuntil('PROB', drop=False)
	print "start!"
	conn.recvline()
	n = int(conn.recvline().split(' : ')[1].split('\n')[0])
	arr_b = map(int, (conn.recvline().split(' : ')[1].split('\n')[0]).strip('[]').split(', '))
	arr_a = map(int, (conn.recvline().split(' : ')[1].split('\n')[0]).strip('[]').split(', '))
	#-------------------------------------------------------------------------------

	b = [0] * (n**2)
	result = [0] * (n**2)

	for i in range(len(b)) :
		b[i] = Int('b[%d]'%i)

	s = Solver()

	for i in range(n) :
		j = i*n
		s.add(sum(b[j:j+n])==arr_a[i])
		s.add(sum(b[i:i+n*(n-1)+1:n])==arr_b[i])

	for i in range(n**2) :
		s.add(b[i] >= 1)
		s.add(b[i] <= 9)

	s.check()
	m = s.model()
	for d in m.decls() :
		_i, _v = int(d.name().strip('b[]')), str(m[d])
		result[_i] = _v

	submit = ''
	for i in range(len(result)) :
		if (i % n == 0) and (i != 0) :
			submit += "|"
		submit += result[i]
	submit += '\n'

	conn.send(submit)
	print "send!!"

#-----main
conn = remote('grr.nadeko.moe', 10002)
cnt = 0
while True:
	try :
		solver()
		cnt+=1
		print "#",cnt,"_Clear!!!!\n"
		if cnt == 20 :
			break
	except :
		print conn.recv()
		conn.close()
		conn = remote('grr.nadeko.moe', 10002)
		cnt = 0
		continue

flag = conn.recvuntil('\n', drop=False)
print flag
print conn.recv()
conn.close()

---

문제에 제공된 python코드를 보면 assert부분을 참고하면 n은 소수이다.

n = a * b * c로 되어있는데 소수는 1과 자기자신만을 약수로 가지기 때문에 a = n, b = 1, c = 1로 볼 수 있다.

a + b + c가 1015209이기 때문에 a = 1015207, b = 1, c = 1이다.

이제 a, b, c를 알아 냈으니 z3를 이용해서 flag를 찾았다.

from z3 import *

a = 1015207
b = 1
c = 1
n = a * b * c

s = Solver()
m = Int('m')

s.add( m/a + m%a + m + m  == 4480179420102935122287)
s.add(m > 1)

s.check()
t = s.model()
str = str(t[t.decls()[0]])
print 'flag =', hex(int(str))[2:-1].decode('hex')