JUST

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 main:

Ah, we see that the data retrieved by curl is being passed to a curious function called 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 work).

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.

what do

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, like doing and instead of or, and some bit inversions with some xors.

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[0] | 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.

Redemption

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 by the sha1digest function included in the binary. We soon noticed that the sha1digest was 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:

pbctf{haha_yosys_goes_brrrrrr_ae8135d1}

Yes! :)

Addendum 1

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.

Addendum 2

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

-cyanpencil