ASIS CTF Finals 2014 - Sattelite (PPC 200)
This task revealed to be pretty easy despite the 200 points. We basically need to connect to a remote service and solve SAT for some boolean formulas. The input format is binary, where a bit at position i represents the value of x_i_ (e.g.: 011 means x1=False, x2=True, x3=True). Here’s an example:
hi all, You must send a string for each level that would make the literal True
send "Sattelite"
Sattelite
(¬x3 ∨ ¬x5) ∧ (x3 ∨ ¬x3) ∧ (¬x5 ∨ ¬x4) ∧ (¬x2 ∨ x5) ∧ (x5 ∨ x4)
00001
OK
The only difficulty we encountered was caused by a bug on the challenge: the length of the binary string passed as input needs to be equal to the number of boolean formulas concatenated with AND, so we need to pad our input with zeroes sometimes (e.g.: (¬x1 ∨ x2) ∧ (x2 ∨ x1) ∧ (x1 ∨ x1) requres a solution like 110 and not 11).