<- HACKON CTF

Play Time

7 minutes to read

We are given a Python script that encrypts the flag:

from xorshiro256 import Xoshiro256estrellaestrella
from hashlib import sha512
from secrets import randbits
from Crypto.Util.number import getPrime

FLAG = b"HackOn{??-_-??}"

rng = Xoshiro256estrellaestrella([randbits(64) for _ in range(4)])
def xor(a,b):
    return bytes(x ^ y for x,y in zip(a,b))
def otp():
    return (rng() << 128) | (rng() << 64) | rng()
def encrypt(message, key):
    return xor(message,key).hex()

def lets_play():
    eee = [otp() for _ in range(5)]
    hhh = int(sha512(b"What is going on????").hexdigest(),16)
    www = int(sha512(b"-_-").hexdigest(),16)
    for _ in range(5):
        print(www*(hhh*getPrime(400) + eee[_]))
lets_play()
print(f"Of course take the flag: {encrypt(FLAG,otp().to_bytes(24,'big') + otp().to_bytes(24,'big') + otp().to_bytes(24,'big') + otp().to_bytes(24,'big'))}")

This script imports another one called xoshiro256.py:

MASK64 = (1 << 64) - 1


def rotl64(x, n):
    return ((x << n) | (x >> (64 - n))) & MASK64


class Xoshiro256estrellaestrella:
    def __init__(self, s: list[int]):
        if len(s) != 4:
            raise ValueError("Invalid state")
        self.s = s

    @staticmethod
    def temper(s1):
        return rotl64(s1 * 5 & MASK64, 7) * 9 & MASK64

    inv9 = pow(9, -1, 1<<64)
    inv5 = pow(5, -1, 1<<64)

    @staticmethod
    def untemper(s1):
        return (rotl64(s1 * Xoshiro256estrellaestrella.inv9 & MASK64, 64 - 7) * Xoshiro256estrellaestrella.inv5 & MASK64)

    def step(self):
        s0, s1, s2, s3 = self.s
        result = s1
        t = (s1 << 17) & MASK64
        s2 ^= s0
        s3 ^= s1
        s1 ^= s2
        s0 ^= s3
        s2 ^= t
        s3 = rotl64(s3, 45)
        self.s = [s0, s1, s2, s3]
        return result

    def __call__(self):
        return self.temper(self.step())

We also have the output of the challenge script:

13212604756760576839566029879790507340621125351650910037096438542986281767798935731815960919847190335319997626490657290703982780531188982755812359825778991287851722231653240101516281221277771687552595606357705667021283245647184176190780371803847239046057899625306709335445492253829904457728963663330232360074002592294748902165490734661754641346105555480845725245401274622849042633220680814862218507825000273496174518135135018296
10941254150150025674552873841829377160894872702989189221030375278924020303440766829212501568712317129316625966056943292892254051556591182699583782809766043430039526087782632726822390246237207588223614532129919563546317959123226772171340188871049507419759715801243252593170422974418428462985058137138632654284570886374958625043528751248848999225696572462957490312158113035640608574297096993882606872975815007084967924414642980776
15101349666572801938485401280432371477809444483981100057606730238263165151424318566626548931488229895122994206046583802385648294413304175367322953662352599315904063583374091625850491510370325443484473334570074021702629429967091991051778066603994035464123640521499352527048160060494173173666036904182158407134434879411353463525907301113557907096744334931379461289162704385044839685089971009445572331890345614370546943037400147983
13342383541948912904739657745633850307061066808554491420342437647156840907474202734010723903582264217743491384126126906186261528960170260592481378655261612977076194385513721691794702104584131178573340233624384858733837689459678253142113892528886104912973772094271490509833087078998828250566430425723306082267268756937078197726277984632313371500970952851404697896276325125638170652585429636027841332778024087695314635287635675733
12636229806834250241258615367399065807361433585224380319327082221039501263453353205604056010474585287969305429059979257806627860612598485817264675754852118128230084965081330020085917729023163749382526170463539873149440032710085890969050246185772149152903578407419978590749722355505197313305689658366450442894623670629857776783671952094413125054252154677545972238794873293061464124474598848521323188015310501328407376905710535393
Of course take the flag: b375f90caac87e919e6f761d8e518e124b62a9658674b09a210503d8844083715f005912fa1e1cfed720c20e9d4f55d3a8eb9b80f0e185c96efce878a15aeb49ebf30eb17de3bd356d465c1e

