DEFCON 2015 – fuckup

TL;DR – continuous custom ASLR using a broken PRNG. Collect outputs, SAT solve for the initial state, predict next base address, ROP to victory.

This is a bit of a tour through my first use of Z3 on a CTF challenge, and might be useful other Z3 noobs trying to figure out how to get started.

Background

I’ve bounced off Z3 a couple of times over the last few years. I’d heard that it was useful (or indeed borderline necessary) for solving certain types of CTF challenges – particularly “keygen” style ones, which have always been a weak point for me.

I had a play around with Z3py during Plaid this year, and thought I had the basics down. Being from a development background, it’s quite a paradigm shift (ding, achievement unlocked) to consider that code you’re writing doesn’t actually *calculate* things, or do any of the operations it looks like it’s doing – it just sets up a series of conditions which need to be met.

So, when I reached a certain point of “fuckup” – a pwnable challenge during DEF CON 2015 CTF qualifiers, and it looked like a SAT solver might be the answer, I thought I’d have another go at cracking how to use Z3.

I haven’t found a good comprehensive guide to using Z3 to solve CTF-style problems before, so this is my attempt to create one. Please bear in mind I’m a complete Z3/SAT noob and this might be a baaaaad approach. If you know any better I’d very much appreciate some feedback 🙂

fuckup

This was a 3-point pwnable challenge in DEFCON 2015 CTF qualifiers. We have the binary and are told it’s running on a certain port on a remote server. On connection the binary says:

Choosing 1 gives us more information:

Disassembling the code leads us to a function at 0x080481A6 which we’ll call “move_to_new_location”. Simplifying slightly, this function:

  • iterates a PRNG,
  • does some annoying floating point operations on the random value,
  • maps a read-write buffer at the random address,
  • copies across the binary from its current mapped location,
  • mprotects the .text segment to be read-execute,
  • switches execution to the same function but in the newly mapped area,
  • unmaps the previous area,
  • moves the stack (I think – this ended up not being important).

We are able to get information on the current random value using menu option 3, which on subsequent runs outputs:

  • Current Random: f6f8df10
  • Current Random: 728e8aa9
  • Current Random: 15852476
  • etc

This shows that relocation is happening quite a lot. Checking the binary, relocation is called (again, simplifying) once each time we perform a menu action. Menu option 4 gives us a free stack smash, but the binary and stack are randomly moved around before the smash occurs.

The approach I used was to try to:

  • predict the next PRNG output, therefore knowing the new program base address,
  • then use the stack buffer overflow to build a simple ROP chain,
  • which mmaps some writable memory, reads in some shellcode, and jumps to it.

PRNG state reconstruction

I spent a while looking at the code for the PRNG iteration function – thank you Hex-Rays decompiler for saving me a lot of time! Eventually I remembered that you should google constants, and there was a juicy one in the routine: 0xDA442D24. This took me to an implementation of Well512, a PRNG (the cleanest I could find is in here).

After poring over it for a while, I noticed that the CTF challenge implementation has a (deliberate) bug which means that the effect of an interation on the internal PRNG state is wider than intended, which I think builds stronger logical links between parts of the state, making it easier to solve. This is supposition, since a comment in IRC by the creator said that making that change made it trivially SAT-solvable.

This is the the PRNG iteration routine reversed out:

My hunch was that collecting enough output from this and feeding it into a SAT solver would allow us to recreate the initial state. So I used Z3py to re-create the algorithm and feed in the gathered results, then solve for the initial state. It’s important to note again here that the code in the “iteration” function isn’t actually doing any computation. It is setting up a large set of logical bitwise operators, really a set of simultaneous equations. Then when we add some actual numbers into the mix Z3 will solve these equations.

Here is my eventual source which could predict the next PRNG output:

Looking at the Z3 model then allows us to extract the initial state for all bar one of the values. The one that we don’t know (the DWORD at index 9) is immaterial because it is immediately replaced on the first iteration of the PRNG, without being used. Here is the output from the Z3 model:

Steps along the way

At this point I feel like I’ve given another “just solve it using Z3” CTF solution. This is what I felt about all the Z3 write-ups I’d seen until this point, and I was hoping to write one differently! So, here is how I approached one of the setbacks. If you just want the solution, skip to the end.

I wanted to make sure that my implementation of the code would produce the same outputs as the real PRNG. To do this I gathered an initial state from the binary using GDB and set those up as the inputs to Z3. Then I used the “simplify” function to collapse the Z3 logic. Normally this will give you a large set of conditions, but since the initial states were all known, Z3 will give a numerical value for each eventual PRNG state.

For my initial, incorrect implementation of the algorithm this checking code looked like this:

This showed that the algorithm was broken, with the following output:

Now we had the problem of diagnosing Z3 logic. We could run the function with just numbers and it worked fine, so something was up. But as far as I know you can’t debug Z3 code, because it’s not really performing the operations, it’s just setting up logic so that they can be run in the future. What I did in the end was deliberately break the algorithm in order to store sub-elements of the result in the PRNG state instead. For example, to check what “c” was being calculated as I changed

to

Looking at this number and performing the actual expected operations I found that it wasn’t producing the output I expected. After looking at all the elements I found that this wasn’t doing what I expected:

In python, “>>” operator performs a logical right shift, eg:

However, Z3 objects treats the “>>” as an arithmetic right shift. This essentially means that bit vectors are treated as signed numbers, and extends the sign, meaning:

So around half of the time, my algorithm was breaking. After fixing that I got the pleasant output of:

And from then on it was a case of collecting outputs as in the previous code.

How did I know it was solvable?

I didn’t. I don’t know how you judge that a particular algorithm is solvable using a particular set of inputs in a reasonable amount of time. I had a hunch that Z3 might help, and I went with that. I’m sure there’s a better way 🙂

Full solution

Once I had code to do the Z3 bit the rest was fairly simple plumbing. I knew the address the binary would be at, so I made a simple ROP chain to map an area of executable memory, read from the socket into it, and then transfer execution to it. And here we are:

And the output:

Leave a Reply

Your email address will not be published. Required fields are marked *