# Symbolic Execution

### Example 1 :  Cracking a relatively simple binary

```cpp
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.

```cpp
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.

```python
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}
```


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://xenon-2.gitbook.io/writeups/binary-exploitation/symbolic-execution.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.