Source code analysis

The xoshiro256.py script implements Xoshiro256** algorithm, which belongs to the family of Xorshift random number generators, and it is just a Linear-feedback Shift Register (LFSR).

The chall.py script uses this Xoshiro256** algorithm, initialized with a random seed, as a PRNG to encrypt the flag with a XOR cipher. In addition, we are given some results that depend on PRNG outputs:

def lets_play():
    eee = [otp() for _ in range(5)]
    hhh = int(sha512(b"What is going on????").hexdigest(),16)
    www = int(sha512(b"-_-").hexdigest(),16)
    for _ in range(5):
        print(www*(hhh*getPrime(400) + eee[_]))
lets_play()
print(f"Of course take the flag: {encrypt(FLAG,otp().to_bytes(24,'big') + otp().to_bytes(24,'big') + otp().to_bytes(24,'big') + otp().to_bytes(24,'big'))}")

Each otp output is a combination of three consecutive PRNG outputs:

def otp():
    return (rng() << 128) | (rng() << 64) | rng()

So, the objective is to use the provided PRNG outputs to find the original seed (or at least some state) in order to find the correct XOR key to decrypt the flag.

Solution

First of all, we can find the PRNG outputs with simple modular arithmetic and integer division. The list eee is composed of 5 otp outputs, and then hhh and www are known integer values. Each given output is computed as:

Where is an unknown 400-bit prime number. Notice that both and are 512-bit numbers, and is a 192-bit number, hence is a 1024-bit number and is a 704-bit number. Therefore, we have:

With this, we are ready to find the seed of the PRNG.

Apart from the LFSR, the Xoshiro256** algorithm also has a temper routine to transform the LFSR output. But it is easy to undo the transform. Actually, the xoshiro256.py script provides an untemper routine, so we don’t have to bother.

This is the solution code up to this step:

from hashlib import sha512

from xorshiro256 import MASK64, Xoshiro256estrellaestrella


hhh = int(sha512(b"What is going on????").hexdigest(), 16)
www = int(sha512(b"-_-").hexdigest(), 16)

with open('output.txt') as f:
    output = [int(f.readline()) for _ in range(5)]
    enc_flag = bytes.fromhex(f.readline().split(': ')[1])

