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:

1. parse the input expression, convert it into a string that eval can recognize & evaluate the result.
2. run through 00...0 to 11...1, substitute variables with 0 or 1
3. 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