Hack-a-Sat 4 Qualifiers Writeups

import base64
import glob
from tqdm.auto import tqdm

from z3 import *

def get_immediate(x):
    # convert constants to BitVec e.g. w2c_i0 = 16ull;` => 16 in BitVec
    return BitVecVal(int(x.partition("=")[2].strip("ul; ")), 32)

def solve_binary(filename):
    wasmpath = f"./as-below/{filename}"
    cpath = f"{wasmpath}.c"

    # Decompile to c
    !wasm2c $wasmpath > $cpath
    lines = open(cpath, "r").read().split("\n")
    !rm $cpath

    # Read file and extract lines of w2c_quick_maths
    lines = lines[lines.index("static u32 w2c_quick_maths(Z__instance_t* instance, u32 w2c_p0) {"):]
    lines = lines[:lines.index("}")]

    # Jump to known prologue
    lines = lines[lines.index("  w2c_i0 = instance->w2c_g0;"):]
    head = [
        '  w2c_i0 = instance->w2c_g0;',
        '  w2c_l1 = w2c_i0;',
        '  w2c_i0 = 16u;',
        '  w2c_l2 = w2c_i0;',
        '  w2c_i0 = w2c_l1;',
        '  w2c_i1 = w2c_l2;',
        '  w2c_i0 -= w2c_i1;',
        '  w2c_l3 = w2c_i0;',
    ]
    assert lines[:len(head)] == head
    lines = lines[len(head):]

    # extract operations and check
    operations = list(zip(lines[8::12], lines[12::12]))[:-2]
    check = lines[0]

    # solve for input
    xref = BitVec("x", 32)
    x = xref
    for y, op in operations:
        y = get_immediate(y)
        if "+=" in op:
            x = x + y
        elif "-=" in op:
            x = x - y
        elif "*=" in op:
            x = x * y
        elif "DIV_U" in op:
            x = UDiv(x, y) # flooring integer division, not floating point
        elif "<<=" in op:
            x = x << y
        elif ">>=" in op:
            x = LShR(x, y) # u32 is used, bitshift is logical
        else:
            raise ValueError()
    s = Solver()
    s.add(x == get_immediate(lines[0]))
    assert str(s.check()) == "sat"

    soln = s.model()[xref].as_long()
    solnb64 = base64.b64encode(str(soln).encode()).decode()
    return soln, solnb64

for f in tqdm(sorted(glob.glob("as-below/*"))):
    binary = f.partition("/")[2]
    ans = solve_binary(binary)
    assert ans
    print(f, ans)

from pwn import *

r = remote("as_below.quals2023-kah5aiv9.satellitesabove.me", 5300)
r.sendline(b"ticket{xray767199juliet4:GPvf2Y6YNUCiazDTbJkdshfXx4DJRekMIesXKNYA_uy7xSpWhtxXDl8fOUwbuqHePQ}")
r.recvuntil(b"send your solution as base64, followed by a newline\n")

# post-hoc info that there is 10 testcases
for _ in tqdm(range(10)):
    binary = r.recvline().decode().partition("\t")[0]
    r.sendline(solve_binary(binary)[1].encode())
print(r.recvline())
print(r.recvline())

#!/usr/bin/env bash
image_name=hyde-street:latest
submission_path=$(pwd)/submission.ts
container_name=$(docker create --rm --env "FLAG=${flag}" --env "SEED=${seed}" $image_name)
docker cp "$submission_path" "$container_name:/submission.ts"
docker start --attach "$container_name"

import { BufReader } from "https://deno.land/std@0.178.0/io/buf_reader.ts";

// Helper functions
const decoder = new TextDecoder();
const dec = (t: Uint8Array) => decoder.decode(t);
const encoder = new TextEncoder();
const enc = (t: string) => encoder.encode(t);
const errLog = (t: Object) =>
  Deno.stderr.writeSync(enc(Deno.inspect(t) + "\n"));

const bufReader = new BufReader(Deno.stdin);
// Read in number of bytes to load the maze grid
const mazeNBytes = +dec((await bufReader.readLine()).line);
// errLog(mazeNBytes);
// Read in the maze grid
const mazeBuf = new Uint8Array(mazeNBytes);
await bufReader.read(mazeBuf);
const maze = dec(mazeBuf);
// errLog(maze);

// Extract grid landmarks
const grid = maze.split("\n").map((row) => row.split(""));
const [r, c] = [grid.length, grid[0].length];
// errLog(`r:${r}, c:${c}`)
let [sy, sx, fy, fx] = [-1, -1, -1, -1];
for (const y in grid) {
  for (const x in grid[y]) {
    const cell = grid[y][x];
    if (cell == "S") (sy = +y), (sx = +x);
    if (cell == "F") (fy = +y), (fx = +x);
  }
}
// errLog(`s:(${sy},${sx}), f:(${fy},${fx})`)

