# 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`!