---
# System prepended metadata

title: PICO CTF WRITEUP

---

# PicoCTF 2024 - Classic Crackme 0x100

## Challenge presentation
We are given the following prompt and a link to get the file:

> A classic Crackme. Find the password, get the flag!. Crack the Binary file locally and recover the password. Use the same password on the server to get the flag!

When we run the command `file`, we get the following output:

```bash
└─$ file crackme100    
crackme100: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=4c56306c51af336d758655e03368b457f2f4c356, for GNU/Linux 3.2.0, with debug_info, not stripped
```

The most important things we should focus on are the following:
1. **64-bit ELF executable**: This tells us that the binary is an Executable and Linkable Format file designed for 64-bit architectures.
2. **Dynamically linked with debugging information**: The binary uses shared libraries at runtime.
3. **Not stripped**: The presence of symbol tables with function and variable names can help us reverse this.

After giving it the execute permission using `chmod +x crackme100`, we can run it:

```bash
└─$ ./crackme100         
Enter the secret password: :)
FAILED!
```

We should proceed by opening the file in `Ghidra` or another decompiler to see what we are dealing with. If we go to the `main` function, we can see that variables are initialized with some hexadecimal values which may be encoded data:

```c
  local_68 = 0x687a63616a697061;
  local_60 = 0x676a796e6674677a;
  local_58 = 0x6d626a7271766472;
  local_50 = 0x7a636a6d63727563;
  local_48 = 0x6c65646777627673;
  local_40 = 0x796b6a78787876;
  uStack_39 = 0x796769;
```

Then the program prompts for a password and reads our input into a buffer (which will be used for a comparison later on):

```c
  printf("Enter the secret password: ");
  __isoc99_scanf(&DAT_00402024,local_a8);
```

Then, some transformations operations are being performed on our input:

```c
  for (; local_c < 3; local_c = local_c + 1) {
    for (local_10 = 0; local_10 < local_14; local_10 = local_10 + 1) {
      local_28 = (local_10 % 0xff >> 1 & local_18) + (local_10 % 0xff & local_18);
      local_2c = ((int)local_28 >> 2 & local_1c) + (local_1c & local_28);
      iVar1 = ((int)local_2c >> 4 & local_20) +
              ((int)local_a8[local_10] - (int)local_21) + (local_20 & local_2c);
      local_a8[local_10] = local_21 + (char)iVar1 + (char)(iVar1 / 0x1a) * -0x1a;
    }
  }
```

Finally, at the end, we see the condition for printing the flag:

```c
  iVar1 = memcmp(local_a8,&local_68,(long)local_14);
  if (iVar1 == 0) {
    printf("SUCCESS! Here is your flag: %s\n","picoCTF{sample_flag}");
  }
  else {
    puts("FAILED!");
  }
```

So, in order to get the flag locally,  we need to find an input that, after being transformed by the program, matches the sequence stored in local_68 and the following variables. However, it is clear that manually deducing the correct password would be  time-consuming and not fun. In order to do avoid this, we can automate the process of finding the correct input by using `angr`.

## What's angr?

`angr` is an open-source binary analysis platform for Python that is built on the concept of _symbolic execution_. What this means is that `angr` doesn't run the binary with real inputs; instead, it looks at many ways at once by treating some inputs as symbols whose values are unknown. 

Essentially, we create a symbol that represents the password we're looking for: its value is unknown at first. This password must meet certain constraints as we go through the binary. These criteria add constraints to our symbol, narrowing the password. After finding a path to this desired conclusion, `angr` works backward, applying all its restrictions to determine the symbol (our password).

To run a successful symbolic execution, `angr` relies on four dependencies:
- `cle`, which is a binary loader, preparing it for analysis;
- `pyvex`, which acts as an instruction emulator and translates binary code into an intermediate representation;
- `claripy`, which enables us to make BitVector objects which are important for symbolic analysis;
- `z3` which is a sat solver and is used to solve complex logical conditions.

So, `cle` prepares the binary for inspection, `pyvex` translates its machine code into an intermediate representation for analysis, `claripy` creates and manipulates symbolic variables for exploring program states, and `z3` solves complex logical conditions during analysis to find paths that meet the given criteria.

`angr` also uses a simulation manager to explore and manage the program, by keeping track of all the explored paths. The symbols are stored in BitVectors, each with its own set of rules and size.
## Using angr to solve Crackme
Installation is easy and can be done by using Python's package manager `pip`. After the installation we are ready to write the Python script. 

We should set up an initial state that indicates the point of entry. We pass this to the simulation manager and explore until either the desired state is reached or all states terminate.
First, we need to load our challenge binary and define the initial state:

```python
import angr
import claripy

binary_path = "crackme100"
proj = angr.Project(binary_path)
state = proj.factory.entry_state()

```
Now, we should use the simulation manager to explore the binary. We are looking for a path to when the flag is being printed. This happens at address `0x00401378` in Ghidra. We also can specify the path we want to avoid, which is the failure one, at `0x00401389

```python
simgr.explore(find = 0x00401378, avoid = 0x00401389)
```

When `angr` finds a satisfying path, it stores the state in a list. To access the input that led to this, we look into the first item of this list:

```python
if simgr.found:
	found_state = simgr.found[0]
	print("Found a path to the target address:", simgr.found[0].posix.dumps(0))
```

The function `posix.dumps(0)` helps retrieve the content from the simulated program’s standard input.
### Complete code
Here's the entire code snippet for readability:

```python
import angr
import claripy

binary_path = "crackme100"
proj = angr.Project(binary_path)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x00401378, avoid = 0x00401389) 

if simgr.found:
	found_state = simgr.found[0]
	print("Found a path to the target address:", simgr.found[0].posix.dumps(0))
```

### Result
After running the python script, we get the following output:

```
Found a path to the target address: b'amf~xwtyw{n\xc1hpauoxphl{sawli\xbbd^qkppvn{uv`pool{_m@{p'
```

The script outputs a byte string with escape sequences for non-printable characters. Binary analysis commonly involves non-textual data, and to keep and use this data we should save the output into a file. This helps make sure that all bytes, including non-printable ones, are captured and passed to the `Crackme`.

```bash
└─$ printf 'amf~xwtyw{n\xc1hpauoxphl{sawli\xbbd^qkppvn{uv`pool{_m@{p' > correctinput.txt
```

If we now pass the contents of this file to the `Crackme`:

```bash
./crackme100 < correctinput.txt 
Enter the secret password: SUCCESS! Here is your flag: picoCTF{sample_flag}
```

All that is left is running the challenge on the server and we get the real flag.

```bash
└─$ nc titan.picoctf.net 63926 < correctinput.txt 
Enter the secret password: SUCCESS! Here is your flag: picoCTF{s0lv3_angry_symb0ls_e1ad09b7}
```