// Adjacency
const d4: [number, number, string, string][] = [
  [0, 1, "E", "W"],
  [0, -1, "W", "E"],
  [1, 0, "S", "N"],
  [-1, 0, "N", "S"],
];

// Flood fill maze solving
type Breadcrumb = [number, number, string];
const flood: (Breadcrumb | null)[][] = grid.map((r) => r.map((c) => null));
function dfs(y: number, x: number, breadcrumb: Breadcrumb) {
  if (y < 0 || y >= r) return;
  if (x < 0 || x >= c) return;
  if (flood[y][x] !== null) return;
  if (grid[y][x] === "X") return;

  flood[y][x] = breadcrumb;
  for (const [dy, dx, fwd, rev] of d4) {
    const ny = y + dy;
    const nx = x + dx;
    dfs(ny, nx, [y, x, fwd]);
  }
}

dfs(sy, sx, [sy, sx, "?"]);
// errLog(flood);
for (const y in grid) {
  errLog(flood[y].map((cell) => (cell || [0, 0, "#"])[2]).join(""));
}

// Backtrack to get the solve path
const backtrack: string[] = [];
while (fy != sy || fx != sx) {
  const [ny, nx, fwd] = flood[fy][fx] as Breadcrumb;
  [fy, fx] = [ny, nx];
  backtrack.push(fwd);
}
backtrack.reverse();
const solution = backtrack.join("");
errLog(solution);

// Submit to grader
console.log(solution);

require 'digest'
require 'fileutils'
require 'logger'
require 'json'
require 'set'

UINT32_MAX = 0xffffffff

NUMBER_TO_GENERATE = 10

def num_in_range(op)
  case op
  when :/
    rand(2..16)
  when :*
    rand(2..32)
  when :-
    rand(0..256)
  when :+
    rand(0..16384)
  else
    fail "couldn't num_in_range for #{op}"
  end
end


FileUtils.mkdir_p "challs"

dest = File.join __dir__, 'src', 'quick_maths.c'

