BLAHAJ/writeups
BLAHAJ
/
writeups
10
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

2020: gctf: sharky

This commit is contained in:
xenia 2020-08-25 00:44:16 -04:00
parent a75699b904
commit a13d9eb135
4 changed files with 501 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

246
2020/gctf/sharky/README.md Normal file
View File

@ -0,0 +1,246 @@
# sharky
writeup by [haskal](https://awoo.systems) for [BLÅHAJ](https://blahaj.awoo.systems)
**Crypto**
**231 points**
**39 solves**
>Can you find the round keys?
provided files: `challenge.py`, `sha256.py`
## tldr
for this i used [Z3](https://github.com/Z3Prover/z3) except with angr's
[claripy](https://docs.angr.io/advanced-topics/claripy) frontend instead of the direct frontend
because i've never used the direct frontend. using claripy/z3 we can construct a symbolic emulation
of the provided sha256 algorithm with the unknowns being symbolic variables. by applying constraints
for the hash output you can have z3 solve for the unknown hash constants
## writeup
initial analysis shows this is a modified sha256 algorithm with the first 8 round constants changed
to random values. the objective is to figure out what these values are given a known hash of a known
plaintext. from `challenge.py`:
```python
NUM_KEYS = 8
MSG = b'Encoded with random keys'
```
first, i checked to see if anything else was funky with the hand coded sha256 implementation by
initializing the "unknown" round constants to the standard constants and checking if the resulting
hash matched the expected "standard" hash for this message. it does, so the only difference is the
first 8 round constants
[sha256](https://en.wikipedia.org/wiki/SHA-2) (this links to wikipedia because i literally studied
sha256 from the wikipedia article during the CTF) starts by padding the message to a multiple of 512
bits. then, for each chunk of 512 bits it expands the chunk to 2048 bits by bit rotations, xors, and
arithmetic. the result is called `w`. `w` is compressed into a 256 bit state `h'` by taking the
previous state and doing 64 rounds of more bit rotations, bitwise ops, and arithmetic combining the
previous state with the nth word of `w` and the nth word of `k`, the sha256 constants table. `h`
also starts with known constants. also sha256 basically operates on 32-bit words, always. so all the
symbolic variables should be 32-bit
in this case we see the message is short enough so there is only one 512-bit chunk of padded input.
this makes things easier. i started by precomputing the `w` array for the known input, since this
doesn't depend on any (modified) constants. then, i took the verbatim python implementation of the
algorithm and stripped out every component except the round function `compression_step` that
combines `h'`, `w[i]` and `k[i]`. i applied some basic simplifications to optimize symbolic
execution such as replacing the manual bit rotate operation with the `claripy.RotateRight` builtin
and removing the bitmasking done after addition, since claripy bit vectors can't change size.
otherwise it's the original provided code, except now it's operating on symbolic variables instead
of actual numbers. it looks like this
```python
def rotate_right(v, n):
# w = (v >> n) | (v << (32 - n))
# return w & 0xffffffff
return claripy.RotateRight(v, n)
def compression_step(state, k_i, w_i):
a, b, c, d, e, f, g, h = state
s1 = rotate_right(e, 6) ^ rotate_right(e, 11) ^ rotate_right(e, 25)
ch = (e & f) ^ (~e & g)
tmp1 = (h + s1 + ch + k_i + w_i)
s0 = rotate_right(a, 2) ^ rotate_right(a, 13) ^ rotate_right(a, 22)
maj = (a & b) ^ (a & c) ^ (b & c)
tmp2 = (tmp1 + s0 + maj)
tmp3 = (d + tmp1)
return (tmp2, a, b, c, tmp3, e, f, g)
```
i figured this was good enough for z3 to work with and just threw it in
```
init_h = [
# standard constants
0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c,
0x1f83d9ab, 0x5be0cd19
]
init_h = [claripy.BVV(x, 32) for x in init_h]
secrets = [claripy.BVS(f"rc_{i}", 32) for i in range(8)]
init_k = secrets + [claripy.BVV(x, 32) for x in [
... rest of the standard constants
]]
def compression(state, w):
round_keys = init_k
for i in range(64):
state = compression_step(state, round_keys[i], w[i])
return state
w = [...] # computed w
real_hash = sys.argv[1]
real_hash = binascii.unhexlify(real_hash)
real_hash = struct.unpack(">8L", real_hash)
solver = claripy.Solver()
state = init_h[:]
out_state = compression(state, w)
state = [x + y for x, y in zip(state, out_state)]
for i in range(8):
solver.add(state[i] == real_hash[i])
for i in range(8):
print(solver.eval(secrets[i], 1)[0])
```
this did Not terminate at all. this is a side effect of me never knowing what i'm doing but in
general it seems that z3 does very poorly when you have few constraints that are each very large and
complex. in fact these ones were so large you literally cannot print them to the console
so i opted to do some handholding. i noticed that since constants 8-63 are the standard ones, the
state from round 8 to the final hash is completely known, and we can backtrack from the final hash
to the round 8 state by solving each round individually. here's the annotated code for this
```python
# i set up round 63 with the final addition that occurs after all rounds are complete
solver = claripy.Solver()
state = [claripy.BVS(f"state_{i}", 32) for i in range(8)]
out_state = compression_step(state, w[63], init_k[63])
for i in range(8):
solver.add(out_state[i] + init_h[i] == real_hash[i])
# this is a helper function that evaluates the input state of a round that produces a known output
# state and reassigns a new wanted_state for that
def get_wanted_state():
global solver
global state
wanted_state = [None]*8
for i in range(8):
res = solver.eval(state[i], 10)
if len(res) != 1:
print("ERROR", i, res)
raise SystemExit()
res = res[0]
wanted_state[i] = res
return wanted_state
# calculate the input to round 63
wanted_state = get_wanted_state()
# emulate 62 downto 8
# each round, we create a symbolic state array for the input, add constraints for the previously
# calculated output, and evaluate
for round in range(62, 8 - 1, -1):
print("emulating round", round)
solver = claripy.Solver()
state = [claripy.BVS(f"state_{round}_{i}", 32) for i in range(8)]
out_state = compression_step(state, w[round], init_k[round])
for i in range(8):
solver.add(out_state[i] == wanted_state[i])
wanted_state = get_wanted_state()
# now we have the exact state that round 8 started with
print("round 8 input state: ", [hex(x) for x in wanted_state])
```
now there should be a lot less work for z3 to guess on, it only needs to work through rounds 0-7
with the symbolic round constants
```python
state = init_h[:]
out_state = compression_round_0_7(state, w)
state = [x + y for x, y in zip(state, out_state)]
for i in range(8):
solver.add(state[i] == wanted_state[i])
for i in range(8):
print(solver.eval(secrets[i], 1)[0])
```
this took absolutely ages to complete and when it did the result was `unsat`. yikes
i'm still not sure what exactly the issue was. it's likely i just made a typo somewhere and didn't
see it. but i deleted this and replaced it with a new strategy, which is to continue going backwards
from round 7 to round 0 instead of going forwards from 0 to 7. what this does is creates a larger
number of constraints -- instead of a single set of 8 constraints on the output we have constraints
for each intermediate state in between each round. but each constraint is individually less complex,
which results in the solving going faster and actually working (!!)
```python
solver = claripy.Solver()
# go from round 7 down to 0
for round in range(7, -1, -1):
print("emulating weird round", round)
# create symbolic variables for this intermediate state
state = [claripy.BVS(f"test_r{round}_{i}", 32) for i in range(8)]
out_state = compression_step(state, w[round], init_k[round])
for i in range(8):
# constrain the output to the wanted input state for the next round
solver.add(out_state[i] == wanted_state[i])
# transfer input state to next round's wanted state
wanted_state = [None]*8
for i in range(8):
wanted_state[i] = state[i]
# add the initial state constraints
for i in range(8):
solver.add(state[i] == init_h[i])
print("answers")
for i in range(len(secrets)):
res = solver.eval(secrets[i], 1)
sys.stdout.write(hex(res[0]))
if i < len(secrets) - 1:
sys.stdout.write(",")
sys.stdout.flush()
sys.stdout.write("\n")
sys.stdout.flush()
print("SHONKS")
```
this works. for some inputs it takes a long time but most of the time it comes up with the answer
quickly. i was too lazy for an automatic script so i simply pasted the answer into netcat
```
$ python solve.py abdc6d366dd37bb452b56335cd8bfbc043e2284001891d358e04a9e76c3b2a49
...
answers
0x9da77f78,0x24597709,0x4fbc375,0xaa5cd315,0xcd73dc57,0x12dafbf7,0x7e206bb4,0xb9097fba
SHONKS
```
the lesson here is if you want z3 to terminate sometime this millenium it's better to provide a
larger number of small constraints than a small number of Giant constraints even if they're
semantically equivalent. i would probably know this if i had ever been formally trained in symbolic
execution,
---
since my team is [BLÅHAJ](https://blahaj.awoo.systems) and this challenge is named `sharky` it was
mandatory to get this flag, so i'm happy i figured it out even though crypto isn't really my strong
suit (yet,)

52
2020/gctf/sharky/challenge.py Normal file
View File

@ -0,0 +1,52 @@
#! /usr/bin/python3
import binascii
import os
import sha256
# Setup msg_secret and flag
FLAG_PATH = 'data/flag.txt'
NUM_KEYS = 8
MSG = b'Encoded with random keys'
with open(FLAG_PATH, 'rb') as f:
FLAG = f.read().strip().decode('utf-8')
def sha256_with_secret_round_keys(m: bytes, secret_round_keys: dict) -> bytes:
"""Computes SHA256 with some secret round keys.
Args:
m: the message to hash
secret_round_keys: a dictionary where secret_round_keys[i] is the value of
the round key k[i] used in SHA-256
Returns:
the digest
"""
sha = sha256.SHA256()
round_keys = sha.k[:]
for i, v in secret_round_keys.items():
round_keys[i] = v
return sha.sha256(m, round_keys)
def generate_random_round_keys(cnt: int):
res = {}
for i in range(cnt):
rk = 0
for b in os.urandom(4):
rk = rk * 256 + b
res[i] = rk
return res
if __name__ == '__main__':
secret_round_keys = generate_random_round_keys(NUM_KEYS)
digest = sha256_with_secret_round_keys(MSG, secret_round_keys)
print('MSG Digest: {}'.format(binascii.hexlify(digest).decode()))
GIVEN_KEYS = list(map(lambda s: int(s, 16), input('Enter keys: ').split(',')))
assert len(GIVEN_KEYS) == NUM_KEYS, 'Wrong number of keys provided.'
if all([GIVEN_KEYS[i] == secret_round_keys[i] for i in range(NUM_KEYS)]):
print('\nGood job, here\'s a flag: {0}'.format(FLAG))
else:
print('\nSorry, that\'s not right.')

78
2020/gctf/sharky/sha256.py Normal file
View File

@ -0,0 +1,78 @@
#! /usr/bin/python3
import struct
class SHA256:
def __init__(self):
self.h = [
0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c,
0x1f83d9ab, 0x5be0cd19
]
self.k = [
0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1,
0x923f82a4, 0xab1c5ed5, 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3,
0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, 0xe49b69c1, 0xefbe4786,
0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147,
0x06ca6351, 0x14292967, 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13,
0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, 0xa2bfe8a1, 0xa81a664b,
0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a,
0x5b9cca4f, 0x682e6ff3, 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208,
0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
]
def rotate_right(self, v, n):
w = (v >> n) | (v << (32 - n))
return w & 0xffffffff
def compression_step(self, state, k_i, w_i):
a, b, c, d, e, f, g, h = state
s1 = self.rotate_right(e, 6) ^ self.rotate_right(e, 11) ^ self.rotate_right(e, 25)
ch = (e & f) ^ (~e & g)
tmp1 = (h + s1 + ch + k_i + w_i) & 0xffffffff
s0 = self.rotate_right(a, 2) ^ self.rotate_right(a, 13) ^ self.rotate_right(a, 22)
maj = (a & b) ^ (a & c) ^ (b & c)
tmp2 = (tmp1 + s0 + maj) & 0xffffffff
tmp3 = (d + tmp1) & 0xffffffff
return (tmp2, a, b, c, tmp3, e, f, g)
def compression(self, state, w, round_keys = None):
if round_keys is None:
round_keys = self.k
for i in range(64):
state = self.compression_step(state, round_keys[i], w[i])
return state
def compute_w(self, m):
w = list(struct.unpack('>16L', m))
for _ in range(16, 64):
a, b = w[-15], w[-2]
s0 = self.rotate_right(a, 7) ^ self.rotate_right(a, 18) ^ (a >> 3)
s1 = self.rotate_right(b, 17) ^ self.rotate_right(b, 19) ^ (b >> 10)
s = (w[-16] + w[-7] + s0 + s1) & 0xffffffff
w.append(s)
return w
def padding(self, m):
lm = len(m)
lpad = struct.pack('>Q', 8 * lm)
lenz = -(lm + 9) % 64
return m + bytes([0x80]) + bytes(lenz) + lpad
def sha256_raw(self, m, round_keys = None):
if len(m) % 64 != 0:
raise ValueError('m must be a multiple of 64 bytes')
state = self.h
for i in range(0, len(m), 64):
block = m[i:i + 64]
w = self.compute_w(block)
s = self.compression(state, w, round_keys)
state = [(x + y) & 0xffffffff for x, y in zip(state, s)]
return state
def sha256(self, m, round_keys = None):
m_padded = self.padding(m)
state = self.sha256_raw(m_padded, round_keys)
return struct.pack('>8L', *state)

125
2020/gctf/sharky/solve.py Normal file
View File

@ -0,0 +1,125 @@
#! /usr/bin/python3
import struct
import binascii
import claripy
import sys
init_h = [
0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c,
0x1f83d9ab, 0x5be0cd19
]
init_h = [claripy.BVV(x, 32) for x in init_h]
secrets = [claripy.BVS(f"rc_{i}", 32) for i in range(8)]
init_k = secrets + [claripy.BVV(x, 32) for x in [
0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3,
0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, 0xe49b69c1, 0xefbe4786,
0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147,
0x06ca6351, 0x14292967, 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13,
0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, 0xa2bfe8a1, 0xa81a664b,
0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a,
0x5b9cca4f, 0x682e6ff3, 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208,
0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
]]
def rotate_right(v, n):
# w = (v >> n) | (v << (32 - n))
# return w & 0xffffffff
return claripy.RotateRight(v, n)
def compression_step(state, k_i, w_i):
a, b, c, d, e, f, g, h = state
s1 = rotate_right(e, 6) ^ rotate_right(e, 11) ^ rotate_right(e, 25)
ch = (e & f) ^ (~e & g)
tmp1 = (h + s1 + ch + k_i + w_i)
s0 = rotate_right(a, 2) ^ rotate_right(a, 13) ^ rotate_right(a, 22)
maj = (a & b) ^ (a & c) ^ (b & c)
tmp2 = (tmp1 + s0 + maj)
tmp3 = (d + tmp1)
return (tmp2, a, b, c, tmp3, e, f, g)
def compression(state, w):
round_keys = init_k
for i in range(64):
state = compression_step(state, round_keys[i], w[i])
return state
w = [1164862319, 1684366368, 2003399784, 544366958, 1685024032, 1801812339, 2147483648, 0, 0, 0, 0, 0, 0, 0, 0, 192, 1522197188, 3891742175, 3836386829, 32341671, 928288908, 2364323079, 1515866404, 649785226, 1435989715, 250124094, 1469326411, 2429553944, 598071608, 1634056085, 4271828083, 4262132921, 2272436470, 39791740, 2337714294, 3555435891, 1519859327, 57013755, 2177157937, 1679613557, 2900649386, 612096658, 172526146, 2214036567, 3330460486, 1490972443, 1925782519, 4215628757, 2379791427, 2058888203, 1834962275, 3917548225, 2375084030, 1546202149, 3188006334, 4280719833, 726047027, 3650106516, 4058756591, 1443098026, 1972312730, 1218108430, 3428722156, 366022263]
real_hash = sys.argv[1]
real_hash = binascii.unhexlify(real_hash)
real_hash = struct.unpack(">8L", real_hash)
# emulate round 63
solver = claripy.Solver()
state = [claripy.BVS(f"state_{i}", 32) for i in range(8)]
out_state = compression_step(state, w[63], init_k[63])
for i in range(8):
solver.add(out_state[i] + init_h[i] == real_hash[i])
def get_wanted_state():
global solver
global state
wanted_state = [None]*8
for i in range(8):
res = solver.eval(state[i], 10)
if len(res) != 1:
print("ERROR", i, res)
raise SystemExit()
res = res[0]
wanted_state[i] = res
return wanted_state
wanted_state = get_wanted_state()
# emulate 62 downto 8
for round in range(62, 8 - 1, -1):
print("emulating round", round)
solver = claripy.Solver()
state = [claripy.BVS(f"state_{round}_{i}", 32) for i in range(8)]
out_state = compression_step(state, w[round], init_k[round])
for i in range(8):
solver.add(out_state[i] == wanted_state[i])
wanted_state = get_wanted_state()
print("round 8 input state: ", [hex(x) for x in wanted_state])
print("emulating rounds 0-7")
from claripy.backends.backend_z3_parallel import BackendZ3Parallel
solver = claripy.Solver(track=True)
try:
for round in range(7, -1, -1):
print("emulating weird round", round)
state = [claripy.BVS(f"test_r{round}_{i}", 32) for i in range(8)]
out_state = compression_step(state, w[round], init_k[round])
for i in range(8):
solver.add(out_state[i] == wanted_state[i])
wanted_state = [None]*8
for i in range(8):
wanted_state[i] = state[i]
except claripy.errors.UnsatError:
print("unsat!!!")
print(solver.unsat_core())
sys.exit()
for i in range(8):
solver.add(state[i] == init_h[i])
print("answers")
for i in range(len(secrets)):
res = solver.eval(secrets[i], 1)
sys.stdout.write(hex(res[0]))
if i < len(secrets) - 1:
sys.stdout.write(",")
sys.stdout.flush()
sys.stdout.write("\n")
sys.stdout.flush()
print("SHONKS")