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

Answer: KDEEIFGKIJ@AFGEJAEF@FDKADFGIJFA@FDE@JG@J

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
        s.add(exp(index))
        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
        s.add(exp(index))
        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))
    
    

  • Get an answer KDEEIFGKIJ@AFGEJAEF@FDKADFGIJFA@FDE@JG@J

other documents

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

• Common usage

  • Use python to quickly handle encryption algorithms (RSA, AES, DES, 3DES, XXTEA, blowfish)
  • How to use the struct library in Python

• 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

  • big and small endian

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

• Python

  • Python disassembly method Python pyc bytecode decompilation and disassembly related knowledge
  • [CTF Reverse- Yangcheng Cup 2020]Bytecode-WP-Python bytecode decompilation

• Remote debugging assembly

  • CTF reverse-[watevrCTF ​​2019]Timeout-WP-remote debugging and modifying the current running location of the program RIP
  • CTF reverse-[watevrCTF ​​2019]esreveR-seems like a complex process, finds the core logic, derives the values ​​in the stack and registers according to the 64-bit architecture to get the result

• Process control

  • CTF reverse-Dig the way Interesting Pointer-overwrite variables through stack overflow to achieve the purpose of modifying the execution process

• Reverse Thinking

  • [CTF Reverse- NPUCTF2020]Baby Obfuscation-Script writing with reverse thinking and logical understanding of the meaning of functions
  • [CTF Reverse- MRCTF2020] EasyCpp - Reverse Generic Manipulation Method for C++ Types
  • [CTF Reverse- SUCTF2018]babyre-WP-cpp simple iteration and blasting of output values ​​by table

• android

  • [CTF Reverse- Net Ding Cup 2020 Qinglong Group]bang-Android shelling reverse: frida-dexdump export to get the source code

• virtual machine

  • [CTF Reverse- GWCTF 2019]babyvm-WP-virtual machine simulation process reverse coding and use of z3 constraint solver to solve equation tools
  • [CTF Reverse- WMCTF2020]easy_re-WP_virtual machine-perl loader interception

• Anti-debugging and SMC

  • [CTF Reverse- SCTF2019]creakme-WP-protection based on AES encryption algorithm: anti-debugging and except_handler and SMC
  • CTF Reverse - [FlareOn1] Shellololol - Executed on the stack, the movement of the multi-layer smc gets the final result

• encryption

  • Based on pycryptodome, Python implements the use of commonly used encryption algorithms such as AES, DES, 3DES, and RSA. The source code examples of various encryption are attached at the end of the article.
  • [CTF Reverse- FlareOn2]very_success-WP_rol cyclic displacement encryption
  • base64 table conversion
    • [CTF Reverse- CISCN2018]2ex-WP_mips-32 architecture and base64 exchange table
    • [CTF Reverse- De1CTF2019]Re_Sign - Depth Algorithm Tracking for Simple Unpacking and base64 Conversion Table Encoding

• flower instruction

  • [CTF Reverse- SCTF2019]babyre-WP_Simple to spend instructions and process identification
  • CTF Reverse-[MRCTF2020]VirtualTree-Constantly established jz flower instruction removal and smc transformation application of the original execution process on the binary tree, writing scripts through reverse thinking to solve the problem

• Flattening of process confusion

  • [CTF Reverse- RoarCTF2019]polyre-WP_Control flow flattening to de-obfuscate idcpy de-instruction
  • CTF Reverse-[SUCTF2019]hardcpp-Use optimized deflat.py to handle obfuscated control flow and parse cpp's lambda to get actual processing logic

• c/cpp basics

  • [CTF Reverse- b01lers2020]little_engine-cpp basic function usage and key points of byte type