Skip to content

Instantly share code, notes, and snippets.

@5teven1in

5teven1in/README.md

Last active June 26, 2021 07:48
Show Gist options
  • Save 5teven1in/9d341b53b5a0939c061f5d1325b849c4 to your computer and use it in GitHub Desktop.
Save 5teven1in/9d341b53b5a0939c061f5d1325b849c4 to your computer and use it in GitHub Desktop.
Download ZIP
HITCON CTF 2020 11011001 Writeup
Raw
README.md

11011001 [255pts]

0100111001101111001000000110100001101001011011100111010000100000011010000110010101110010011001010010110000100000011101110110100001100001011101000010000001100001011100100110010100100000011110010110111101110101001000000110010101111000011100000110010101100011011101000110100101101110011001110010000001100110011011110111001000111111

11011001-878450f7a8f95309ce756975ce912376d829c1d7caeed7f80da72ee3bc67e5ca

Author: david942j
30 Teams solved.

# Team Submit Time
1 Samurai 2020-11-28 21:42:56 UTC
2 c0r3dump 2020-11-28 22:51:13 UTC
3 More Smoked Leet Chicken 2020-11-28 23:31:35 UTC
Raw
run.sh
#!/bin/bash
python solve.py | ./11011001-878450f7a8f95309ce756975ce912376d829c1d7caeed7f80da72ee3bc67e5ca
# Congratulations!
# Here's your gift: hitcon{fd05b10812d764abd7d853dfd24dbe6769a701eecae079e7d26570effc03e08d}
Raw
solve.py
from z3 import *
from math import ceil, log2
def popcount(bvec):
return Sum([ZeroExt(int(ceil(log2(bvec.size()))), Extract(i,i,bvec)) for i in range(bvec.size())])
v = [BitVec(f'v{i}', 32) for i in range(20)]
data = [0x81002, 0x1000, 0x29065, 0x29061, 0x0, 0x0, 0x16C40, 0x16C00, 0x20905, 0x805, 0x10220, 0x220, 0x98868, 0x80860, 0x21102, 0x21000, 0x491, 0x481, 0x31140, 0x1000, 0x801, 0x0, 0x60405, 0x400, 0x0C860, 0x60, 0x508, 0x400, 0x40900, 0x800, 0x12213, 0x10003, 0x428C0, 0x840, 0x840C, 0x0C, 0x43500, 0x2000, 0x8105A, 0x1000]
s = Solver()
for i in range(20):
s.add(v[i] & 0xFFF00000 == 0)
s.add(data[i * 2] & v[i] == data[i * 2 + 1])
for i in range(20):
for j in range(18):
s.add(And(((v[i] >> j) & 7) != 7, ((v[i] >> j) & 7) != 0))
for k in range(20):
v12 = BitVecVal(0, 32)
for i in range(20):
v12 = (v12 | (((v[i] >> k) & 1) << i))
for j in range(18):
s.add(And(((v12 >> j) & 7) != 7, ((v12 >> j) & 7) != 0))
for i in range(20):
s.add(popcount(v[i]) == 10)
for k in range(20):
v19 = BitVecVal(0, 32)
for i in range(20):
v19 = (v19 | (((v[i] >> k) & 1) << i))
s.add(popcount(v19) == 10)
if s.check() == sat:
m = s.model()
for i in range(20):
print(m[v[i]])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment