Elementary(rev, warmup) - Confidence 2019

elementary.md

Search in IDA for mov eax, 0 and exclude from results those occuring in main function. (Let's save all this in a file named step1)

Then filter the information from step1 to extract only addresses, For example, using this command:

awk '{ print $1 }' step1 | cut -d':' -f2 > avoid_addr

Then use angr script to find a solution.

import angr
import claripy

# angr uses 0x400000 as base address for PIE executables

START = 0x40071a # start of main
FIND  = 0x40077f # Good job message basic block
AVOID = [0x400786] # Wrong messages bassic block
with open("avoid_addr", "r") as fin:
    for l in fin:
        # add other addresses to avoid, all those "mov eax, 0"
        AVOID.append(0x400000 + int(l.strip(), 16))

BUF_LEN = 104


def char(state, c):
    return state.solver.And(c <= '~', c >= ' ')


def main():
    p = angr.Project("elementary")

    flag = claripy.BVS('flag', BUF_LEN * 8)
    state = p.factory.blank_state(addr=START, stdin=flag)

    for c in flag.chop(8):
        state.solver.add(char(state, c))

    ex = p.factory.simulation_manager(state)
    ex.use_technique(angr.exploration_techniques.Explorer(find=FIND, avoid=AVOID))

    ex.run()

    return ex.found[0].posix.dumps(0).decode("utf-8")


if __name__ == '__main__':
    print("flag: {}".format(main()))

Profit: flag: p4{I_really_hope_you_automated_this_somehow_otherwise_it_might_be_a_bit_frustrating_to_do_this_manually}

(I assume that you're asking about the program we we're given to analyse, If you're asking what the Python script does, then I recommend to read about symbolic execution and constraint solving(ex: SMT solvers)).

In simple and short terms, the program reads input(a password), then each character is checked(at a granularity of bits, it verifies bits of each character to be more precise) if it satisfies a condition. If a condition is not satisfied, the execution is terminated, otherwise next check is executed and so until the password is correct.

I hope I made it a bit clearer. :)

oh, thank you!
i assumed that at the first place but, i found it hard to understand the disassembly of those functions, i've never seen that before(checking bits of a long string)

I've tested your script with angr version 8.20.6.8. I had to raise BUF_LEN to 128, leading to a bit vector of 1024 bits. Otherwise, angr just stops during the scanf with an unsatisfied state. Any clue why this would happen?

Edit: it's 1024, not 992

Hey,
I guess you raised the length to 124 (* 8 = 992) not 128 or ?
But I'm not sure what exactly may be the issue in this case. I tend to believe that something change in angr's internals. Maybe it's related to https://reverseengineering.stackexchange.com/questions/19164/problem-with-scanf-fgets-in-angr-stdin-exploration

Sorry I cannot give a clear answer. :/

Thanks for the reply. I had a typo in the total, it's 1024 bits. It does seem suspiciously well-rounded, I guess this would require a closer look at that scanf implementation. The solution space should fit in your original size, since it ends with <SimulationManager with 1 found, 713 avoid>.