# CalATMity We're linked a socket server and the binary running on it, which seems like a classic "license"-style executable. Running it: ``` Thanks for using Nook stop! Please enter your 16-digit PIN: ``` Popping the binary into Binja also shows that we are dealing with compiled Rust (oof). Thankfully there are debug symbols, and I found two interesting functions: - `tiny_eval:main()` - `tiny_eval:do_eval()` Let's start with `main`, which looks for a file named `debug.pkl`. If that doesn't exist, the program turns to a string at the address `0x6f932`. Then it applies the following: 1. Base64 decode 2. Gzip decompress 3. Deserialize with `serde-pickle` We can perform this ourselves, deserializing with Python's `pickle` library directly. The prettified contents: ```jsonld { "gates": [ {"op": ("NOT",)}, {"op": ("AND",)}, {"op": ("AND",)}, ...], "netlist": [ [1, 131], [2], [3], ...] } ``` Based on the terminology alone, this object definitely represents a binary circuit. We have a list of gates that can either be NOT, AND, or XOR, as well as a netlist which describes circuit connections - more on this later. This circuit is then passed into the `do_eval` function along with our PIN input. I didn't explore much further, but at this point my guess was we needed to satisfy this circuit. ## Circuit Structure I'm not too experienced with digital circuits, so it wasn't immediately clear how to interpret the pickled object. Nevertheless, a few observations: * `gates` has 1821 elements * `netlist` has 1885 elements * `netlist` contains 1882 distinct numbers: `0, 1, 2, ..., 1819, 1820, 1885` From this, we can ~~guess~~ deduce the circuit structure. First, the numbers from `0` to `1820` represent the 1821 gates (0-indexed). The 64 mising numbers most likely represent our input PIN, and `1885` is the circuit output. Next, there are 1885 nets - exactly matching 1821 gates plus 64 inputs. Hence each net contains the outputs of that gate/input. For example: * If the 1337th net is `[682, 1606, 1615]`, then gate 1337 feeds into gates 682, 1606, and 1615. * If the 1884th net is `[29, 579, 871]`, then input 1884 feeds into gates 29, 579, 871. * Output 1885 only appears once, in net 1476: `[1885]`. Here's my setup: * `inputs` is essentially the inverse of `netlist`, mapping each gate to the nets that feed into it. * `final` is the output gate. ```python import base64 import pickle import gzip circuit = open('calatmity', 'rb').read()[0x6f932:] circuit = base64.b64decode(circuit) circuit = gzip.decompress(circuit) circuit = pickle.loads(circuit) gates = circuit['gates'] netlist = circuit['netlist'] inputs = [[] for _ in gates] for i, net in enumerate(netlist): if net == [1885]: final = i else: for j in net: inputs[j].append(i) ``` ## Satisfiability I decided to use z3 to crack the circuit. The general approach: * Create a Bool variable for every net (gate and input). * Assert each gate operation in the solver. * Assert that gate 1476 (the output) is true. ```python from z3 import * s = Solver() nets = [Bool('net_{}'.format(i)) for i in range(1886)] s.add(nets[final] == True) for i, gate in enumerate(gates): args = [nets[x] for x in inputs[i]] op = gate['op'][0] if op == 'NOT': s.add(nets[i] == Not(args[0])) elif op == 'AND': s.add(nets[i] == And(args[0], args[1])) elif op == 'XOR': s.add(nets[i] == Xor(args[0], args[1])) else: raise Exception assert s.check() model = s.model() ``` This works, although there turns out to be quite a few valid models. We also haven't reversed engineered how the integer is converted into this bit sequence. But after some trial and error, I figured out that the PIN is directly interpreted as an integer and converted into binary. The least significant bit is net 1884, while the most significant bit is net 1821: ```python pin = 0 for i in range(64): if model[nets[len(gates)+i]]: pin |= 1 << i ``` Furthermore, notice that a 16-digit integer is much smaller than 2<sup>64</sup>. Hence we can assert that some of the upper bits are zero: ```python for i in range(53, 63): s.add(nets[len(gates)+i] == False) ``` And we arrive at the valid PIN: `7879797576737871` - `NOOKLING`!