Layer7 리버싱 10차시 과제(VM) - prob for beginner

일단 문제를 내려받고 아이다를 통해 열어보았다.

이런 식의 코드가 나왔다.
사용자로부터 16자리 플래그를 입력받고, initcpu, runcpu 두 개의 함수를 거친 후에 v5의 HIDWORD값이 참이라면 Wrong.., 거짓이라면 Correct!를 출력하고 있다.
내용을 보니 v5의 HIDWORD값이 거짓이 나오게 해야할 것 같은데, HIDWORD가 무엇일까?
인터넷에 쳐보니, 상위 4바이트라고 한다. (Hi(GH) DWORD)
흠, 아무래도 v4변수는 v5까지 포함하는 것 같은데, 아이다가 해석을 잘못한 것 같다.
y키를 이용해 v4의 크기를 4로 바꿔주자.

이런 식으로 문자열 형식으로 바꿔주면, 아까는 HIDWORD로 표현되던 부분이 이런 식으로 바뀐다.

따라서 v4의 4번째 인덱스에 들어있는 값의 상위 4바이트가 0이면 Correct!가 출력된다.

이렇게 분석준비를 끝마쳤으니, 본격적으로 initcpu, runcpu를 분석해보자.

initcpu를 호출하는 과정이다.
0으로 초기화된 버퍼 v4, 사용자로부터 문자열을 입력받은 v5 두 개를 인자로 건네주고 있다.

initcpu 내부이다.
a1은 v4, a2는 v5의 주소를 갖고 있다.
아마 이 함수는 중요한 역할은 아니고, 그냥 사용자로부터 입력받은 문자열을 v4 배열에 복사하고 있는 것 같다.

그럼 다음으로 runcpu 부분을 분석해보자.

사용자가 입력한 문자열이 들어있는 v4를 인자로 주고 있다.

runcpu 내부이다.
a1은 사용자의 입력이 담긴 v4 문자열의 주소를 가지고 있고, 밑에 보면 a1에 모두 DWORD로 접근하는 것을 볼 수 있기에 a1의 자료형 자체를 _DWORD *로 하면 코드가 간결해질 것이다.

코드가 굉장히 간결해졌다.

이제 우리는 여기서 저 연산을 거치는 와중에 a1[3]을 0으로 만드는 입력값을 찾아야하는데,
z3-solver를 이용해 풀어볼 것이다.

일단 z3-solver에 쓸 식을 만들어주자.
그러기 위해선 stub의 데이터를 복사하고 그걸 이용해 식을 계산하는 과정을 문자열로 출력하면 z3-solver에 쓸 식을 얻어낼 수 있다.
그냥 저 위 코드를 그대로 복사해서 코드로 만들어주고,

이 부분만 문자열로 출력하면 식을 얻어낼 수 있다.
한 번 만들어보자.

stub의 데이터는 [shift+e] 키를 눌러 얻어낼 수 있다.

이런 식으로 얻어낸 후에, 이 데이터를 C++ 코드에 복사한다.

그 이후, runcpu 코드를 그대로 붙여 넣으면,

이런 코드가 나온다.
그리고 이걸 컴파일하고 실행시킨다면,

이런 식들이 나오는데, 모두 z3-solver에서 사용할 식들이다.
중간에 & 0xFFFFFFFF을 써준 이유는 4바이트를 벗어날 수 있기 때문이다.

그럼 이걸 그대로 z3-solver로 옮겨준 뒤, Correct!를 출력할 조건, 즉, v4[3]==0 -> a1[7]==0 (a1은 int형이므로)을 add해주고, model 해주면 a1과 관련된 모든 플래그가 나올 것이다.

일단 파이썬 익스플로잇 코드에 들어가 8개의 32비트 비트벡터를 선언해준다.
그 후, Solver 객체를 할당해준 후,

이런 식으로 식을 모두 할당해주면 model을 수행했을 때 플래그가 나올 것이다.

이런 식으로 출력 코드를 짜면 플래그가 4글자씩 무작위로 나올 것이다.

이런 식으로 플래그가 나오는데, 이를 플래그 순서대로 조합하면

flag : L7{VM_BEGINNER!}