Rating:


IDA로 열어보면 main 함수가 이와같이 생겼습니다.

일론 머스크가 아니라 머론 어스크에게 패스워드를 물어봅니다.

포맷 스트링을 통해서 문자열을 입력받았기 때문에, 임의의 함수 이름을 제가 편한대로 _scanf() 로 변경하였고,

`%4s` 로 입력을 받기 때문에 4자리의 비밀번호겠구나 라고 생각했습니다.

중간에 for문 가지고 장난치는 부분이 나오는데 코드를 쓱 보면 argv에 장난질 하지 말라는 내용인 것 같아 무시해버렸습니다.

여차해서, 결국엔 else 분기에 있는 `pickFunction(seed)`를 호출하게 됩니다. 함수 포인터로 말이죠.

그럼 `pickFunction` 함수로 가보겠습니다.

인자로 seed를 받고, seed를 가지고 특정 연산을 거친 뒤 그 값이 73이면 flag를 출력하는 함수를 호출합니다.

funOne 부터 funFive가 있었는데, funTwo 만 flag를 출력하는 함수였고 나머지는 다 낚시였습니다.

파일 포인터로 flag 파일을 read하는 것을 보면 바로 알 수 있겠죠?

그런데 우리는 `(seed[2] | seed[3]) & (*seed | seed[1])` 라는 연산을 해서 73이 나오는 seed 값을 모릅니다. 그래서 z3 Solver로 대신 풀어주겠습니다.

```Python
from z3 import *

seed1 = BitVec('seed1', 8)
seed2 = BitVec('seed2', 8)
seed3 = BitVec('seed3', 8)
seed4 = BitVec('seed4', 8)
s = Solver()

s.insert(seed1 > 33)
s.insert(seed1 < 127)
s.insert(seed2 > 33)
s.insert(seed2 < 127)
s.insert(seed3 > 33)
s.insert(seed3 < 127)
s.insert(seed4 > 33)
s.insert(seed4 < 127)

s.insert((seed3 | seed4) & (seed1 | seed2) == 73)

print( s.check() )
print( s.model() )
```

여기서 각 seed에 33, 127을 넣어준 이유는 "출력 가능한 ASCII 문자"의 범위를 지정해준 겁니다.

왜 지정을 해줬냐면, 이러한 지정을 해주지 않으니 seed의 일부 값이 0이 나오는 기현상이 발생했기 때문에 지정을 해주었습니다.

바로 스크립트를 가동해보았습니다.

잘 작동하는 것을 확인할 수 있습니다.

nc로 연결해서 해당 패스워드를 입력해줍니다.

간단하게 플래그를 획득할 수 있었습니다.

flag는 `flag{c1RcU1t5_R_fUn!2!}`