# Hacking Tube

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

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)

Finally, we get the flag!

flag: ASIS_5b5e15ec25479ac8b743c6e818d75464