CTF Reverse-[Anxun Cup 2019]game-Use deflat to de-obfuscate conventional logic judgments

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

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