Tags: reversing quantum 

Rating:

Pwn2Win CTF 2019: HARPA Hyper quantum Login system

DISCLAIMER: I'm the chall author, I just wrote the solution as if I was playing the CTF! Category: Rev Points: 500 Solves: 0

HARPA implemented quantum authentication systems for their machines. We found this prototype and believe it is possible to recover the password. We need your help.

Hints

Even quantum Systems are just Linear operators in disguise. Quantum Information algorithms can be implemented following any convention for the order of qubits in the registers.

Write-up

Rev

We are given 4 files: control.py, chall.qasm, otp/otp{0,1}.csv. After reversing the control.py we conclude that we have partial control of the input to the quantum circuit in chall.qasm. Our input string is decoded in a Base64 variant and the bits are used to choose elements from the matrices stored in otp/otp{0,1}.csv.

def encode_string(s):
    return ''.join(encoding_dict[c] for c in s )

def gen_keys(enc_s):
    if len(enc_s)<BLOCK_EL: enc_s +='0'*(BLOCK_EL-len(enc_s))
    return [enc_s[i:i+BLOCK_SIZE] for i in range(0,BLOCK_EL,BLOCK_SIZE)]

def get_states(keys,otp):
    return [[otp[int(i)][j][kn] for j,i in enumerate(k)] for kn,k in enumerate(keys)]

These selected elements were broken in 16 pieces, and now each piece is appended with an unknown padding and the results are passed as input to the circuit via the generated file converted_input.inc.

def initial_state(s):
    res = np.array(s)
    return res/np.linalg.norm(res)

def setup_state(vec):
    out = ( 'initialize('
            + ','.join('{:.9f}'.format(v) for v in vec)
            + ')'
            + ','.join('b[{}]'.format(j) for j in range(NBITS))
            + ';\n'
            )
    return out

# main

keys = gen_keys(encode_string(pwd))
states = get_states(gen_keys(encode_string(pwd)), otp)

for kn,padding,state in zip(range(len(states)),my_secrets.padding, states):
    with open("converted_input.inc","w") as f:
        print(setup_state(initial_state(state + padding)))
        f.write(setup_state(initial_state(state + padding)))

The result of each run is filtered on one of the output values, it is checked that there are counts for only one state, the resulting state is converted to an integer and compared to the loop iteration counter. If we pass all tests in all rounds, we can login

# In the main loop
target = []
while len(target)==0:
    results = qiskit.execute(circ, backend, shots=30).results()
    counts = results.get_counts(circ)
    target = list(filter(lambda s: s[-1]=='1', counts.keys()))

if len(target)==1 and int(target[0][-NBITS-2:-1], 2) == int(kn):
    count+=1

# Final check
if count==BLOCK_SIZE:
    print("Login successful!")

But, what is it actually doing?

There are many examples of quantum algorithms, but not that many have been fully implemented in qasm. Also, the capitalization in the title spells HHL... After some research, we determine that the circuit implements the HHL algorithm for solving linear systems of the form A*x=b. We are finally able to understand that the circuit is using the state generated from our password and using it as the b. The matrix A must be extracted from the circuit, x is the target and we must determine which b will make the test int(target[0][-NBITS-2:-1], 2) == int(kn) pass.

We must also satisfy len(target)==1, which means our state must have only one component. To understand why, we need some quantum mechanics. A quantum state of N qubits is encoded as a vector of 2^N entries. So, for a 2-qubit state we would have: |psi> = a*|00> + b*|01> + c*|10> + d*|11> => (a,b,c,d). The sum of the modulus-squared of all coefficients of a state |psi> must equal one, and the probability of measuring a certain state is the modulus square of it's coefficient. So, if we have kn=0, we want our state to maximize the chances of measuring |00>, our target state should be (1,0,0,0). Finally, if we multiply A by a vector with only one non-zero entry we get a column of A as a result, and that is our b for that round!

Extracting A

Looking at the qasm code, some parts look random, and some parts seem to follow a pattern. It was possible to identify that the random parts can be reduced to no-ops, leaving a much more treatable circuit. Also, we could find an implementation of the algorithm that follows the same patterns present in the processed circuit.

Using the found implementation code as a reference, we extracted the matrix A following the procedure suggested there.

def get_unitary(code):
    if isinstance(code,str):
        code = get_circuit(code)
    un = qiskit.Aer.get_backend('unitary_simulator')
    return qiskit.execute(code,un).result().get_unitary()

def get_A(U):
    return (-1.j*logm(U[1::2,1::2])).real/(2*np.pi)*2**8

A = get_A(get_unitary('relevant code'))
A = A[:16,:16] #Only need first 16x16 block

Recovering the password

The state we construct from our password is equal to the columns in matrix A up to a multiplicative constant. We can find the most frequent ratios to recover the right constant and retrieve the bit pattern. (Note: in principle, it is possible to have different constants for each column. For reasons I won't go into, I decided to use a single constant when building the chall).

all_ratios = np.round(list((A/(otp[0]+1e-30)).ravel())+list((A/(otp[1]+1e-30)).ravel()),decimals=6)
counter = Counter(all_ratios)
otp_mul = otp * counter.most_common(2)[1][0] #Most frequent is zero
A_approx = np.round(A,decimals=3)
otp_approx = np.round(otp_mul,decimals=3)
np.fill_diagonal(A_approx,-32) # Euler's identity can mess up the diagonal. Use otp values to determine the correct one

rec_keys = np.zeros_like(A_approx,dtype=np.int)
rec_keys[np.where(A_approx == otp_approx[1])] = 1
decoding_dict = { v:k for k,v in encoding_dict.items() }

def decode_string(s):
    dec = ''
    for i in range(0,len(s),6):
        dec += decoding_dict.get( s[i:i+6], '')
    return dec

print(decode_string(''.join([str(v) for v in rec_keys.T.ravel()])))

This prints }zlPevlOS_ot_sMeTsyS_Ra3nML__rom_0t{RB-HTC, which when reversed gives CTH-BR{t0_mor__LMn3aR_SysTeMs_to_SOlvePlz}. This is very close to a flag and we could actually brute-force all the letters that seem to be wrong, but there is a better way. Turns out the OTP is undecidable in four locations (otp[0][i,j]==otp[1][i,j] for 4 pairs i,j) and we only need to brute-force these 4 bits. There is only one string that looks like a flag: CTF-BR{N0_mor3_LIn3aR_SysTeMs_to_SOlvePlz}

Additional comment

Right after the CTF, I talked with the teams that were trying to solve the chall to see how close they were. They had the idea of removing the control bit to process the unitary matrix. While developing the chall I though this could be done, but never tried to implement it as I already had another solver.

I was really bothered after seeing that this solution was not working and I tried to find something wrong with it. At first, I thought that the operator tdg c[0]; could not be ignored as they had done, and that's what I told them, but I was wrong. In fact, they transformed ccx c[0],q2[0],q2[1]; in cx q2[0],q2[1]; and this was the real issue. Originally, if c[0] is zero q2[1] will not flip irrespective of q2[0]'s state, but in the modified version this is no longer the case!

In the end, I kept learning things even after the CTF!

Original writeup (https://github.com/PdPano/writeups/tree/master/pwn2win2019/harpa_hyper_quantum_login_system).