wk3 - structs, SAT solvers

Theme: Reverse Engineering, Structures, SAT Solvers

Knapsack (150)

Given

"Let's go shopping! How many of each would you like?"

Solve

Statically analyse the compiled binary using Binary Ninja. Head to main() to gain a general understanding of the program. Inside main(), we see a scanf() function that takes in 6 inputs, separated by hyphens. Conditions are listed after the input is read in. If any input is negative, the program returns the message "Nah, that's not how we count around here!" and will not deliver the flag. If the output from calling process() on all six inputs equals zero, that will also deny us the flag.

Head to process() to see what it does. Inside process(), we see two conditions that evaluate to zero, which means we should avoid these. We must ensure the sixth argument is greater than zero, and we must also ensure var_6 * arg6 + var_1 * arg1 + var_2 * arg2 + var_3 * arg3 + var_4 * arg4 + var_5 * arg5 = var_0, where var_0 to var_6 are hardcoded int-32 values.

To engineer the desired input that will pass the conditions, we create a Python script using Z3 solver. Define variables and add to the solver object all the conditions that need to be true. \

from z3 import BitVec, Solver, sat

# declare three integers, the goal of our solver
# make sure the type is correct 
# here, all are int32_t
# order should match the order in which they are entered in the program
in_1 = BitVec('in_1', 32)
in_2 = BitVec('in_2', 32)
in_3 = BitVec('in_3', 32)
in_4 = BitVec('in_4', 32)
in_5 = BitVec('in_5', 32)
in_6 = BitVec('in_6', 32)

# create solver and enforce constraints per the program control flow
s = Solver()
# give the solver requirements s.t. when fulfilled, output is TRUE
s.add(in_1 >= 0x0, in_2 >= 0x0, in_3 >= 0x0, in_4 >= 0x0, in_5 >= 0x0, in_6 > 0x0)

var_0 = 0x645
var_1 = 0xd7
var_2 = 0x113
var_3 = 0x14f
var_4 = 0x163
var_5 = 0x1a4
var_6 = 0x244

process_result = var_1 * in_1 + var_2 * in_2 + var_3 * in_3 + var_4 * in_4 + var_5 * in_5 + var_6 * in_6
s.add(process_result == var_0)


# solve!
assert s.check() == sat, "Error, not satisfiable!"
print(s.model()) # print out the inputs I need

Enter the output from Z3 script when prompted. Obtain flag.

Flag

flag{1ts_n0t_t0_b4d_s0lv1ng_pr0bl3ms_w1th_Z3!_c3d3d36a98a4c0db}

Flips (200)

Given

• Binary executable Goal

• Enter a bunch of numbers correctly

Solve

Scope the program statically on Binary Ninja.

Head into main() to see what occurs. The program begins by calling a traversal() function. And if the fail flag equals zero, we get the flag. This means that within the traversal() function, something happens that could set the fail flag to one. We want to prevent that happening. traversal() is called by passing in the address of node_0. This suggests we are traversing some linked list or tree structure.

Head into traversal(). Notice that it is recursive. First, we call traversal() on the input node plus 8 bytes. Then we ask for two user inputs: one unsigned int-64 and one signed int-64. Both get converted to an unsigned long within get_input(). Then, we check that the output from calling process() on the two user inputs is not equal to the input node dereferenced. If not equal, set the fail flag to one. This means we want them to equal. Afterwards, we call traversal() again on the input plus 16 bytes. The recursive calls suggest that we are traversing the left node, then processing the current node, and moving on to the right node. This implies a binary tree structure. Specifically, we're doing in-order traversal.

Go into process(). A variable is initialised to be zero. This acts as a counter. In every iteration of the for-loop, we XOR the two input arguments. If the XOR-result is bitwise-ANDed with 1 and is true, we increment one to the counter. We right-shift the XOR-result by one step in the next iteration. Effectively, this is checking every corresponding bit-pairs in both input numbers. If they are different (XOR will be true, and bitwise-AND that with 1 gives us 1, otherwise 0), we add the count by one. The counter thus gives us how many bits differ in the two numbers. This is also known as the hamming distance between two numbers expressed in binary.

Combine findings from process() with traversal() to crystallise our goal: for every node, we enter two numbers whose hamming distance equals the value of the node. This requires us to first determine the order of node traversal, and for each node, determine what two numbers to enter.

Let's determine the order of traversal through this binary tree by tracing the code. The first call to traversal() is made on node_0. Inside node_0, it calls traversal() on itself's address plus 8 bytes, which is node_1 (see .data section in decompiled code). Inside node_1's call, it further calls node_3.

Continue this reasoning through the end. We end up with this order of traversal: 3, 1, 4, 0, 5, 2, 7, 9, 6, 8.

For each node, determine what two numbers to enter. Take node 3 as an example. Node 3 holds the value 0x0e in memory, which is 14 in decimal. We want to enter two numbers with exactly 14 bits that differ. The simplest way to do it is enter 0, then enter a number with exactly 14 1's, which equals 16383 in decimal.

Side note on entering numbers: they should be inputted as decimal numbers instead of hex or binary. We know this from get_input(), where the input strings are specified to be interpretted as base-10 numbers.

Apply the same reasoning for all nodes. Here are the results for the second number to enter (let the first number always be zero):

• Node 3 - 16383

• Node 1 - 8191

• Node 4 - 524287

• Node 0 - 262143

• Node 5 - 131071

• Node 2 - 262143

• Node 7 - 1048575

• Node 9 - 16383

• Node 6 - 32767

• Node 8 - 524287

Run the program. Enter the numbers for each node when prompted - in order! Get the flag.