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'`

:

1 |
(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:

1 |
~((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 `sympy`

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:

1 2 3 4 5 6 7 |
#!/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 `/dev/null`

, 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.

1 2 3 4 5 |
./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:

1 2 3 4 5 6 7 |
$ cat keys/plain-1125.key 3c73e7f16fcb767a $ python >>> hex(int("3c73e7f16fcb767a", 16)) '0x3c73e7f16fcb767a' >>> bin(int("3c73e7f16fcb767a", 16)) '0b11110001110011111001111111000101101111110010110111011001111010' |

## Solution Code

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 |
# 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() |

1 2 3 4 5 6 7 8 9 10 |
#!/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: