# ASIS CTF Finals 2014 – SATELLITE

Description: Connect here and find the flag: `nc asis-ctf.ir 12435`

After we connect to the server, it show us the following message:

```
hi all, You must send a string for each level that would make the literal True
send "Sattelite"
Sattelite
(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)
```

Hmmm, it’s seems like it give us a some kind of expression, which `∨`

means **OR**, `∧`

means **AND** and `¬`

means **NOT**. And we have to send “**something**” to make the literal True. After having some discussion with teammates, I finally understand what we should send.

Let us define that `x1`

is a **variable** and `(¬x2 ∨ ¬x4)`

is a **clause**. **The number of the variable depends on how many clause are in the expression**.

For example, for the following expression:

```
(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)
```

there are **5** clauses in the expression, so the number of the variable is **5**, which means `x1`

~`x5`

.

As for the following expression:

```
(¬x6 ∨ x2) ∧ (x3 ∨ x1) ∧ (¬x5 ∨ ¬x6) ∧ (¬x2 ∨ ¬x7) ∧ (¬x4 ∨ ¬x1) ∧ (x2 ∨ x8) ∧ (¬x6 ∨ ¬x2) ∧ (¬x3 ∨ ¬x7) ∧ (x3 ∨ ¬x6)
```

there are **9** clauses in the expression, so the number of the variable should be **9**, which means `x1`

~`x9`

, even though `x9`

doesn’t appear in the expression.

We have to send a string which represent the value of each variable, that make the literal **True**.
For instance, as for the expression

```
(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)
```

we can send `00000`

, which makes `(¬0 ∨ ¬0) ∧ (¬0 ∨ 0) ∧ (0 ∨ ¬0) ∧ (0 ∨ ¬0) ∧ (0 ∨ ¬0)`

equals **True**.

And for the expression

```
(¬x6 ∨ x2) ∧ (x3 ∨ x1) ∧ (¬x5 ∨ ¬x6) ∧ (¬x2 ∨ ¬x7) ∧ (¬x4 ∨ ¬x1) ∧ (x2 ∨ x8) ∧ (¬x6 ∨ ¬x2) ∧ (¬x3 ∨ ¬x7) ∧ (x3 ∨ ¬x6)
```

both `110000000`

and `110000001`

will all make the literal True, since `x9`

doesn’t appear in the expression.

So we finally know what should we send to pass the level and get the flag, time to write some code. For this challenge I decide to write a python script to calculate the answer and send it automatically.

I assume that the number of variable won’t larger than 20 ( just a wild guess, and luckily, I was right ^_^ ). So I decide to calculate the answer by brute-forcing all the possible string. If there are 5 variables, I just went through all the string from `00000`

~ `11111`

. The time complexity is `2^n`

, which isn’t very effective, but it can still calculate the right answer in less than 5 seconds.

So here is what I’m going to do:

- parse the input expression, convert it into a string that
`eval`

can recognize & evaluate the result. - run through
`00...0`

to`11...1`

, substitute variables with`0`

or`1`

- use
`eval`

to evaluate the result. If it’s`1`

, send the answer, or else run the next string.

For example, the input expression is

```
(¬x2 ∨ ¬x4) ∧ (¬x1 ∨ x2) ∧ (x5 ∨ ¬x1) ∧ (x1 ∨ ¬x1) ∧ (x4 ∨ ¬x5)
```

After the parsing function, the string will be like this:

```
(~2 | ~4) & (~1 | 2) & (5 | ~1) & (1 | ~1) & (4 | ~5)
```

and then run through `00...0`

to `11...1`

, substitute `1`

,`2`

…to `0`

or `1`

. To ensure the result will be only `1`

or `0`

, each `0`

& `1`

will do the `& 0x1`

operation ( convert operands to 1 bit ). So the final evaluate string will be:

```
(~0 & 0x1 | ~0 & 0x1) & (~0 & 0x1 | 0 & 0x1) & (0 & 0x1 | ~0 & 0x1) & (0 & 0x1 | ~0 & 0x1) & (0 & 0x1 | ~0 & 0x1)
```

```
from socket import *
from struct import *
def string_to_expression(input_str):
# OR, AND & NOT's ascii code might be weird and should be treated as special case
# 226 136 168 -> OR (ascii: 124)
# 226 136 167 -> AND (ascii: 38)
# 194 172 -> NOT (ascii: 126)
expression = [] # list for storing the expression's ascii code & variable id
cur_num = 0 # calculate single variable id
max_num = 0 # total variable number
inCal = False
for c in input_str:
asc = ord(c)
if c.isdigit() == True:
if inCal == False:
inCal = True
cur_num = 10*cur_num + asc - 48
else:
if inCal == True:
inCal = False
expression.append(cur_num)
cur_num = 0
if asc == 226 or asc == 136 or asc == 194 or asc == 120: #ignore, continue
continue
elif asc == 168: # OR
expression.append(124)
elif asc == 167: # AND
expression.append(38)
elif asc == 172: # NOT
expression.append(126)
elif asc == 10: # end of expression, break
break;
elif asc == 40: # '(', count variable number
max_num += 1
expression.append(asc)
else:
expression.append(asc)
return expression, max_num
def carry(x_list, size):
# from 0000 to 0001, 0001 to 0010.....
x_list[size-1] += 1
for i in range(size-1, -1, -1):
x_list[i-1] += x_list[i]/2
x_list[i] %= 2
return x_list
def cal_ok(eval_list, cur_max):
index_list = [[] for i in range(cur_max)] # index list that record each variable's position
x_list = [0]*cur_max
for index,item in enumerate(eval_list):
if item <= cur_max:
index_list[item-1].append(index)
cnt = 2**cur_max
for i in range(cnt):
for number in range(cur_max):
for index in index_list[number]:
eval_list[index] = x_list[number]
eval_str = ""
for item in eval_list:
if item == 0 or item == 1:
eval_str += str(item)
eval_str += str(' & 0x1 ')
else:
eval_str += chr(item)
# print "calculating: " + eval_str
# print "result: " + str(eval(eval_str))
if eval(eval_str) == 1: # found the answer!
return "".join(str(c) for c in x_list)
else: # add 1 bit and run the next string
carry(x_list, cur_max)
sock = socket(AF_INET, SOCK_STREAM) #create socket (IP, TCP)
sock.connect(("asis-ctf.ir" , 12435))
print sock.recv(1024)
sock.send("Sattelite\n")
while True:
res = sock.recv(1024)
print res
if "ASIS" in res: # get the flag
break
eval_list, cur_max = string_to_expression(res) # convert input expression to list
eval_str = cal_ok(eval_list, cur_max) # calculate the right answer
print "ans: " + eval_str
sock.send(eval_str+'\n')
ok = sock.recv(1024)
print ok
if "OK" not in ok:
break
sock.close()
```

Finally, we get the flag!

flag: `ASIS_5b5e15ec25479ac8b743c6e818d75464`

## Comments