Thursday, 22 May 2014

The winter of 2014 was cold.

During the months of January and February of the year 2014 I gave an objective to myself. It was to finish the masters dissertation to the point of submission. I also learned that picking a hard topic was probably not the best idea but it was certainly rewarding. Nonetheless, I still received a distinction (the Oxford version of an A) for the work. So, I'm happy share it with the world welcoming any sort of feedback.

If you're interested you can read the full paper here: The full paper

Personal computing devices and servers are becoming more powerful by the day through hardware parallelisation. Such advances require developers to look into concurrency in order to take advantage of the new computing power. However, much of the code is written without formal verification and checked only heuristically through unit or other tests. This dissertation will show how Communicating Sequential Processes (CSP) can be used to detect errors in an application that supports concurrent execution. This is done by isolating common concurrency problems and mapping them into CSP representations. Finally, Failures-Divergences Refinement (FDR) software package is used to perform refinement checks to detect the errors in the source code. This process allows the developer to build assertions that their code must pass to prove its correctness. 

I would like to thank my advisor, Dr. Andrew Simpson, and the Software Engineering Program staff for their guidance and quick responses. This project could not have been accomplished without the generosity, patience and accommodation of the family scholarship fund. I am particularly grateful to the American people for providing the opportunity and the Lithuanian people for their infinitely delicious food and heavenly honey. Finally, I wish to thank my wife, Diana, for her love, support and conversation. 

Wednesday, 21 May 2014

A simple one

CTF challenges can be great fun. One evening had a few minutes and decides to work a simple one from CSAW. It can be downloaded from Here's the break down:

A server listens on a TCP socket port 31338. It forks on a connection creating a new process for each client. The server send sends some data and reads some data into a buffer. At that point the handling function either calls exit or returns. The last part is interesting because on return the exploit can succeed and gain execution. If the exploit fails to set up the stack correctly, the process will exit without gaining execution.

This challenge is a good starter, although I would not expect this sort of a situation to come up anymore. Perhaps in old or deliberately bad software. This situation was more common in the 90's. The use in the exercise is to go through the motions of learning how stack corruption vulnerabilities work.

First, a connection comes in. The server forks to create a new process:

The handle function is called with the client socket file descriptor as the first parameter. Here we see a modern compiler convention to place the parameters on the stack using a mov instruction. Older compilers usually use the push instruction. The end result is the same because at the time of the call the first thing on the stack (i.e. [esp]) is the first parameter. This fits the calling convention used by the called function.

The handle function has several things in its stack frame: buffer, some byte variable, 32bit integer:

We see that the buffer is of size 2047 bytes due to it's large offset. Specifically, it is the distance between the buffer and the next variable. 0x80C - 0xD which is 2060 - 13 = 2047. I called the next variable 'zero' because that is the value that will be assigned to it after the overflow happens. The cookie actually simulates a stack canary implemented early on by compilers to protect against stack based buffer over flows. We'll see later how that can be over come for this challenge.

The cookie will contain a random value seeded off of the time that the handle function runs. At first glance I was thinking that we would have to try to guess it based on the approximate time of the server. But it gets better. Here we can see the assignment:

We can also see that the cookie is being saved of to a location in the data segment called secret. Later, that is how the function will know if the cookie has been corrupted.

Let's look at the next interesting chunk of code:

There are two calls to the send function. First one loads the address of the buffer as the parameter which actually sends the stack location of the buffer. Second send loads up the cookie and sends that to the client. So we really have all information we need. This would also explain the funny characters we get upon connection to the server.

Finally, the overflow occurs when the receive function is called. That is because it reads 4096 bytes into a 2047 byte buffer. 

After the receive, the zero variable is assigned with zero value (just one byte). This is here just to make things slightly harder for you. Next the cookie is checked against the secret value. If the value matches then the function jumps away to return. The return is what will trigger the exploit and give us the code execution. If the value do not, then the code falls through and executes exit.

So the stacks looks like this: 
(low addr)
 [ 2047 bytes ] | [ zero byte] | [cookie] | [ few registers ] | [return addr] | [ socket]
(high addr)

This means that we need to write to the socket a value large enough to overwrite the return address which will become the EIP when the retn instruction is executed. So the actual exploit looks like this:

This code will read from the socket the address of the buffer and the cookie which will allow us to put those values into the exploit string.

Simple! Right? Well, not if you've never done this before.