# 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:

{
    "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.

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.

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:

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⁶⁴. Hence we can assert that some of the upper bits are zero:

for i in range(53, 63):
	s.add(nets[len(gates)+i] == False)

And we arrive at the valid PIN: `7879797576737871` - `NOOKLING`!