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

일단 ida64로 실행파일을 열어보았다.

main함수의 초반 부분은 이런데, prob-begin 문제와 같이 %s 형식 지정자로 입력받지만, v4변수가 long long형이기 때문에 char[16]형으로 바꿔주었다.

바꾸기를 원하는 변수를 클릭하고 y키를 누르면 변수 타입을 바꿀 수 있다.

이렇게 변수를 바꿔준 후, 밑에 있는 if문으로 확인했다.

이런 식으로 아주 긴 조건문이 나왔는데, 잘 보면 v4의 0번째부터 QWORD만큼(즉, 8바이트)을 가져와서 쓰고 있다.
이 말은 입력받은 16자리 문자열을 8바이트짜리 long long형 두 개로 바꿔 사용하고 있다는 것이다.

따라서 우린 z3-solver로 방정식을 풀기 전, 변수를 선언할 때 long long의 크기만큼으로 선언해야 하고, 중간에 xor같은 비트연산자들이 나오므로, 비트벡터를 이용해 풀어야 한다는 사실을 알 수 있다.
한 번 구현해보자.

일단 이런 식으로 z3를 임포트 해오고,

64비트짜리 비트벡터 2개를 선언해 필요한 미지수를 선언한 후,
마지막으로 if문에 포함돼있는 두 개의 식을 add시키면 방정식의 해를 구할 수 있다.
참고로, 숫자 뒤에 LL이 붙어있는데, 이는 C에서 숫자가 long long형임을 명시해줄 때 쓴다.
따라서 정수형의 크기 제한이 없는 파이썬에서는 쓸데가 없다.
삭제해주자.
모든 똑같은 항목에 대해서 똑같은 작업을 수행할 땐, "모든 항목 변경"을 이용하면 편한다.

여기서 모든 항목 변경을 클릭하면 소스에 포함된 모든 "LL"에 대해 똑같은 작업을 수행할 수 있다.

이 작업을 두 번하고, QWORD 포인터 같이 파이썬에서 안 쓰이는 놈들을 제거해주면, solve.check()를 출력했을 때 sat이 나온다.

sat이 정상적으로 출력된 걸 볼 수 있다.
따라서 s.model()을 실행시킨 후, 리스트 v4에 들어있는 순서대로 출력하면 플래그가 나올 것이다.
이것도 간단하니 구현해보자.
* as_long은 z3_solver의 Int를 파이썬의 long형으로 변환시켜 준다.
* to_bytes는 파이썬 정수를 바이트씩 끊어서 보여준다.

방금 별표 표시(*)로 알려줬던 함수들을 순서대로 잘 섞어서 출력하면,

이런 식으로 플래그가 나온다.

flag : L7{WO_R_U_GOSU?}