# CTF Reverse-[Anxun Cup 2019]game-Use deflat to make conventional logical judgments after the main confusion is de-obfuscated

Source: https://buuoj.cn/

Content: none

Attachment: https://pan.baidu.com/s/1qq_64SNIRnnTTCNqNIKOiw?pwd=1iz9 Extraction code: 1iz9

## general idea

Determine the functions related to the input, and then use deflat.py to flatten the program for these functions.

Reverse scripting to get the answer

## detailed steps

• Check file information

• When custom methods such as general_inspection and trace are turned on, the program finds that the control flow is particularly large, which may be confused

Use deflat.py (see attachment), check that the address of the main method in ida is 0x4006F0, and deflat the functions that operate on the input, check1, check3, and check2, respectively.

• A check2 is set in the check3 function. This function is to judge whether the input value of the user is the same as the global variable. Double-click to open the sodoku and D0g3 variables, and shift+e to get the map as shown in the figure. The D0g3 variable will receive the changed input value, even if the user input is the same as its sodoku variable

• The implementation of the check1 function is to convert v_input:

• 0-len/2-1 of v_input is interchanged with len/2-len
• v_input[2n] and v_input[2n+1] are interchanged
• v_input[k] = (v_input[k] & 0xF3 | ~v_input[k] & 0xC) - 20
• Create a 0-9 map by using z3, i.e. each digit gets its original input

• ```from typing import List
import z3
import struct

def convert(raw: str) -> List[int]:
raw = bytearray.fromhex(raw)
raw = [raw[x*4:(x+1)*4] for x in range(int(len(raw)/4))]
raw = [struct.unpack('<I', x)[0] for x in raw]
return raw

v_sudo = '010000000400000005000000030000000200000007000000060000000900000008000000080000000300000009000000060000000500000004000000010000000200000007000000060000000700000002000000080000000100000009000000050000000400000003000000040000000900000006000000010000000800000005000000030000000700000002000000020000000100000008000000040000000700000003000000090000000500000006000000070000000500000003000000020000000900000006000000040000000800000001000000030000000600000007000000050000000400000002000000080000000100000009000000090000000800000004000000070000000600000001000000020000000300000005000000050000000200000001000000090000000300000008000000070000000600000004000000'
v_d0g3 = '010000000000000005000000030000000200000007000000000000000000000008000000080000000000000009000000000000000500000000000000000000000200000000000000000000000700000000000000000000000100000000000000050000000000000003000000040000000900000000000000010000000000000000000000030000000000000000000000000000000100000000000000000000000700000000000000090000000000000006000000070000000000000003000000020000000900000000000000040000000800000000000000000000000600000000000000050000000400000000000000080000000000000009000000000000000000000004000000000000000000000001000000000000000300000000000000000000000200000001000000000000000300000000000000070000000000000004000000'
v_sudo = convert(v_sudo)
v_d0g3 = convert(v_d0g3)
print(f'v_sudo:{v_sudo}')
print(f'v_d0g3:{v_d0g3}')
s = z3.Solver()
v_result = [index + 48 for index, x in enumerate([0] * 10)]  # ascii to initialize numbers
v_input = [0] * len(v_result)
v_input = [z3.BitVec(str(index), 16) for index, x in enumerate(v_input)]

def exp(index: int):
x = v_input[index]
r = v_result[index]
return (x & 0xf3 | ~x & 0xc) - 20 == r

def get_result(index: int) -> int:
r = None
result = s.check()
if result == z3.sat:
rs = s.model()
r = rs[0]  # Get the final result key
r = rs[r].as_long()  # convert to value
else:
print(f'fail on {index}')
s.reset()
return r

key_mapper = [get_result(index) for index, x in enumerate(v_result)]
print(f'key_mapper:{key_mapper}')
```
• get key_mapper:[72, 73, 74, 75, 68, 69, 70, 71, 64, 65]

• It is found that in the final input judgment, only the item that is 0 in the current array is judged, that is, the input value is the inconsistent value of v_sudo and v_d0g3

• ```# Only fill in the position of 0 in d0g3, so that v_sudo == v_d0g3
is_invalid = -1
v_encoded = [v_sudo[index] if x == 0 else is_invalid for index,
x in enumerate(v_d0g3)]  # convert to input
v_encoded = list(filter(lambda x: x != is_invalid, v_encoded))
v_encoded = [key_mapper[x] for x in v_encoded]
v_encoded = [chr(x) for x in v_encoded]
print(f'v_encoded:{v_encoded}')
```
• Get the converted v_input v_encoded:['D', 'F', 'A', 'K', 'F', 'D', 'I', 'G', 'F', 'J', '@ ', 'A', 'D', 'F', '@', 'E', 'G', 'J', 'J', '@', 'D', 'K', 'E', 'E', 'F', 'I', 'K', 'G', 'J', 'I', 'A', '@', 'G', 'F', 'J', 'E ', 'E', 'A', '@', 'F']

• After finally passing it through key_mapper, press:

• 0-len/2-1 of v_input is interchanged with len/2-len
• v_input[2n] and v_input[2n+1] are interchanged
• The final exp is

