NiNi's Den

# 2017::HITCON-Quals::Sakura::English

Word count: 769 / Reading time: 5 min
2017/11/07 Share

Ask to input 400 chars, then take it as a 20*20 arry
Next the binary run a function to verify the array
If the verification were success, it would give you the SHA256 hash of you input, which is flag

Let’s take a look at the function I mentioned
There are 150 while loops in this function
Before loops, it initialize lots of variables
Those loops are all similar to each:

!!Notice that if verification was failed, the binary would not stop immediately, it only set the flag to false

It’s not so hard to find out that you can do some symbolic execution to get the right input
But there are so many loops and so many variables
This is a ppc problem (っ・Д・)っ

Because I don’t know how to quickly get the address that I want to put into the avoid of angr’s explorer, I decided to use z3 solver.

For convenient, let’s name some weird function.
Most of them just return the argument directly, so I named them nothing
Some function would return the argument adding by a number, so I named them plus_(number)
OK, I dumped psudocode to sakura_de.c and seperate the syntax of initializing local variables to a text file, variable

Now, all I need to do is to write a script to generate a z3 script

solver.py

sakura_de.c (partial)

variables (partial)

Original Author: Terrynini

Publish at: November 7th 2017, 4:39:57