We are given a binary named
JUST and an endpoint
nc just.chal.perfect.blue 1337.
We run the binary (in a docker sandbox) to see what’s up:
$ ./JUST cat: motd.ansi: No such file or directory Enter a URL:
at this point, we try entering
http://google.com and we get as response:
Enter a URL: http://google.com Retrieving http://google.com
Alright, let’s look at the binary :)
This is a screen of the start of the
main function (some variable names were
inserted by me while reversing:
As you can see, not much happens other than a call to libcurl to retrieve
the contents of an http endpoint.
Let’s go further down
Ah, we see that the data retrieved by curl is being passed to a curious
meme, 8 bytes at a time, xoring the result of a call to
meme with the input for the next call (This reminds of how CBC block ciphers
Note to the reader: the ‘meme’ function name was not put by me. It was already there in the binary.
The output of the
meme is then passed to a function called
sha1digest. The result
of the hash is then compared to something, and then if we pass all those checks the first 8 bytes of the result of
meme are sent to
system() (not included in the screenshot).
Now, what does the meme function do?
Good question. It’s a question that bothered us of a long while. Let’s have a look at it with IDA:
Uh-Oh. That does not look good.
Let’s have a look at the disassembly:
Ummm… it’s a huge, single, massive basic block that contains half a million instructions. No good.
At first we tried to guess what the meme function did, trying stuff like AES or DES or whatever. This, did not work. We tried many things but
meme looked like it was doing random stuff.
So at this point I decided to have a deeper look at how the function was composed. The fact that there was basically no control flow (being a single solid massive basic block), complicated things a lot, and sent us in the direction of this being something similar to movfuscator.
Let’s have a look at the instructions:
The function was mostly made of patterns like the above. A few things were different each time,
and instead of
or, and some bit inversions with some
After a while I realized that this line could basically be translated to:
mem[0xd63] = input[0x3] | input[0x2]
Soon enough, we realized the program was just doing simple boolean logic operations on a
64 bit long bitvector. Patterns were very similar and I started writing a lifter to
express better the logic of whatever
meme was doing.
Spoiler: this took a long time. I ended up parsing the disassembly of
meme in python. This was not a smart idea, but around 4 hours later, I had a 200+ lines python script that took the half a million lines of disassembly and outputted 50k lines of the following:
mem[0xcf5] = ~input[0x4] & input[0x5] mem[0xd63] = input[0x3] | input[0x2] mem[0xdd2] = input[0x2] & ~input[0x3] mem[0xe41] = input | input[0x1] mem[0xeb0] = mem[0xdd2] & ~mem[0xe41] mem[0xf1f] = mem[0xd63] & ~mem[0xeb0] mem[0xffd] = ~mem[0xf8e] ^ input[0x6] mem[0x106c] = mem[0xf1f] ^ input[0x4] mem[0x10db] = ~mem[0x106c] ...
At this time, Robin noticed that no element of the
mem array was written to more than once.
This meant that we had to deal with a circuit, or something. I did not put a lot of weight
on this, and it was a mistake on my part :)
I went on to waste 2/3 hours on trying a tool called
MBA-blast that should simplify mixed-boolean
arithmetic expression, hoping that it could help us understand this mangled mess. But it did
not work at all and just made me frustrated.
We tried pinging random teammates on discord, hoping they had a magic solution somewhere.
But, sadly, did not work either.
The lift, the crane, and the z.
At this point I was on 10+ hours into this challenge, and my mental sanity was almost completely drained. I ran out of insults and curses to throw at the challenge author, in every language I knew of. The situation was critical.
Out of the blue, Robin came in with a desperate suggestion: “why don’t you just try z3?”
Now, you see, z3. never. works. Like angr. You just waste hours on hours on setting them up, and they hang somewhere solving who knows what constraint.
Anyway, I was so desperate I decided to go with it. I wrote another lifter, that did the following:
mem[0xffd] = ~mem[0xf8e] ^ input[0x6] => mem_0xffd_ = z3.Xor(z3.Not(mem_0xf8e, input_0x6))
for every single boolean logic operator. This took around one hour.
Pain. Sorrow. Regret. Hopelessness.
Very surprisingly, z3 finished very fast. Unfortunately, the result was wrong. To be a bit more specific, we were using z3 to build a pre-image of the
meme function. In other words, we asked z3 to give us the correct input to give to
meme such that the output would be the string
/bin/sh;; but when we plugged the input z3 gave us, it was wrong.
Unfortunately, there were, let’s just say, multiple bugs in my lifting scripts.
I was not in my happiest mood, as I would prefer being hit by a school bus and forced to use Windows for the rest of my life instead of having to debug a z3 script on a meme function.
After two gruesome hours spent unhealthily staring at assembly and python, we were still stuck.
All of a sudden, Andy came in clutch by finding a flipped condition, and this happened:
Finally, z3 gave us the correct pre-image. No one could believe it. Miracles happen.
We then rushed to solve the rest of the chall. To summarize, the
sha1digest function compared the hash of the first 8 bytes with the following 24 bytes of the output of
meme. So we basically had to ask z3 for 4 pre-images of the
meme and we were golden.
Or at least we thought. Unfortunately, the sha1 hash we inserted did not match the hash outputted
sha1digest function included in the binary. We soon noticed that the
in fact not
sha1, as it was a custom implementation in which the author, feeling in a exceptionally funny mood, changed a few constants, lol!. My heart is burning with anger.
Since I ran out of insults against the author, I started cursing his family. To solve this issue we just used gdb and stole what was supposed to be the correct hash, and run z3 again to get the pre-image.
Finally, we passed all the checks, and we managed to pop a shell on the server. This was the flag:
Later, the challenge author revealed to us how the
meme function was created. The tool
the author used is called yosis, and is able to synthetize fpga bitstreams from verilog.
It was around 30 lines of verilog, compiled to around half a million x86 instructions.
I could have said not-so-nice things about the chall author in this writeup, but the quality of his ctf-related memes on his twitter account more than make up for the pain we felt while solving this chall.
Go follow him! twitter link