• ```from typing import List
import z3
import struct

def convert(raw: str) -> List[int]:
raw = bytearray.fromhex(raw)
raw = [raw[x*4:(x+1)*4] for x in range(int(len(raw)/4))]
raw = [struct.unpack('<I', x)[0] for x in raw]
return raw

v_sudo = '010000000400000005000000030000000200000007000000060000000900000008000000080000000300000009000000060000000500000004000000010000000200000007000000060000000700000002000000080000000100000009000000050000000400000003000000040000000900000006000000010000000800000005000000030000000700000002000000020000000100000008000000040000000700000003000000090000000500000006000000070000000500000003000000020000000900000006000000040000000800000001000000030000000600000007000000050000000400000002000000080000000100000009000000090000000800000004000000070000000600000001000000020000000300000005000000050000000200000001000000090000000300000008000000070000000600000004000000'
v_d0g3 = '010000000000000005000000030000000200000007000000000000000000000008000000080000000000000009000000000000000500000000000000000000000200000000000000000000000700000000000000000000000100000000000000050000000000000003000000040000000900000000000000010000000000000000000000030000000000000000000000000000000100000000000000000000000700000000000000090000000000000006000000070000000000000003000000020000000900000000000000040000000800000000000000000000000600000000000000050000000400000000000000080000000000000009000000000000000000000004000000000000000000000001000000000000000300000000000000000000000200000001000000000000000300000000000000070000000000000004000000'
v_sudo = convert(v_sudo)
v_d0g3 = convert(v_d0g3)
print(f'v_sudo:{v_sudo}')
print(f'v_d0g3:{v_d0g3}')
s = z3.Solver()
v_result = [index + 48 for index, x in enumerate([0] * 10)]  # ascii to initialize numbers
v_input = [0] * len(v_result)
v_input = [z3.BitVec(str(index), 16) for index, x in enumerate(v_input)]

def exp(index: int):
x = v_input[index]
r = v_result[index]
return (x & 0xf3 | ~x & 0xc) - 20 == r

def get_result(index: int) -> int:
r = None
result = s.check()
if result == z3.sat:
rs = s.model()
r = rs[0]  # Get the final result key
r = rs[r].as_long()  # convert to value
else:
print(f'fail on {index}')
s.reset()
return r

key_mapper = [get_result(index) for index, x in enumerate(v_result)]
print(f'key_mapper:{key_mapper}')
# Only fill in the position of 0 in d0g3, so that v_sudo == v_d0g3
is_invalid = -1
v_encoded = [v_sudo[index] if x == 0 else is_invalid for index,
x in enumerate(v_d0g3)]  # convert to input
v_encoded = list(filter(lambda x: x != is_invalid, v_encoded))
v_encoded = [key_mapper[x] for x in v_encoded]
v_encoded = [chr(x) for x in v_encoded]
print(f'v_encoded:{v_encoded}')

result = v_encoded
vel = len(result)  # result_len
vehl = int(vel / 2) # result_half_len

for i in range(vehl):
(result[i], result[i+vehl]) = (result[i+vehl], result[i])

for i in range(0, vel-1, 2):
(result[i], result[i+1]) = (result[i+1], result[i])

print(''.join(result))

```

## other documents

• CTF Reverse - Commonly Used Reverse Tools Extraction code: pnbt

• Common usage

• Station B tutorial CTF training for a provincial team in China (reverse engineering part)

• A Chinese provincial team CTF training (reverse engineering part) (authorized) (1)
• Basic encryption methods such as XXTEA, Base64 exchange table
• Python library Z3 Constraint solving of equations, infinitives, etc.
• Basic fake jump instructions (dirty bytes)
• unnatural program flow
• Flatten program control flow
• OLLVM program flow (virtual machine shell) is difficult and generally not tested
• Press the X key to track in ida to find all references where Ty is w (that is, the type is written), which is usually the key position
• A Chinese provincial team CTF training (reverse engineering part) (authorized) (2)
• ollydb moves to remove the shell, upx is an example
• Reverse and custom dummy instructions for python
• use pycdc Extraction code: dorr decrypts the exe or pyc compiled by python
• Parse the instruction calls manually implemented with the py dictionary one by one
• Reverse of C++ compiled program
• A Chinese provincial team CTF training (reverse engineering part) (authorized) (3)
• simple modulo encryption
• base58 Look for a particularly large number, which is usually the identifier of the algorithm, or the find crypt plugin ctrl+alt+f that comes with ida7.7 and above
• A common key location is where there is a new memory allocation, which is usually a key location, or where there is a sudden return in the middle of a function
• Maze problem, just draw it carefully
• dynamic question
• Pay attention to the anti-debugging branch that will be executed, such as int 3, which needs to be skipped
• basic knowledge

More general practice of CTF reverse questions and common tools to download Refer to the content of this blog post: How to play the CTF reverse Reverse problem

## Related Reverse CTF Questions

Tags: Python security

Posted by Ludichrist on Wed, 18 May 2022 00:20:16 +0300