eee = [(o % (hhh * www)) // www for o in output]

rng_outputs = []

for e in eee:
    rng_outputs.append(Xoshiro256estrellaestrella.untemper((e >> 128) & MASK64))
    rng_outputs.append(Xoshiro256estrellaestrella.untemper((e >> 64) & MASK64))
    rng_outputs.append(Xoshiro256estrellaestrella.untemper(e & MASK64))

Now we only need to find the PRNG seed.

The z3 way

If we are lazy, we can take z3 and just tell it to find the seed of the PRNG. For this, we have to define the seed [s0, s1, s2, s3] as 64-bit bit-vectors, and perform the same operations as the challenge PRNG. After that, we simply add the constraints that each PRNG output matches the corresponding symbolic PRNG output:

from z3 import BitVec, RotateLeft, sat, Solver


s = [BitVec(f's{i}', 64) for i in range(4)]


def z3_step():
    result = s[1]
    t = (s[1] << 17) & MASK64
    s[2] ^= s[0]
    s[3] ^= s[1]
    s[1] ^= s[2]
    s[0] ^= s[3]
    s[2] ^= t
    s[3] = RotateLeft(s[3], 45)
    return result


solver = Solver()

for e in rng_outputs:
    solver.add(z3_step() == e)

if solver.check() != sat:
    exit(1)

model = solver.model()

s0, s1, s2, s3 = [model[BitVec(f's{i}', 64)].as_long() for i in range(4)]
print([s0, s1, s2, s3])

This code simply finds the seed.

The SageMath way

We have said that Xoshiro256** is an LFSR. Therefore, all the operations in step are linear in terms of bits. As a result, we can say that each s1, s2, s3 and s4 is list of 64 binary variables. In other words, we are working on , the finite field of two elements, where addition is a binary XOR and multiplication is a binary AND.

Once we know this, we can define binary variables to work as s1, s2, s3 and s4. Then, we can define how each PRNG step works:

  • XOR is just adding binary variables one by one
  • We can implement left shift and rotation using list indexing and concatenation in Python

Finally, we compute each symbolic output and subtract (equivalent to addition ) each expected output, bit by bit. Then, we are left with solving a homogeneus system of equations, which can be done as a matrix equation , finding the right kernel.

from sage.all import BooleanPolynomialRing, Sequence


n2b = lambda n: list(map(int, f'{n:064b}'))
b2n = lambda b: int(''.join(map(str, b)), 2)

s_bits = BooleanPolynomialRing(','.join(','.join(f's{k}_{i}' for i in range(64)) for k in range(4))).gens()

s0_bits = list(s_bits[0:64])
s1_bits = list(s_bits[64:128])
s2_bits = list(s_bits[128:192])
s3_bits = list(s_bits[192:256])

s = [s0_bits, s1_bits, s2_bits, s3_bits]


def step():
    global s
    s0, s1, s2, s3 = s
    result = s1
    t = s1[17:] + [0] * 17
    s2 = [s0_i + s2_i for s0_i, s2_i in zip(s0, s2)]
    s3 = [s1_i + s3_i for s1_i, s3_i in zip(s1, s3)]
    s1 = [s1_i + s2_i for s1_i, s2_i in zip(s1, s2)]
    s0 = [s0_i + s3_i for s0_i, s3_i in zip(s0, s3)]
    s2 = [t_i + s2_i for t_i, s2_i in zip(t, s2)]
    s3 = s3[45:] + s3[:45]
    s = [s0, s1, s2, s3]
    return result


eqs = []

for i, r in enumerate(rng_outputs):
    for r_i, sym_r_i in zip(n2b(r), step()):
        eqs.append(r_i + sym_r_i)

A, _ = Sequence(eqs).coefficients_monomials(sparse=False)
sol = A.right_kernel_matrix()[0]

s0 = b2n(sol[0:64])
s1 = b2n(sol[64:128])
s2 = b2n(sol[128:192])
s3 = b2n(sol[192:256])
print([s0, s1, s2, s3])

And with this, we will also get the seed.

Decrypting the flag

Once we have the seed, we can use the same PRNG as the challenge and get the XOR key to decrypt the flag:

def xor(a, b):
    return bytes(x ^ y for x, y in zip(a, b))


def otp():
    return (rng() << 128) | (rng() << 64) | rng()


rng = Xoshiro256estrellaestrella([s0, s1, s2, s3])

for i in range(5):
    assert otp() == eee[i]

print(xor(enc_flag, b''.join(otp().to_bytes(24, 'big') for _ in range(4))).decode())

Flag

With both scripts, we can capture the flag:

$ python3 solve_z3.py
[12884506012955422719, 18404887875378004044, 12245814120916282883, 12686849208438892288]
HackOn{la4ticces_4nd_l1n34r_s1yst3ms_wh4t_a_misterious_w0rld_pd:iwant2sleep}

$ python3 solve_sage.py
[12884506012955422719, 18404887875378004044, 12245814120916282883, 12686849208438892288]
HackOn{la4ticces_4nd_l1n34r_s1yst3ms_wh4t_a_misterious_w0rld_pd:iwant2sleep}

The full scripts can be found in here: solve_z3.py and solve_sage.py.