Crackme overview#

The simple crackme is a very simple program, it reads a password from stdin and show whether it is correct or wrong. When analyzed with IDA, a quick overview on the graph mode reveals that the stdin buffer (rsp + 0x20) goes through a loop that xor’s each input byte, and then compare with it with the string “password”. In other words, the correct password is a string that, after some operations, is transformed into “password”.

Below is a list of the instructions and their addresses:

Solver#

In order to solve this crackme, i wrote a Triton script in Python, emulating the program execution and symbolizes the input buffer. In addition, I used taint analysis to monitor whether the program reads from or writes to the first byte of the buffer. In order to better understand better how the program manipulate the input. Below, I explain each function of the script, you can view the complete script here.

After initializing the Triton context, I used the lief library to parse the binary and called loadBinary to load its sections into memory.

1
def loadBinary(ctx, binary):
2
    for sec in binary.sections:
3
        ctx.setConcreteMemoryAreaValue(
4
            sec.virtual_address,
5
            list(sec.content)
6
        )
7
        print(f"[+] Loading"
8
              f" {hex(sec.virtual_address)} - {hex(sec.virtual_address + sec.virtual_size)}"
9
              f" {sec.name}")

Then, I called the setup function to configure the stack, populate the input buffer, and taint the first byte. RSP is a global variable with an arbitrary value of 0x7ffffff0, note that the buffer address is the same as the one identified during static analysis in IDA, rsp + 0x20.

After setting the rsp and rbp registers, a loop is executed to populate each byte with a dummy value (0x41, which corresponds to ‘A’ in the ASCII table). Each byte is then symbolized to inform Triton to monitor operations on this memory address, an alias is set to facilitate debugging, and to finish, taintMemory is used to taint the byte at BUFFER_ADDR.

1
RSP = 0x7ffffff0
2
BUFFER_ADDR = RSP + 0x20
3
BUFFER_SIZE = 8
4

5
...
6

7
def setup(ctx):
8
    ctx.setConcreteRegisterValue(ctx.registers.rsp, RSP)
9
    ctx.setConcreteRegisterValue(ctx.registers.rbp, RSP)
10

11
    addr = BUFFER_ADDR
12
    for i in range(BUFFER_SIZE):
13
        ctx.setConcreteMemoryValue(addr, 0x41)
14
        sym = ctx.symbolizeMemory(MemoryAccess(addr, CPUSIZE.BYTE))
15
        sym.setAlias(f"input_{i}")
16
        addr += 1
17

18
    ctx.taintMemory(BUFFER_ADDR)

The run function receives the address from which the program should start execution. I chose 0x1081 to skip the binary initialization code and avoid having to hook operating system functions, allowing me to focus on the part where the input is transformed. You can check the addresses and instructions in the screenshots at the beginning of the article.

The condition of the while loop is that the program counter (pc) is less than or equal to the maximum address of the .text section, obtained from the loadBinary function. Each instruction retrieved from the pc address is emulated using ctx.processing(inst).

If the instruction reads from or writes to memory that has been tainted, it is printed to the console. The program is emulated until CHECK_ADDR is executed, just before the comparison, because by then the input has already been transformed. At this point, Triton knows all the operations that have been executed on the input.

1
START_ADDR  = 0x1081
2
CHECK_ADDR  = 0x10C8
3

4
...
5

6
def run(ctx, pc):
7
    while pc <= 0x211c:
8
        inst = Instruction(pc, ctx.getConcreteMemoryAreaValue(pc, 15))
9
        ctx.processing(inst)
10

11
        if inst.isTainted():
12
            print("[tainted] %s" % inst.getDisassembly())
13

14
        if inst.getAddress() == CHECK_ADDR:
15
            solve(ctx)
16
            break
17

18
        pc = ctx.getConcreteRegisterValue(ctx.registers.rip)

Finally, the solve function iterates over each symbolized byte and queries Triton for the value it must have to match the corresponding character in the PASSWORD variable.

1
PASSWORD = b"password"
2

3
...
4

5
def solve(ctx):
6
    result = ""
7
    for k, v in enumerate(PASSWORD):
8
        input = ctx.getSymbolicMemory(BUFFER_ADDR+k).getAst()
9
        model = ctx.getModel(input == v)
10
        value = next(iter(model.values())).getValue()
11
        result += chr(value)
12
    print("-------------------")
13
    print("Password: %s" % result)

At execute this script, it show the sections loaded, tainted instructions and the correct password.

Source code.