Challenge Description
Memory Acceleration While everyone was asleep, you were pushing the capabilities of your technology to the max. Night after night, you frantically tried to repair the encrypted parts of your brain, reversing custom protocols implemented by your father, wanting to pinpoint exactly what damage had been done and constantly keeping notes because of your inability of forming new memories. On one of those nights, you had a flashback. Your father had always talked about a new technology and how it would change the galaxy. You realized that he had used it on you. This technology dealt with a proof of a work function and decentralized networks. Along with Virgil’s help, you had a “Eureka!” moment, but his approach, brute forcing, meant draining all your energy. Can you find a quicker way to validate new memory blocks?
Source Files
Source Analysis
From source.py
We have to provide two integers first_key and second_key such that
phash(block, first_key, second_key) == 0. block will be presented by
the challenge server. If we do it 4 times, we get our flag.
It’s roughly like how we validate blocks with Proof-of-Work in blockchains
Lets take a look at phash from pofwork.py
Few things to note here -
rotlis 32-bit rotate leftsboxis AES sbox, so that we dont try linear/differential cryptanalysis XD- Every operation in
phashcan be roughly thought on working on 32 bituints since each operation is preceded by&m (0xffffffff)which makes everything operate mod - Which means
rv1,rv2,x,y,z,uare all 32bit values including our keys, i.e `rv1 = 0x2423380b4d045 & m = 0x80b4d045 - Insted of a block,
md5(block)is hashed, so we have little to no control over the message and we have to actually expoit the keys.
Finding relevant key1 and key2 seems difficult by bare logic, dont worry
since the first block provides a subtle hint
"You don't have to add the z3 solver to your firmware ever again. Now you can use it forever.
We can make an SMT model in z3 and let it do its wonders!
But first let us demarcate the function so it’s easier to refer
function setup
key1 loop
key2 substitution
key2 loop
final multiplication
Enter Z3
Since we are dealing with 32 bits entities only, we will use theory of
bitvectors. Where each variable is simply considered a collection of
bits and all the operations are treated as symbolic computation upon
those sets of bits. Pretty much like a hardware circuit, where each
component is say a 32 bit register.
Representing function setup
Representing key1 loop
Wait, how will sub work?
Good question, it wont the sub is a previously defined python function which
expects python int to index the SBOX and return a value. It wont
understand BitVec as index and so wont our model understand our function!
Theory of Arrays
SMT solvers are so mature, we can use multiple theories to create and solve a
model!
With theory of arrays, we can essentially declare an array with arbitrary index
and arbitrary stored value.
Representing key2 substitution
What is ZeroExt? Note that subkey2 after substitution is a list of 8-bit
entities. Now this one wouldn’t look much severe to a programmer since all
programming languages dont bother much about adding two integer values c/c++
would give type warning but just add the smaller value to a bigger value
without ranting. whereas python doesn’t bother at all. But if we think like
a hardware, you will be bothered when presented to add a 32-bit register to
a 8-bit register. Since we require this value later, we make it a 32 bit value
by Extending with 24 zeros in the front (if we were not dealing with uint32
we would have sign-extended these 8-bit values.
Representing key2 loop
Now after all this bizarre symbolic computation, we are not done yet, we are
not here just to model but to ask the solver to find the values of key1 and
key2 such that this symbolic function evaluates to 0
Calling a solver
Putting it all together
Lets go!
Two hours later (external animation).
Well, no key yet?
I know, lets discuss a few problems and workarounds
Too complicated model
- Too many multiplications. There are 13 loops and a lot of multiplications. And as one may know, factoring has never been easy.
- We dont even have a tentative time by which the solver will spew a satisfying model. This is the general drawback of SMT/SAT solvers.
- Not breaking the problem as (an actually intelligent) human
So lets analyze the problem carefully part by part.
Re-analysis
- The final value is
h(final) = h(part 2)*u*z (part 1)and we need it to be 0 finalhwill be 0 if sum of least significant0ofh,uandzexceeds -
as overflows are ignored in 32-bit multiplication.
- What if we can get
hof key2 loop to 0 by its own?
Reversing only key2 loop
It seems to be working but only for a limited number of values, lets see how
frequently can it work independent of h from first loop.
It appears that if we entirely ignore key1, and let h be whatever it
desires to be i.e. random, we can have our luck with finding key2 with
roughly 1 in 400 chance (ignoring the zeros for u*z entirely)
So we can bruteforce for key1, try solving for key2 and this should
take a couple of seconds and lo we are done.
Solve Script
Final Test
Post solve wanderings
I solved the challenge manually by prompting bruteforce 4 times. I wanted to
create a netcat script, but couldn’t as Hack The Box terminated all instances
post the CTFs so I cant access the server.
I wonder why is there an uncanny resemblance between the hash function and a hash collision challenge I created last year for zh3r0 CTF v2
Anyways, it was a fun challenge, I had a lot of fun and hope that some weird soul had its fun too reading this writeup :)