meithecatte

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

open import HoTT-UF-Agda

ℍ' : {X : 𝓤 ̇ } (x : X) (B : (y : X) → x ＝ y → 𝓥 ̇ )
   → B x (refl x)
   → (y : X) (p : x ＝ y) → B y p
ℍ' {X = X} x B b y p = 𝕁 X A f x y p B b
  where
  A : (x' y' : X) → x' ＝ y' → _

meithecatte

%define is_gpr(r) \
    (%isidni(r, ax) || %isidni(r, cx) || %isidni(r, dx) || %isidni(r, bx) || \
     %isidni(r, sp) || %isidni(r, bp) || %isidni(r, si) || %isidni(r, di))

%define num_gpr(r) \
    (0*%isidni(r, ax) + 1*%isidni(r, cx) + 2*%isidni(r, dx) + 3*%isidni(r, bx) + \
     4*%isidni(r, sp) + 5*%isidni(r, bp) + 6*%isidni(r, si) + 7*%isidni(r, di))

%macro reginstr 4
    %if is_gpr(%3) && is_gpr(%4)

meithecatte

/- Base types -/
variable (τ : Type)

/- Base type inhabitants -/
variable (ν : τ → Type)

def Name := String
    deriving DecidableEq

inductive Term :=

meithecatte

ECSC 2023 Qualifier Write-up

Sanity Check

The CTF landscape has changed a lot in the last year, with the introduction of OpenAI ChatGPT.

It assumed that the flag would be a simple message, but it corrected itself with a little hint.

meithecatte

Kolska Leaks

• LFI at /download?filename=$1
• /download?filename=/proc/self/exe confirms the application is written in Python
• with some luck, guess /download?filename=/app/app.py or /download?filename=app.py to get the source code
• source code includes SECRET_KEY, enough to fake an admin cookie
  • best done by deploying the app locally and modifying the code to create an admin cookie by default

meithecatte

% thx @jix_ for sharing their fonts
% compiles out of the box on https://tectonic-typesetting.github.io/ but may work
% on other LaTeX distros
\documentclass[a4paper,12pt,headings=standardclasses]{scrartcl}
\usepackage{mathpazo}
\usepackage{fontspec}
\setmainfont{TeX Gyre Pagella}
\setkomafont{disposition}{}\RedeclareSectionCommands[font=\bfseries]{paragraph}

\usepackage{tikz,tkz-euclide}

meithecatte

Sanity Check (recon/zajebiste)

Find the flag by joining the CTF's Discord server.

The description makes it sound easy. However, that is a red herring. After some false starts, I solved it by using mitmproxy's scripting abilities.

mitmproxy setup

First, create a separate Firefox profile by going to about:profiles and

meithecatte

#include <iostream>
#ifdef SELFTEST
#include <cstring>
#include <cassert>
#include <random>
#endif

using namespace std;

unsigned patterns[] = {

meithecatte

#!/usr/bin/env runhaskell
{-# LANGUAGE OverloadedStrings #-}
import Prelude hiding (replicate, putStrLn)
import Data.List hiding (replicate)
import Data.Tuple
import Data.Ord
import Data.Function
import Data.ByteString (replicate, ByteString)
import Data.ByteString.Char8 (putStrLn, pack)
import Control.Monad

meithecatte

import Data.Semigroup

data Permutation = Permutation [Int] deriving (Eq, Show)

permute :: Permutation -> [a] -> [a]
permute (Permutation p) xs = (xs !!) <$> p

instance Semigroup Permutation where
    a <> Permutation b = Permutation $ permute a b
    stimes = stimesMonoid