NUMBER_TO_GENERATE.times do |n|
  out_f = File.open dest, 'w'

  out_f.puts <<~EOS.strip
  #include <stdint.h>
  #include <stdbool.h>

  bool quick_maths(uint32_t run) {
  EOS

  want = rand(0..UINT32_MAX)
  run = want

  rand(10..20).times do
    stmt = nil
    result = nil

    loop do
      # skipping multiplication for now; idiv vs. fdiv ;_;
      operation = %i{+ - /}.sample
      operand = num_in_range(operation)

      result = run.send operation, operand

      # next here loops again
      next if result >= UINT32_MAX
      next if result <= 0

      stmt = "run = run #{operation} #{operand};"
      stmt += " // #{result}" if ENV['CHALLENGE_DEV_DEBUG']
      break
    end

    out_f.puts stmt
    run = result
  end


  out_f.puts <<~EOS.strip
  return (run == #{ run });
  }
  EOS

  out_f.close

  `make clean all`


  size = `wc -c build/ominous_etude`.split[0].to_i
  digest = `sha256sum build/ominous_etude`.split[0]

  new_omen_name = "generated"
  FileUtils.mv 'build/ominous_etude', "challs/#{new_omen_name}"
  FileUtils.mv dest, "challs/#{new_omen_name}.c"

  $stderr.puts JSON.dump({
    'sha256' => digest,
    'size' => size,
    'answer' => want.to_s
  })

  got = nil


  IO.popen("deno run --no-remote --allow-read=/chall/challs/generated,/chall/challs/generated.c --allow-env=SOLVER_DEBUG /submission.ts #{new_omen_name}",
    'r+',
    # should redirect child stderr to my stdout
    :err => :out) do |line|
      got = line.gets
      line.close
  end

  puts got
  puts got.to_i == want

  IO.popen("/chall/challs/#{new_omen_name}", 'w+', :err => :out) do |result|
    result.puts got
    puts result.gets
    puts did_get = result.gets.strip
    result.close
    unless "cool :)" == did_get
      puts result.puts
      puts "got a wrong answer"
      exit 1
    end
  end
end

puts ENV['FLAG'] || "no flag set in environment"

#!/usr/bin/env bash
image_name=hyde-street:latest
submission_path=$(pwd)/submission.ts
container_name=$(docker create --rm --env "FLAG=${flag}" --env "SEED=${seed}" $image_name)
docker cp "$submission_path" "$container_name:/submission.ts"
docker start --attach "$container_name"

// Helper functions
const decoder = new TextDecoder();
const dec = (t: Uint8Array) => decoder.decode(t);
const encoder = new TextEncoder();
const enc = (t: string) => encoder.encode(t);
const errLog = (t: Object) =>
  Deno.stderr.writeSync(enc(Deno.inspect(t) + "\n"));

// Load source file
const generatedC = await Deno.readTextFile("/chall/challs/generated.c");
const sourceLines = generatedC.split("\n");

// Parse operations
const operations: [string, number][] = [];
let checkValue = -1;
for (let sourceLine of sourceLines) {
  // errLog(sourceLine);

  const checkValueMatch = /return \(run == (\d+)\);/g.exec(sourceLine);
  if (!!checkValueMatch) {
    checkValue = +checkValueMatch[1];
  }

  const operationMatch = /run = run (.) (\d+);/g.exec(sourceLine);
  if (!!operationMatch) {
    const op = operationMatch[1];
    const y = +operationMatch[2];
    operations.push([op, y]);
  }
}

errLog("operations:");
errLog(operations);
errLog("checkValue:");
errLog(checkValue);

// Backtrack
let current = checkValue;
operations.reverse();
for (const [op, y] of operations) {
  switch (op) {
    case "+":
      current -= y;
      break;
    case "-":
      current += y;
      break;
    case "/":
      current *= y;
      break;
  }
}
errLog("solution: " + current);
console.log(current);

#!/usr/bin/env bash
image_name=so-above:challenge
submission_path=$(pwd)/lag.ts
container_name=$(docker create --rm --env "FLAG=${flag}" --env "SEED=${seed}" $image_name)
echo "await new Promise((resolve) => { setTimeout(resolve, 60000); })" > $submission_path
docker cp "$submission_path" "$container_name:/submission.ts"
docker start "$container_name"
sleep 1
mkdir -p $(pwd)/leak-challs
docker cp "$container_name:/chall/challs/generated" "$(pwd)/leak-challs/generated"
docker cp "$container_name:/chall/challs/generated.c" "$(pwd)/leak-challs/generated.c"
docker kill "$container_name"

import iced from "npm:iced-x86@1.18.0";
import elfinfo from "npm:elfinfo@0.4.0-beta";
import predicates from "npm:@tool-belt/type-predicates@1.2.2";

// Helper functions
const decoder = new TextDecoder();
const dec = (t: Uint8Array) => decoder.decode(t);
const encoder = new TextEncoder();
const enc = (t: string) => encoder.encode(t);
const errLog = (t: Object) =>
  Deno.stderr.writeSync(enc(Deno.inspect(t) + "\n"));

// For server
// const binary = await Deno.readFile("/chall/challs/generated")
// For local testing
const binary = await Deno.readFile("./leak-challs/generated");
const elfdata = await elfinfo.open(binary);
errLog(Object.keys(elfdata.elf));

const sections = elfdata.elf?.sections as elfinfo.ELFSection[];
const symtab = sections.find((x) => x.name === ".symtab") as elfinfo.ELFSection;
const rodata = sections.find((x) => x.name === ".rodata") as elfinfo.ELFSection;
errLog(Object.keys(symtab));

const rodataCode = binary.slice(
  Number(rodata.addr) + 0x40,
  Number(rodata.addr) + rodata.size
);
const rodataBuf = new ArrayBuffer(rodataCode.length);
const rodataBytes = new Uint8Array(rodataBuf);
const rodataDoubles = new Float64Array(rodataBuf);
rodataCode.forEach((x, i) => (rodataBytes[i] = x));
errLog(rodataDoubles);

const quickmathsSym = (symtab as any).symbols.find(
  (x) => x.name === "quick_maths"
);
const quickmathsCode = binary.slice(
  Number(quickmathsSym.value),
  Number(quickmathsSym.value) + quickmathsSym.size
) as Uint8Array;

const instrDecoder = new iced.Decoder(
  64,
  quickmathsCode,
  iced.DecoderOptions.None
);
const instructions = instrDecoder.decodeAll();
const formatter = new iced.Formatter(iced.FormatterSyntax.Nasm);

for (const instructionIdx in instructions) {
  const instr = instructions[instructionIdx];
  const disasm = formatter.format(instr);
  errLog(disasm);
}

const operations: [string, number][] = [];
let checkValue = -1;
let nextY = -1;

for (const instructionIdx in instructions) {
  const instr = instructions[instructionIdx];
  const disasm = formatter.format(instr);

  const relativeMemoryLoadMatch = /xmm[01],\[rel ([0-9A-F]{4})h\]/g.exec(
    disasm
  );
  if (!!relativeMemoryLoadMatch) {
    const operationIdx = operations.length;
    const nextYIdx = (parseInt(relativeMemoryLoadMatch[1], 16) - 0xe77) / 8;
    nextY = rodataDoubles[nextYIdx];
  }

  const operationMatch = /(add|sub|div)sd/g.exec(disasm);
  if (!!operationMatch) {
    switch (operationMatch[1]) {
      case "add":
        operations.push(["+", nextY]);
        break;
      case "sub":
        operations.push(["-", nextY]);
        break;
      case "div":
        operations.push(["/", nextY]);
        break;
    }
  }
}
checkValue = rodataDoubles[rodataDoubles.length - 1];

errLog("operations:");
errLog(operations);
errLog("checkValue:");
errLog(checkValue);

let current = checkValue;
operations.reverse();
for (const [op, y] of operations) {
  switch (op) {
    case "+":
      current -= y;
      break;
    case "-":
      current += y;
      break;
    case "/":
      current *= y;
      break;
  }
}
console.log(current);

#!/usr/bin/env bash
image_name=so-above:challenge
submission_path=$(pwd)/submission.ts
container_name=$(docker create --rm --env "FLAG=${flag}" --env "SEED=${seed}" $image_name)
docker cp "$submission_path" "$container_name:/submission.ts"
docker start --attach "$container_name"

import iced from "npm:iced-x86@1.18.0";
import elfinfo from "npm:elfinfo@0.4.0-beta";
import predicates from "npm:@tool-belt/type-predicates@1.2.2";

// Helper functions
const decoder = new TextDecoder();
const dec = (t: Uint8Array) => decoder.decode(t);
const encoder = new TextEncoder();
const enc = (t: string) => encoder.encode(t);
const errLog = (t: Object) =>
  Deno.stderr.writeSync(enc(Deno.inspect(t) + "\n"));

// For server
const binary = await Deno.readFile("/chall/challs/generated");
// For local testing
// const binary = await Deno.readFile('./leak-challs/generated');
const elfdata = await elfinfo.open(binary);
// errLog(Object.keys(elfdata.elf));

const sections = elfdata.elf?.sections as elfinfo.ELFSection[];
const symtab = sections.find((x) => x.name === ".symtab") as elfinfo.ELFSection;
const rodata = sections.find((x) => x.name === ".rodata") as elfinfo.ELFSection;
// errLog(Object.keys(symtab));

const rodataCode = binary.slice(
  Number(rodata.addr) + 0x40,
  Number(rodata.addr) + rodata.size
);
const rodataBuf = new ArrayBuffer(rodataCode.length);
const rodataBytes = new Uint8Array(rodataBuf);
const rodataDoubles = new Float64Array(rodataBuf);
rodataCode.forEach((x, i) => (rodataBytes[i] = x));
// errLog(rodataDoubles);

const quickmathsSym = (symtab as any).symbols.find(
  (x) => x.name === "quick_maths"
);
const quickmathsCode = binary.slice(
  Number(quickmathsSym.value),
  Number(quickmathsSym.value) + quickmathsSym.size
) as Uint8Array;

const instrDecoder = new iced.Decoder(
  64,
  quickmathsCode,
  iced.DecoderOptions.None
);
const instructions = instrDecoder.decodeAll();
const formatter = new iced.Formatter(iced.FormatterSyntax.Nasm);

const operations: [string, number][] = [];
let checkValue = -1;
let nextY = -1;

for (const instructionIdx in instructions) {
  const instr = instructions[instructionIdx];
  const disasm = formatter.format(instr);
  // errLog(disasm);

  const relativeMemoryLoadMatch = /xmm[01],\[rel ([0-9A-F]{4})h\]/g.exec(
    disasm
  );
  if (!!relativeMemoryLoadMatch) {
    const operationIdx = operations.length;
    const nextYIdx = (parseInt(relativeMemoryLoadMatch[1], 16) - 0xe77) / 8;
    nextY = rodataDoubles[nextYIdx];
  }

  const operationMatch = /(add|sub|div)sd/g.exec(disasm);
  if (!!operationMatch) {
    switch (operationMatch[1]) {
      case "add":
        operations.push(["+", nextY]);
        break;
      case "sub":
        operations.push(["-", nextY]);
        break;
      case "div":
        operations.push(["/", nextY]);
        break;
    }
  }
}
checkValue = rodataDoubles[rodataDoubles.length - 1];

errLog("operations:");
errLog(operations);
errLog("checkValue:");
errLog(checkValue);

let current = checkValue;
operations.reverse();
for (const [op, y] of operations) {
  switch (op) {
    case "+":
      current -= y;
      break;
    case "-":
      current += y;
      break;
    case "/":
      current *= y;
      break;
  }
}
console.log(current);