# dreamland - zer0pts CTF 2022
###### tags: `zer0pts CTF 2022` `rev`
Writeups: https://hackmd.io/@ptr-yudai/rJgjygUM9
## Overview
We're given an x86-64 ELF binary. Although it's a bit complicated, the program is compiled without optimization and strip, and it's very easy to read the binary.
There is a subtle obfuscation that replaces every `for` statement with a pair of `setjmp` and `longjmp`.
i.e.
```c
#define FOR(var, s, e, block) { \
int var; \
jmp_buf L ## var; \
if ((var = setjmp(L ## var) + s) < e) { \
block; \
longjmp(L ## var, var - s + 1); \
} \
}
...
FOR (i, 1, 99, {
s_i[i] = s[i-1] ^ ((s[i] ^ comp0[i]) & (s[i+1] ^ comp1[i]));
});
```
This obfuscation is not effective at all. IDA can output a pretty code.
## Analysis
The program is a stream cipher. I wrote the cipher based on an existing stream cipher named [MICKEY](https://en.wikipedia.org/wiki/MICKEY). This is where the challenge description came from and "dreamland" is the name of a Japanese theme park that copied the concept of Disney but was abandoned years ago XD
Anyway, there are two hard part in this task.
### Modifying Formula into Z3-friendly Form
Basically you can use Z3 to reverse the states of the stream cipher. However, there's one hard part.
```c
void __nightmare_s(u8 s[], u8 is, u8 cs)
...
if (cs == 0) {
FOR (i, 0, 100, {
s_clocked[i] = s_i[i] ^ fb0[i] ^ fb;
});
} else {
FOR (i, 0, 100, {
s_clocked[i] = s_i[i] ^ fb1[i] ^ fb;
});
}
void __nightmare(u8 r[], u8 s[], u8 mixing, u8 input_bit)
{
u8 ir, is;
u8 cr = s[1] ^ r[14];
u8 cs = s[51] ^ r[4];
...
__nightmare_s(s, is, cs);
}
```
In `__nightmare_s` function, `s[51] ^ r[4]` is used for a conditional branch. Both `s` and `r` are what we're trying to find and we can't use it for the branch condition in Z3. Z3 provides some features such as `Select` or `If` but it often makes the solver very slow.
The best solution, I believe, is to modify the formula info a Z3-friendly form.
The current problem is that we have to use a Z3 variable for the branch condition.
| cs | formula |
|:-:|:-:|
| 0 | s_clocked[i] = s_i[i] ^ fb0[i] ^ fb |
| 1 | s_clocked[i] = s_i[i] ^ fb1[i] ^ fb |
We notice that whether use `fb0` or `fb1` is the only difference made by `cs`. Both `fb0[i]` and `fb1[i]` are 1-bit values. That is, we may swap `cs` and `(fb0[i], fb[i])` by precisely re-constructing the table.
| fb0[i] | fb1[i] | formula |
|:-:|:-:|:-:|
| 0 | 0 | s_clocked[i] = s_i[i] ^ 0 ^ fb |
| 0 | 1 | s_clocked[i] = s_i[i] ^ cs ^ fb |
| 1 | 0 | s_clocked[i] = s_i[i] ^ cs ^ 1 ^ fb |
| 1 | 1 | s_clocked[i] = s_i[i] ^ 1 ^ fb |
Now you can add the constraints for Z3!
### Undeterministic Reverting
The second problem is that the state cannot be reverted deterministicly. Multiple state may make transition into one state in this stream cipher.
The binary has ASCII check after reading the flag, so we can use it for pruning in DFS.
## Solver
```python=
from z3 import *
import string
import re
tap = [0,1,3,4,5,6,9,12,13,16,19,20,21,22,25,28,37,38,41,42,45,46,50,52,54,56,58,60,61,63,64,65,66,67,71,72,79,80,81,82,87,88,89,90,91,92,94,95,96,97]
comp0 = [0,0,0,0,1,1,0,0,0,1,0,1,1,1,1,0,1,0,0,1,0,1,0,1,0,1,0,1,0,1,1,0,1,0,0,1,0,0,0,0,0,0,0,1,0,1,0,1,0,1,0,0,0,0,1,0,1,0,0,1,1,1,1,0,0,1,0,1,0,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,1,0,1,0,1,0,0,0,0,0,0,1,1,0]
comp1 = [0,1,0,1,1,0,0,1,0,1,1,1,1,0,0,1,0,1,0,0,0,1,1,0,1,0,1,1,1,0,1,1,1,1,0,0,0,1,1,0,1,0,1,1,1,0,0,0,0,1,0,0,0,1,0,1,1,1,0,0,0,1,1,1,1,1,1,0,1,0,1,1,1,0,1,1,1,1,0,0,0,1,0,0,0,0,1,1,1,0,0,0,1,0,0,1,1,0,0,0]
fb0 = [1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,0,0,1,0,1,1,1,1,1,1,1,1,1,1,0,0,1,1,0,0,0,0,0,0,1,1,1,0,0,1,0,0,1,0,1,0,1,0,0,1,0,1,1,1,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,0,1,1,0,1,0,0,0,1,1,0,1,1,1,0,0,1,1,1,0,0,1,1,0,0,0]
fb1 = [1,1,1,0,1,1,1,0,0,0,0,1,1,1,0,1,0,0,1,1,0,0,0,1,0,0,1,1,0,0,1,0,1,1,0,0,0,1,1,0,0,0,0,0,1,1,0,1,1,0,0,0,1,0,0,0,1,0,0,1,0,0,1,0,1,1,0,1,0,1,0,0,1,0,1,0,0,0,1,1,1,1,0,1,1,1,1,1,0,0,0,0,0,0,1,0,0,0,0,1]
def hyper_feedback(i, cs):
v = (fb0[i], fb1[i])
if v == (0, 0):
return 0
elif v == (0, 1):
return cs
elif v == (1, 0):
return cs ^ 1
elif v == (1, 1):
return 1
def bit(x, n):
return (x >> n) & 1
def search(enc, r, s, max_length, flag='', bitstack=[]):
#print(flag.encode(), bitstack)
solver = Solver()
orig_r, orig_s = BitVec('r', 100), BitVec('s', 100)
cr = bit(orig_s, 1) ^ bit(orig_r, 14)
cs = bit(orig_s, 51) ^ bit(orig_r, 4)
# __nightmare_r(orig_r, 0, cr) --> r
fb = bit(orig_r, 99)
for i in range(100):
rc = 0
if i > 0:
rc = bit(orig_r, i-1)
if i in tap:
rc ^= fb
rc ^= bit(orig_r, i) & cr
solver.add(rc == r[i])
# __nightmare_s(orig_s, 0, cs) --> s
fb = bit(orig_s, 99)
s_i = [0 for i in range(100)]
s_i[99] = bit(orig_s, 98)
for i in range(1, 99):
s_i[i] = bit(orig_s, i-1) ^ ((bit(orig_s, i) ^ comp0[i]) & (bit(orig_s, i+1) ^ comp1[i]))
for i in range(100):
solver.add(s[i] == s_i[i] ^ fb ^ hyper_feedback(i, cs))
# Find all possible states
while True:
result = solver.check()
if result == sat:
m = solver.model()
new_r, new_s = [], []
for i in range(100):
new_r.append((m[orig_r].as_long() >> i) & 1)
new_s.append((m[orig_s].as_long() >> i) & 1)
new_bitstack = list(bitstack)
new_bitstack.append(new_r[0] ^ new_s[0])
solver.add(Not(And(orig_r == m[orig_r], orig_s == m[orig_s])))
new_flag = flag
if len(new_bitstack) == 8:
c = 0
for i in range(8):
c |= (new_bitstack[7-i]) << i
c ^= enc[-1-len(new_flag)]
if chr(c) not in string.printable:
continue
new_flag = chr(c) + new_flag
print(new_flag.strip(), len(new_flag), bin(c), hex(c))
if len(new_flag) == max_length:
print("[+] Candidate: " + new_flag)
if new_flag.startswith("zer0pts{"):
print("[+] FLAG: " + new_flag)
continue
new_bitstack = []
search(enc, new_r, new_s, max_length, new_flag, new_bitstack)
else:
break
if __name__ == '__main__':
with open("../distfiles/flag.txt.enc", "rb") as f:
f.seek(0, 2)
size = f.tell()
f.seek(0, 0)
enc = f.read(size - 26)
rb = f.read(13)
sb = f.read(13)
r, s = [], []
for i in range(13):
for j in range(8):
if i*8+j < 100:
r.append((rb[i] >> j) & 1)
s.append((sb[i] >> j) & 1)
search(enc, r, s, size-26)
```
Sign in with Wallet
Connect another wallet