Google CTF | Reverse a Cellular Automata

This is a writeup for one of the challenges from the Google CTF which I participated in a few weeks ago. My friend Chris and I were finally able to get this flag after a lot of hitting our heads together. The Reverse a Cellular Automata challenge (may not be up in the future) was a lot of fun.

This crypto category flag gave us the base64 encoded flag and the encryption key after one iteration of Wolfram’s rule 126 was ran on it. Our job was to move backward one step and get the actual key.

Wolfram Rule 126

This rule is a bit similar to the Game of Life. In this case, take an n bit number, for example 101110, and run through the following rules:

• For every bit, if the value is the SAME as each of its two neighbors, its next value is 0
• Otherwise, its value is 1
• The least/most significant bits are neighbors with each other

So in the example above, if we’re dealing with 101110 and run rule126 on it, our next value would be: 111011.

It’s trivial to go forward one step, it’s a bit more difficult to go backward which is what this problem requires.

Reverse Rule 126

We didn’t prove this, but pragmatically speaking, given a number N there is at least one ancestor n' where rule126(n') == N. Let’s call the set of all values of n' where rule126(n') == N‘. It seems that, in many cases |N'| is rather high. That is, the number of potential values of n' ∈ N' is large.

The most obvious way to solve this problem would be to brute force it. But since the encryption key is 64 bits this would take about 545 years so we decided to go a different route. We needed to limit our search space.

In order to do so, we thought about the rule126 rules in reverse. For instance, what does it mean if a given bit in N is a 0? Well, it means that in the previous ancestor n' that bit was the same as each of its neighbors. In other words, if we saw a 0 in bit b_1 then in n' bits {b_0,b_1,b_2} were either all 0 or all 1. The opposite is true if we encounter a 1 in b_1. That is, bits {b_0,b_1,b_2} were NOT either all 0 or all 1.

As we talked this through, it became apparent that we could use a SAT solver to limit our search space.

SAT Solvers

SAT Solvers, or satisfiability solvers, take a number of constraints and determine if the constraints are satisfiable. That is, if there is some solution which will satisfy all of the constraints.

In order to use one, we needed to write our rules above as a series of constraints. Let’s say we have three bits: A, B, and C where B is some bit b_i and A and C are B‘s left and right neighbors respectively. If the value of B is 0 then we know that in n':

(A ^ B ^ C) V (~A ^ ~B ^ ~C)

In other words, either all of those bits are on or they’re all off.

Similarly if the value of B is 1 then:

~((A ^ B ^ C) V (~A ^ ~B ^ ~C))

Unfortunately, SAT solvers do not take logical propositions like the ones above. They need to take constraints in something called Conjunctive Normal Form (CNF). Luckily, any valid logical proposition can be written in CNF and there are lots of tools to automatically rewrite propositions in CNF.

to_cnf

We were able to use a python library called <a href="https://docs.sympy.org/latest/modules/logic.html">sympy</a> which has the ability to rewrite propositional logic into CNF. This was ideal for our use case, and we were able to quickly generate our logic above into equivalent logic in CNF. This was then fed into our sat solver and we were on our way. I won’t go into all of the rewrites, but see our final solution below to get a feel for how this worked.

Getting Ancestors

Running our solver gave us gave us 10,753 different possible values for n' which was honestly much larger than I expected. Not to worry though, we saved each valid n' as a binary key and then ran our decryption script with each key using the following code:

#!/bin/bash
FILES=keys/enc-*
for f in $FILES
do
    printf "Processing $f file...\n"
    echo $BASE64_FLAG | openssl enc -d -aes-256-cbc -pbkdf2 -md sha1 -base64 --pass file:"$f" 2>/dev/null | grep "CTF"
done

In other words, if the decryption had an error we directed it to <a href="https://en.wikipedia.org/wiki/Null_device">/dev/null</a>, otherwise we checked to see if CTF was in the output and we had our flag. The decryption code above was given to us in the question.

./decrypt.sh
...
Processing keys/enc-1125.key file...
CTF{reversing_cellular_automatas_can_be_done_bit_by_bit}
...

And we got it! Though it’s not really incredibly helpful, I thought it was interesting:

$ cat keys/plain-1125.key
3c73e7f16fcb767a
$ python
>>> hex(int("3c73e7f16fcb767a", 16))
'0x3c73e7f16fcb767a'
>>> bin(int("3c73e7f16fcb767a", 16))
'0b11110001110011111001111111000101101111110010110111011001111010'

Solution Code

# reverse.py
import pycosat
LEN = 64

# run rule126 on some bits
def rule126(bits):
    ret = []
    for i, b in enumerate(bits):
        if bits[i - 1] == b and b == bits[(i + 1) % len(bits)]:
            ret.append('0')
        else:
            ret.append('1')
    return ret


# generate a list of all possible predecessors n' where 
# rule126(n') == bits
def reverse_rule126(bits, n=LEN):
    cnf = []
    for i, b in enumerate(bits):
        if b == '0':
            # (A | ~A) & (A | ~B) & (A | ~C) & (B | ~A) & (B | ~B) & (B | ~C) & (C | ~A) & (C | ~B) & (C | ~C)
            cnf += [[var(i, n), -var(i, n)], [var(i, n), -var(i - 1, n)],
                    [var(i, n), -var(i + 1, n)], [var(i - 1, n), -var(i, n)],
                    [var(i - 1, n), -var(i - 1, n)], [var(i - 1, n), -var(i + 1, n)],
                    [var(i + 1, n), -var(i, n)], [var(i + 1, n), -var(i - 1, n)],
                    [var(i + 1, n), -var(i + 1, n)]]
        else:
            cnf += [[var(i, n), var(i - 1, n), var(i + 1, n)],
                    [-var(i, n), -var(i - 1, n), -var(i + 1, n)]]
    solutions = pycosat.itersolve(cnf)
    return [['1' if v > 0 else '0' for v in solution] for solution in solutions]


# logic to make sure LSB and MSB are neighbors
def var(i, n):
    if i < 0:
        return n
    if i >= n:
        return 1
    return i + 1


# return a list of bits of size n from a hex number
def hex_string_to_bits(hex_string, n):
    ret = [b for b in bin(int(hex_string, 16))[2:].zfill(n)]
    assert len(ret) == n, "Len: {}".format(len(ret))
    return ret


# return a hex number from a list of bits
def bits_to_hex_string(bits):
    return hex(int(''.join(bits), 2))[2:]

def main():
    hex_string = '66de3c1bf87fdfcf'
    prev_vals = reverse_rule126(hex_string_to_bits(hex_string, LEN))
    for i, v in enumerate(prev_vals):
        val_string = bits_to_hex_string(v)
        hex_string_prime = bits_to_hex_string(rule126(v))
        assert hex_string_prime == hex_string, "Hex String: {}".format(hex_string_prime)
        print "{} is a valid string".format(val_string)
        fname = 'keys/plain-{}.key'.format(i)
        with open(fname, 'w') as f:
            f.write(val_string)


if __name__ == '__main__':
    main()

#!/bin/bash

FILES=keys/*
COUNT=0
for f in $FILES
do
    echo "Processing $f file...\n"
    xxd -r -p "$f" > keys/enc-${COUNT}.key
    let COUNT=COUNT+1
done

Links

From another CTF Player:

• http://sprunge.us/KdVf3A
• http://sprunge.us/EWdhp1