Search

[REV] solver

Year
2021
CTF Name
TrollcatCTF
Category
REV
Type
Z3

1. Description

I love soluchan
nc 157.230.33.195 4444
Flag format Trollcat{.*} Author : codacker

2. Write up

문제 파일을 받아서 확인해보면 64bit ELF 파일임을 확인할 수 있다.
# unzip solver.zip Archive: solver.zip inflating: crackme # file crackme crackme: ELF 64-bit LSB shared object, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=6c8f4137ce00dd9571d3b551dc81d8d4354e4d91, for GNU/Linux 3.2.0, stripped
Bash
복사
문제 파일은 아래와 같이 실행된다.
실행 시 "Enter key: " 문자열 출력 후 입력받음
키가 틀린 경우 "Invalid key" 문자열 출력
# ./crackme Enter key: aaaabbbbccccdddd Invalid key
Bash
복사
실행으로 알아낸 정보를 기반으로 확인해보면 아래와 같은 루틴을 확인 할 수 있다.
[rbp+buf]에 입력한 문자열 저장
입력한 문자열을 기반으로 sub_563109F28738 함수 실행
함수의 결과가 0이 아닌 경우 플래그 출력
sub_555A363D9200 함수의 결과에 따라 플래그가 출력되기 때문에 sub_555A363D9200 함수 내부를 확인해봐야 한다.
함수 내부는 아래와 같다. 입력한 key값을 갖고 여러가지 연산을 하고 있고 이때 아래의 조건을 모두 만족하면 플래그를 얻을 수 있다.
sub_555A363D9200 함수 내부를 확인해보면 우리가 입력해야하는 키 길이는 22자리임을 알 수 있다. 이를 기반으로 z3 모듈을 활용해 해당 수식들을 만족하는 키를 찾았다.
from z3 import * result = "" key = [ BitVec('a%i'%i,8) for i in range(0,22)] s = Solver() for i in range(1,22): s.add(key[i] > 47, key[i] <= 122) s.add(key[0] + key[3] == 100) s.add(key[1] + key[18] == 214) s.add(key[2] + key[4] == 178) s.add(key[5] ^ key[6] == 76) s.add(key[8] - key[7] == 17) s.add(key[10] - key[9] == 59) s.add(key[12] + key[11] - key[13] == 69) s.add(key[15] + key[14] - key[16] == 31) s.add(key[16] + key[17] - key[18] == 88) s.add(key[20] ^ key[19] ^ key[21] == 69) if (s.check()): m = s.model() for i in range(22): result += chr(m[key[i]].as_long()) print (result) #4z90y8t9J:u1M920Cq\0G2 #flag : Trollcat{z3_b4by}
Python
복사

3. FLAG

Trollcat{z3_b4by}