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

일단 파일을 다운받고 ida64로 열어 디컴파일 후 코드를 분석해보았다.

처음 부분에 "%s" 형식 지정자로 입력을 받는데 입력받는 변수 타입이 그냥 char형인 걸 보고 y키를 이용해 변수 타입을 16칸짜리 char형 배열로 바꿔주었다.

정상적으로 변경된 걸 볼 수 있다.

그 후, 밑에 있는 코드를 분석해보았다.

밑에 if문으로 굉장히 복잡한 식으로 입력한 정보가 식에 맞는지 틀린지 확인하고 맞으면 Correct! Flag is ur input, 틀리면 Wrong을 출력하고 프로그램을 종료하고 있다.

따라서 맞는 입력값을 찾으려면 저 식을 모두 만족하는 변수 16개를 모두 찾아야 하는데, 미지수 x개가 있을 때 모든 x를 구하기 위해선 식이 x개 필요하고, 마침 조건문에 들어있는 식의 개수가 16개이니 16개의 미지수 모두 찾아낼 수 있다.
그러나 문제가 있다.
저 16개의 방정식을 손으로 풀어야 한다면 굉장히 많은 시간과 노력이 들 것이다.
따라서 우린 z3-solver를 이용해 방정식을 대신 풀도록 시킬 것이다.
일단 z3-solver를 사용할 수 있도록 z3를 임포트해주자.

그 다음, z3-solver를 사용할 수 있게 Int형으로 미지수를 설정해두자.
차례대로 s[0], s[1] ... s[15] 까지 설정을 마쳤다.

이렇게 설정을 마치면, Solver() 함수를 호출해 식을 계산해낼 수 있는 환경을 만들자.

이런 식으로 짜고, solver.add()를 16번 호출해 각 add() 함수 안에 각 방정식을 넣으면 알아서 풀어줄 것이다.

이런 식으로 각 add() 안에 방정식을 넣어준다.
그 후, solver.check()를 호출하고 solver.model()까지 호출하면 방정식이 모두 풀어진다.

그 다음 순서에 맞게 출력하기 위해,

이런 식으로 Int() 리스트 s에 들어있는 순서대로 출력하면 플래그가 나올 것이다.

플래그가 잘 나온다.
flag : L7{4_G00D_3T4R7}