[CTF] wwctf 2024 - floats

서론 

대회에서는 풀지 못했지만, 요즘 리버싱에 집중하고 있기도 하고, 늦게 참가했더니 거의 유일하게 건든 문제라, 간단하게 기록해놓으려 한다. 

 

풀이

 

열면 엄청난 코드가 나를 반긴다.

./floats asdfasdfasdfasdf
Wrong :(

 

input을 받고 검사하는데, 잘 보면 32 바이트짜리 input을 16:16으로 나누어 각각 check1 함수, check2 함수에 전달하는 것을 알 수 있다.

 

 

이 코드 블럭은 비트가 0이면 0x8000000, 1이면 0x00000000로 할당해준다. 0x80000000는 -0.0, 0x00000000는 +0.0이다. 

 

그다음에는 각종 연산을 한다. 대회때는 핵심 아이디어까지만 파악하고 다른 분에게 넘겼었다. 

연산에는 +, -밖에 존재하지 않는다. -0.0 또는 +0.0밖에 없으니까 이 연산을 조금 더 간단하게 만들 수 있다. 

 

 

이렇게 나온다. 그러면 더하는 연산은 곧 & 연산과 같고, 빼는 연산은 곧 A & ~B 로 나타낼 수 있다. 

그러면 비트연산으로 어셈블리 코드를 파싱하자

 

movss   xmm1, [rbp+var_1584]
movss   xmm0, [rbp+var_15B0]
addss   xmm0, xmm1
movss   [rbp+var_1578], xmm0
movss   xmm0, [rbp+var_1584]
movss   xmm1, cs:dword_9040
xorps   xmm0, xmm1
movss   xmm1, [rbp+var_15B0]
subss   xmm0, xmm1
movss   [rbp+var_1574], xmm0

 

• cs:dword_9040는 0x80000000이므로 무시한다. 
• movss / xmm1 / var_1584 이런식으로 세가지 뭉텅이로 나눠서 파싱한다 

예를 들어서 

 

v137 = v121 + v132;

movss   xmm1, [rbp+var_1588]
movss   xmm0, [rbp+var_15B4]
addss   xmm0, xmm1
movss   [rbp+var_156C], xmm0

 

v138 = (float)-v132 - v121;

movss   xmm0, [rbp+var_1588]
movss   xmm1, cs:dword_9040
xorps   xmm0, xmm1
movss   xmm1, [rbp+var_15B4]
subss   xmm0, xmm1
movss   [rbp+var_1568], xmm0

 

v139 = (float)-(float)(v121 + v132) - v138;

movss   xmm0, [rbp+var_156C]
movss   xmm1, cs:dword_9040
xorps   xmm0, xmm1
movss   xmm1, [rbp+var_1568]
subss   xmm0, xmm1
movss   [rbp+var_1564], xmm0

 

이렇게 상응하는데 그러면 이걸 bitwise 연산으로 바꿔서 보기 쉽게 나열하는 것도 가능하다는 것이다. 

 

1. idapython 스크립트로 어셈블리 잡아옴 
2. check1, check2에 있는 loop들에 대해 비트연산으로 쭉 쓰게 만듬 

 

 

스크립트 두개를 돌리면 이렇게 뽑아낼 수 있다. check1과 check2는 사실 같은 기능을 수행한다.

이걸 가지고 z3 솔버에 넣으면 된다. 대회때 못쓰기도 했고 다른 사람 것 가져오고 싶지도 않아서 z3 스크립트 단계를 대충 요약하자면 

 

1. BitVec으로 128개의 변수를 초기화
2. 문자열 길이만큼 루프도므로 그것 고려해서 그냥 IDA 에서 주는대로 구현하면 된다. 
3. 우리가 잡아온 연산을 넣는다. z3이 이제 마땅히 되어야 하는 값을 만들어줄 것이다. 

비트를 다시 스트링으로 변환하면 값을 구할 수 있다. 

 

생각 

아이디어 자체의 신박함 (summation algorithm 차용) 한 것이 재밌었다. 씨텦을 정말 오랜만에 뛰는데 주마다 뛰는 게 여러모로 좋을 것 같다. 동아리에서도 드림핵 풀고 어쩔 수 없이 드림핵만 풀게 되는데 이게 좀 시야를 좁혀놓는다