Symbolic Execution

Cheezing

Example 1 : Cracking a relatively simple binary

undefined8 main(void)

{
  int iVar1;
  size_t sVar2;
  long counter;
  undefined4 *encrypted_flag;
  char local_108 [256];
  
  puts("Welcome to CTFd+!");
  puts(
      "So far, we only have one challenge, which is one more than the number of databases we have.\n"
      );
  puts("Very Doable Pwn - 500 points, 0 solves");
  puts("Can you help me pwn this program?");
  puts("#include <stdio.h>\nint main(void) {\n    puts(\" Bye!\");\n    return 0;\n}\n");
  puts("Enter the flag:");
  fgets(local_108,256,stdin);
  sVar2 = strcspn(local_108,"\n");
  counter = 0;
  encrypted_flag = &DAT_00104060;
  local_108[sVar2] = '\0';
  do {
    iVar1 = FUN_00101230(encrypted_flag[counter]);
    if ((char)iVar1 != local_108[counter]) {
      puts("Incorrect flag.");
      return 0;
    }
    counter = counter + 1;
  } while (counter != 0x2f);
  # Flag 
  puts("You got the flag! Unfortunately we don\'t exactl y have a database to store the solve in...")
  ;
  return 0;
}

We know that our flag is 0x2f in size, and definitely performs a series of XOR operations (via FUN_00101230) on the encrypted_flag to compare it against our input.

int FUN_00101230(uint param_1)

{
  byte bVar1;
  uint uVar2;
  int iVar3;
  
  uVar2 = 0;
  iVar3 = 0;
  do {
    bVar1 = (byte)iVar3 & 0x1f;
    iVar3 = iVar3 + 1;
    param_1 = (param_1 * param_1 >> bVar1 | param_ 1 * param_1 << 0x20 - bVar1) * 0x1337 + 0x420133 7
              ^ uVar2;
    uVar2 = uVar2 + 0x13371337;
  } while (iVar3 != 0x20);
  return (param_1 >> 8) + (param_1 >> 0x10) + param_ 1 + (param_1 >> 0x18);
}

We can just specify our bad and good addresses in respect to disassembly in Ghidra.

import angr
import claripy

# Load the binary with PIE enabled
project = angr.Project("./ctfd_plus", main_opts={'base_addr': 0}, auto_load_libs=False)

 
# Create the initial state of the binary
state = project.factory.full_init_state(args=["./challenge_binary"])

simgr = project.factory.simgr(state)

puts_success_offset = 0x1127  # Address of success 'puts("You got the flag...")' relative to base
puts_failure_offset = 0x1117  # Address of failure 'puts("Incorrect flag.")' relative to base

# Add success and failure addresses to simulation manager
simgr.explore(find=puts_success_offset, avoid=puts_failure_offset)
# Print the number of found states
print(f"Number of found states: {len(simgr.found)}")

# Print the input and output for each found state
for i, state in enumerate(simgr.found):
    input_data = state.posix.dumps(0)   
    output_data = state.posix.dumps(1)   
    print(input_data)
    print(output_data)
    
# Number of found states: 1
# Input for found state 0: lactf{m4yb3_th3r3_1s_s0m3_m3r1t_t0_us1ng_4_db}