run go.sh and check your flag...
According to the go.sh file the engineTest binary could be run with four arguments called cp, ip, /dev/stdin (dv for short), and op. The cp, ip and op files were provided, they contained some kind of binary data, probably a bunch of 64bit numbers based on their hexdump.
Reversing the binary suggested that it contained some kind of a VM. Some more reversing revealed that it is basically a 1D, 1bit, binary spreadsheet app.
Observations:
- Running go.sh printed " Wrong! ".
- A cell was exactly one bit and was stored in an array, packed into bytes.
- The cells were indexed like this: bitfield[index >> 6] >> (index & 63).
- There were 4 instructions, binary AND, OR, XOR and a TERNARY operator, each 5 bytes.
- The instructions were read from cp.
- Initial values for some of the cells were read from ip and dv. As ip was given, and only dv was unknown the flag was the initial value for some cells.
- Output positions were read from op, these were printed after executing the instruction. The " Wrong! " message had thus came from the spreadsheet.
- The first two cells were always 0 and 1.
- A topological sort was performed on the instructions before executing them, and only instructions that formed a DAG were allowed, thus every cell was written by at most one instruction.
Notable functions:
0x4010C8: main
0x40284C: init_spreadsheet
0x4017DC: ensure_dag_and_topological_sort
0x402C3A: run_spreadsheet
0x402B6C: set_bit_at
0x402BFA: get_bit_at
The following data structures were used in the binary:
The format of an instruction:
struct Inst {
uint64_t opcode, src1, src2, src3, dst;
};
The format of the input files:
struct CP {
uint64_t n_bits;
uint64_t n_instructions;
struct Inst instructions[n_instructions];
};
struct IP {
uint64_t n_in_positions;
uint64_t in_positions[n_in_positions];
};
struct DV {
// bits for in_positions packed into bytes (LSb)
uint8_t in_values_packed[n_in_positions/8];
};
struct OP {
uint64_t n_out_positions;
uint64_t out_positions[n_out_positions];
};
The format of the output written to stdout:
struct Output {
// bits for out_positions packed into bytes
uint8_t out_values_packed[n_out_positions/8];
};
The main spreadsheet structure:
struct Spreadsheet {
uint64_t n_bits;
uint64_t n_instructions;
uint8_t bitfield[(n_bits + 63) >> 6];
uint64_t sorted_instruction_indices;
uint64_t current_instruction_index;
};
At this point it had became evident that a SAT solver could be used to find the flag. I had implemented the spreadsheet logic in Z3 and searched for a solution that would yield a message that is not " Wrong! ".
The relevant part of the python script:
solver = Solver()
inps = [BitVec("inp_%i" % p, 1) for p in range(n_in_positions)]
bits = [BitVec("bit_%i" % p, 1) for p in range(n_bits)]
outs = [BitVec("out_%i" % p, 1) for p in range(n_out_positions)]
solver.add(bits[0] == 0)
solver.add(bits[1] == 1)
for k, pos in enumerate(in_positions):
solver.add(inps[k] == bits[pos])
for i in topological_sort(n_bits, instructions):
if i.op==1: bits[i.dst] = bits[i.src1] & bits[i.src2]
elif i.op==2: bits[i.dst] = bits[i.src1] | bits[i.src2]
elif i.op==3: bits[i.dst] = bits[i.src1] ^ bits[i.src2]
elif i.op==4:
bits[i.dst] = If(bits[i.src1] == 1, bits[i.src2], bits[i.src3])
for k, pos in enumerate(out_positions):
solver.add(outs[k] == bits[pos])
solver.add(Not(And(*[bitsEqByte(outs[i*8:i*8+8], ord(c))
for i, c in enumerate(" Wrong! ")])))
assert solver.check() == sat, "not SAT"
model = solver.model()
flag = []
for k, inp in enumerate(inps):
if k % 8 == 0:
flag.append(0)
flag[-1] |= model[inp].as_long() << (k % 8)
print(bytearray(flag))
Running this script gave us the flag: flag{wind*w(s)_*f_B1ll(ion)_g@t5s}