b01lers - chuggachugga

나름 쉬운 문제이다.

 

오호 64bit 바이너리

알맞은 코드를 입력해야되는 것 같다.

 

바로 아이다로 분석을 시작했다.

 

'뭐가 이렇게 많지?' 라고 겁먹었지만 그럴 필요 없다. 

 

메인 함수만 보면 된다.

 

일단 코드를 입력하고 비교하는 것이 키포인트이기 때문에 입력받는 함수를 찾았다.

 

여기서 v33[1]이 문자열의 크기라고 유추할 수 있다.

 

fmt_Fscan의 포맷이 뭔지는 잘 모르겠는데, 실제로 코드에 3글자아래로 입력하면 에러가 뜬다.

 

그럼 그 아랫부분의 코드를 살펴보자

 

S[2]가 't'인지 비교하고,,,,S[1]은 'c'인지 비교하고 S[3]^'t'의 결과가 18인지 비교해보면...

 

맙소사 ctf라는글자가 완성된다. 덤으로 S[4]가 '{'에서 쐐기를 박는다.

 

그럼 여기 나와있는 코드들을 쭉 조합 및 연산하여 플래그를 구하면 된다.

 

나는 이걸 손과 머리로 해도 금방 할 줄 알고 하다가 시간 엄청 날려먹었다.

(딱 봐도 z3로 푸는 문제였는데 오랜만이기도하고, 뭔가 귀찮아서.....)

 

직접적으로 어떤 문자인지 비교해주는 부분을 제외하고, 나머지는 수식을 정리해서 z3로 풀어보도록 하자.

 

 

직접 정리해본 결과, 나는 저 정도의 수식이 가장 간단했다. 

 

그럼 이 수식들을 z3를 이용해서 풀어보자!

 

이렇게 z3 소스코드를 만들고, 플래그를 유추해볼 수 있고,

 

나는 한글자를 알아내지 못해서 나머지 한글자는 브루트포싱 했다.

 

이런식으로 좀 거지같지만 간단하게 소스를 짜면,,,,

 

플래그로 보이는 내용이 나오고, 이를 입력해보면!?