LakeCTF 2022 - baby rev (rev, z3)

WriteUp › Lake
,

분석 환경: Windows 11, Ubuntu 20.04
사용자 제공 파일: 바이너리, nc 접속 주소

평소에 리버싱 분야를 잘 풀지 않는데, 뭔가 오늘따라 풀어보고 싶어서 솔브가 많은 리버싱 하나 열어봤다.

Analysis

IDA로 열면 main함수가 있는데 대충 핵심적인 부분(밖에 없지만)을 가져오면 아래와 같다.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
__printf_chk(1LL, "What's your your number:", envp);
fflush(_bss_start);
__isoc99_scanf("%u", &input);
v3 = 0LL;
key = 0;
if ( input - 0x10000 > 0x7FFF0000 )
  goto LABEL_4;
do
{
  v5 = input >> v3++;
  key = (v5 & 1) + 2 * key;
}
while ( v3 != 0x20 );
if ( input == key )
{
  v7 = fopen("flag.txt", "r");
  if ( v7 )
  {
      // print flag
  }
}

사용자 입력을 받고 그 입력에 대해 ‘어떠한 연산’을 진행한 결과(key)와 비교해서 맞으면 flag를 출력해준다.

브루트 포싱을 하면 되지 않을까? 이 코드를 c로 옮겨서 브포해봐야겠다.

Solve

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// gcc -o solve solve.c
#include <stdio.h>

int main() {

	int input = 1;

	while(1) {
		if (input - 0x10000 < 0x7fff0001) {
			int key = 0;
			for (int v3 = 0; v3 < 0x20; v5++) {
				key = ((input >> v3) & 1) + 2 * key;
			}

			if (input == key) {
				printf("%d\n", input);
				break;
			}
		}
		input++;
	}

}

이런식으로 c로 코드를 옮기고 루프를 돌려주면 아래와 같이 98304라는 값이 나온다. 사실 이 문제 정답을 여러개인데 하나만 입력하면 flag를 던져주기 때문에 하나만 출력하고 바로 break를 해주었다.

1
2
3
4
5
jir4vvit@ubuntu:~/ctf/lake/rev-baby$ ./solve 
98304
jir4vvit@ubuntu:~/ctf/lake/rev-baby$ nc chall.polygl0ts.ch 3600
What's your your number:98304
EPFL{4ft3r_th15_h0w_h4rD_caN_r3V_8e?}

More

이 문제를 파이썬 모듈인 Z3 solver를 이용하여 풀 수도 있다.

Z3 solver

Z3 solver는 특정 값, 즉 정답을 찾아주는 SMT solver 모듈이라고 한다. (SMT: Satisfiability Modulo Theories)
어떠한 수식을 만족하는 값이 존재하는 지 찾아주는 건데, 존재한다면 그 값을 구해준다.

1
2
x + y = 12
x - y = 6

예를 들어, 이런 연립방정식이 존재할 때, x와 y의 값을 Z3 solver가 구해줄 수 있다.
바로 아래와 같이..

1
2
3
4
5
>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> solve(x+y==12,x-y==6)
[x = 9, y = 3]

아래에 다운로드 방법과 여러 링크들을 남기고 Z3를 이용하여 이 문제를 어떻게 풀 수 있는지 알아보자.

다운로드 방법

1
pip install z3-solver

공식 github 링크
z3py-tutorial

solve with Z3

일단. 모듈을 가져오고 변수 두 개를 선언해야 한다.

1
2
3
4
5
6
7
from z3 import *

#ipt = Int('ipt')
ipt = BitVec("ipt", 32)

#key = Int('key') # key is not variable
key = 0

실수들이.. 주석처리되어 있는데, 가장 처음 했던 실수는 사용자 인풋을 그냥 Int()로 정의한 점이다.
BitVec("", 비트수)로 정의해야 한다. 왜냐하면 이 문제에서 사용자 인풋을 가지고 비트연산을 진행하는데 Int()로 선언하면 TypeError가 발생하기 때문이다.

1
TypeError: unsupported operand type(s) for >>: 'instance' and 'int'

그래서 비트연산을 할 때는 비트연산을 위한 BitVec()으로 선언을 해줘야 한다.

두 번째 했던 실수는 단순하다. 그냥 미지수 아닌데 미지수로 선언해줬다. 그러면 안된다.

1
2
for v3 in range(0, 32):
    key = ((ipt >> v3) & 1) + 2 * key

파이썬으로 연산 코드를 작성해준다.

1
2
3
4
5
s = Solver()

s.add(ipt - 0x10000 < 0x7fff0001)
s.add(0 < ipt)
s.add(ipt == key)

Z3 solver는 Solver 객체를 지원해준다. 이 객체를 사용해보자. s.add(수식)로 ipt에 대한 제약 조건 및 값을 구하는 조건도 추가해줬다.

Sovler 객체 참고 링크

1
2
3
while s.check() == sat:
    print(s.model())
    s.add(ipt != s.model()[ipt]) # dupule check

s.check()는 해당 방적식을 만족하는 값(정답, 해)이 있는지 체크해준다. 값이 있으면 sat, 없으면 unsat, 해결할 수 없으면 unknown을 반환한다고 한다.

이 문제는 값이 여러 개가 나오므로 중복 체크도 해주었다. 방금 구한 ipt의 값을 제외한 다른 값을 구할 수 있다.

s.model()은 s.check()가 sat일 때 만족하는 해 중 하나를 반환한다.

최종 코드

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
from z3 import *

ipt = BitVec("ipt", 32)
key = 0

for v3 in range(0, 32):
    key = ((ipt >> v3) & 1) + 2 * key

s = Solver()

s.add(ipt - 0x10000 < 0x7fff0001)
s.add(0 < ipt)
s.add(ipt == key)

while s.check() == sat:
    print(s.model())
    s.add(ipt != s.model()[ipt]) # duplicate check

Reference

https://tistory.d1n0.me/18
https://realsung.tistory.com/185