0CTF Quals 2019: "fixed point" writeup

This crackme-style reversing task consisted of an x86_64 binary whose main operations are:

  • Build a table data of 128-bit constants.
  • Check that the input matches flag\{[0-9a-f]{32}\}.
  • Hex-decode the inner part of the flag to obtain a byte string x.
  • Initialize a 128-bit integer variable v with the value -1 (all bits set).
  • For each byte c in "flag{" + x + "}":
    • Compute v := data[(v&0xff) ^ c] ^ (v >> 8).
  • Check that v in little-endian representation equals x.

There seems to be little hope to solve this problem generally for a “random” data array, hence we first focused on finding useful structure in the algorithm that generates the constants:

  bit = 8
  off = 128
  val = 1
  data[0] = 0
  do {
    lsb = val & 1
    val >>= 1
    if (lsb) {
      val ^= 0xb595cf9c8d708e2166d545cf7cfdd4f9
    }
    ctr = 0
    do {
      data[off+ctr] = data[ctr] ^ val;
    } while ((ctr += 2*off) < 0x100)
    off >>= 1
  } while (--bit)

The first part of the outer loop (shift and XOR) looks like division by t in a binary finite field GF(2128)=GF(2)[t]/poly. One way to divide by t is making sure (by adding the modulus) that the constant term is zero, then simply replacing each ti by ti1. The code above is equivalent to these steps, but performs them in reverse order, hence we need to shift the given constant and add back the lost LSB to obtain the modulus polynomial. Assuming this is true, the polynomial in use must be:

poly := 0xb595cf9c8d708e2166d545cf7cfdd4f9 << 1 | 1

Hence the value of val ranges through t1, t2, t3, etc., which can be seen to always equal tbit7. The second part of the loop adds this tbit7 to all the data[i] with the (bit1)th bit of i set. In other words: data[i]=bits_to_poly(i)/t8.

(Here, bits_to_poly denotes reinterpreting an integer in {0,,21281} as an element of GF(2128).)

sage quickly confirms this:

poly = 0xb595cf9c8d708e2166d545cf7cfdd4f9 << 1 | 1
F.<t> = GF(2**128, modulus = sum(int(c)*x**i for i,c in enumerate(bin(poly)[2:][::-1])))

es = []
for l in open('data.txt').read().strip().split('\n'):
    lo,hi = map(int, l.strip().replace(' ','').rstrip(',').split(','))
    es.append(F.fetch_int(hi<<64 | lo))

for i in range(256):
    assert es[i] == F.fetch_int(i) / t**8


Revisiting the flag checking algorithm with this new information, we realize that

v := data[(v&0xff) ^ c] ^ (v >> 8)

is just an addition of the flag byte followed by a division by t8! Instead of viewing this as consuming one flag byte at a time, we may equivalently XOR the flag bytes into v in the beginning (hence making it bigger than 128 bits).

This point of view implies that the output of the flag processing loop is nothing more than a computation of the form f(x)=(C+t40x)/t822=C1+C2x

where x are the flag bits converted to a polynomial and C is a constant coming from the flag{...} around the input and the initialization of v as -1.

The main consequence of this is: the flag checking algorithm is an affine function over the vector space GF(2)128!

Hence, we can recover C1 by simply evaluating that function at 0, and since fC1 is GF(2)-linear we can also (by evaluating fC1 on a basis of GF(2)128) find a matrix AGF(2)128×128 such that f(x)=C1+Ax.

With that description, it is easy to find a fixed point: If f(x)=x, then C1+Ax=x, hence (A1)x=C1. This is just what the following sage script does (it needs the values initialized in the first sage snippet above):

v2n = lambda v: int(''.join(map(str, v)), 2)
n2v = lambda n: vector(GF(2), '{:0128b}'.format(n))
n2s = lambda n: struct.pack('<QQ', n&2**64-1, n>>64).encode('hex')
flagify = lambda v: 'flag{' + n2s(v2n(v)) + '}'
def compute(vecflag):
    assert vecflag in GF(2)**128
    hexflag = flagify(vecflag)
    decflag = hexflag[:5] + hexflag[5:-1].decode('hex') + hexflag[-1:]
    v = -1 & 2**128-1
    assert len(decflag) == 22
    for c in map(ord, decflag):
        v = (v >> 8) ^^ (es[(c ^^ v) & 0xff]).integer_representation()
    return n2v(v)

origin = compute(vector(GF(2),128))
A = []
for i in range(128):
    v = vector(GF(2), (j == i for j in range(128)))
    A.append(compute(v) - origin)
sol = (matrix(A) - 1).solve_left(origin)
flag = flagify(sol)
print('input:  {:#x}'.format(v2n(sol)))
print('output: {:#x}'.format(v2n(compute(sol))))
print('--> {}'.format(compute(sol) == sol))
print(flag)

Running this code yields the flag:

$ ./pwn.sage
input:  0xa4efbaba0fa55545faf7b779c3440367
output: 0xa4efbaba0fa55545faf7b779c3440367
--> True
flag{670344c379b7f7fa4555a50fbabaefa4}
$ 

Direct method

One can also compute C in the equation for f above explicitly and simply solve for a root of fx, a linear polynomial. During the CTF, we went for the linear-algebraic approach outlined above, which is why it’s shown first, but for completeness, here’s the code for directly finding a solution (again making use of things defined above):

prfx = b'flag{'
tpl = prfx + b'\0'*16 + b'}'
R.<x> = F[]
f = sum(t**i for i in range(128))
f += sum(F.fetch_int(ord(c))*t**(8*i) for i,c in enumerate(tpl))
f += t**(8*len(prfx))*x
f /= t**(8*22)
for sol,_ in (f - x).roots():
    print('flag{' + n2s(sol.integer_representation()) + '}')

@hxp