Layer7 리버싱 9차시 과제 - prob4 풀이

이번에도 prob3와 마찬가지로 소스에서 Correct!를 출력하는 부분을 실행시키는 것이 목표인 것 같다.

따라서 저 조건에 맞는 입력을 넣어야 되는데, 미지수가 총 4개이고, 식은 8개이다.
따라서 미지수보다 식의 개수가 많으므로 충분히 풀 수 있다.
z3-solver를 이용해 한 번 풀어보자.
일단, unsigned long long형으로 자료를 선언해야하는데, 중간에 xor 등 비트연산자가 나오므로 비트벡터 형식으로 선언해야 한다.

이런 식으로 미지수 4개를 unsigned long long(64비트)의 비트벡터 형식으로 선언했다.
그 후, 임의의 변수에 Solver 객체를 할당하고, 식을 모두 추가한 뒤 check()를 호출하면 방정식이 풀렸다는 뜻의 sat이 출력될 것이다.

이런 식으로 if문에 있던 방정식을 모두 추가하고, check()를 호출했더니,

이런 식으로 sat이 출력됐다.

따라서 맞는 값을 입력했다는 걸 알 수 있고, 이를 data에 들어있는 순서대로 출력하면 플래그가 나올 것이다.
그러나 한 가지 문제가 있다.
바로 우리가 얻은 값은 64비트 정수형이라 문자로 출력이 불가능하다는 것이다.
바로 이때 필요한 함수가 to_bytes라는 함수이다.
to_bytes(8, "little") 또는 to_bytes(8, byteorder="little")
이런 식으로 쓰면 정수를 8바이트씩 리틀엔디언 방식으로 잘라 준다.
이를 이용하면 64비트 정수도 1바이트씩 쪼개서 출력할 수 있다.
한 번 해보자.

이렇게 비트벡터를 정수형으로 변환하고, 그 정수를 8바이트씩 리틀엔디언 방식으로 쪼갠 후, 문자로 변환해 한 글자씩 data에 들어있는 순서대로 출력하면 플래그가 나온다.

플래그가 정상적으로 나왔다.

flag : L7{DID_YOU_MASTER_Z3_SOLVER?WOW}