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

이번 과제는 친절하게도 익숙한 C++파일이었고, 내용은 C언어와 다를 게 없었다.
따라서 문자열을 문자 변수 여러개로 인식해서 보기 불편하게 만드는 불상사는 생기지 않았다.

한 번 코드를 살펴보자.

이런 식으로 16자리 문자열을 입력받은 후, 문자열에 대해 특정 연산을 수행한 후에 그 연산 결과가 조건을 만족시키면 Correct!, 다르면 Wrong...을 출력하고 있다.
아마 Correct!를 출력해야 플래그가 나올 것 같기에 저 식을 z3-solver로 풀어 해를 구하면 될 것 같다.
(참고로 미지수의 개수만큼 식이 있어야 식을 풀 수 있는데 위의 조건문엔 식이 총 16개이므로,
사용자 입력의 길이와 같아 해를 구할 수 있는 조건을 만족한다.
그럼 한 번 구현해보자.

일단, 비트연산자들은 보이지 않으니, z3 Int형으로 선언하면 풀 수 있을 것 같다.
그래서 이렇게 16개짜리 z3 Int형의 미지수들을 선언해주었다.

그 다음, s를 Solver()함수로 할당받은 후, s에 방정식을 16개 모두 추가하면, s.check()를 실행했을 때 sat이 출력될 것이고, 그 후 data에 들어있는 순서대로 출력하면 플래그가 나올 것이다.

따라서 그냥 이런 식으로 s에 16개 방정식을 모두 추가했다.

그 후, 아까 말했던 대로 s.check()를 수행한 후, s.model()의 결과값을 data 변수에 들어있는 순서대로 출력하면 플래그가 나올 것이다.

이런 식으로 model한 결과값을 data에 들어있는 순서대로, 문자형으로 바꾼 후 출력하면 플래그가 출력될 것이다.

플래그가 정상적으로 출력된 걸 확인할 수 있다.

flag : L7{EZ_PROB_SOL!}