A vulnerability that was not

This is a history of fail. I was analysing a piece of code, in assembly, that I thought would be vulnerable to a zero allocation bug allowing me to overwrite some bytes of heap space (overwriting a structure with many function pointers!). However, after spending like 2 hours analysing statically the “bug”, and documenting it, I finally discovered it wasn’t vulnerable. #Fail.

The “vulnerable” code

The “vulnerability” I was analysing (that wasn’t a bug finally) was something, stripping non interesting parts, like this one:

// The not really vulnerable code
void foo(int x)
{
  if ( (unsigned int)(x – 69) > 0x63FFFBB )
  {
    return;
  }
 
  // Can I force here a zero allocation?
  char *buf = malloc(x + 68);
 
  // Then overwrite heap memory here...
}

Taking a brief look: do you think it’s exploitable? Well, at first I thought yes but it isn’t. The 1st check is unsigned and there is no possible number we can craft that subtracting 69 is less or equal to 0x63fffbb and, at the same time, adding to that number 68 would be equal to zero. The best way of probing it: using a SMT solver.

The Z3 SMT Solver

A SMT Solver is a tool to solve Satisfiability Modulo Theories problems. The best one I know is Z3, which is half open source (the code is open but you cannot use it for commercial purposes). Using a SMT solver like Z3 I would have solved that problem (the probable exploitability of the previous code) in less than 1 minute but I decided it was better to lose 2 hours of my time analysing a non existing bug… In the following lines I will explain how to setup Z3 and use the Python bindings to check if it’s possible to force a zero allocation with this code or not.

Setting up Z3 and the Python bindings

We first need to download the Z3 code:

git clone https://git01.codeplex.com/z3

This will download a zip file with all the Z3 code (I don’t know why Microsoft did this..). We need to unpack the downloaded zip file and, after that, execute the following commands (for building it in Linux):

$ autoconf
$ ./configure
$ make

This will make the Z3 binary. Now, we need the Z3 dynamic library as it will be used by the Python bindings. We get it by issuing the following command:

$ make so

Now we will have the libz3.so library in the path $CUR_DIR/bin/external/libz3.so. We need to put the environment variable LD_LIBRARY_PATH pointing to this directory or just copy the library to /usr/lib or /usr/local/lib. No matter what you do, after this step you will be able to run the Z3 Python bindings. You can try it by running the example named “example.py” provided with the Z3 source code:

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print s.check()
print s.model()

$ python example.py 
sat
[y = 2, x = 4]

Writing an equation to solve our problem

The provided example for Z3 bindings is just too simple for us. If we try to abstract our problem using only the information given by this example changing from Real to Int it will say that the problem is solvable but we would be wrongly expressing it. A normal “integer” in maths will not be the same like an integer for computers: if we add 1 to 0xFFFFFFFF we will get the number 0x100000000 but, for a computer, it will actually have the value 0x0 (for a 32bit integer). So, instead of using Real or Int, we need to use what is called a “Bit vector”. A bit vector of 32bits is actually what we want. So let’s abstract the predicates of the previous C code and write our first equation with the Z3 bindings for Python:

>>> from z3 import * # Import the Z3 stuff
>>>
>>> x = BitVec('x', 32) # Create a bit vector of 32bits
>>> s = Solver()
>>> s.add(x-68 <= 0x63fffbb, x+68 == ) # Add our equation
>>> s.check() # And check if it's satisfiable
sat

So, according to Z3 and the equation we fed to it, it’s solvable! We can get a valid ‘x’ solution for it calling s.model():

>>> s.model()
[x = 4294967228]
>>> hex(4294967228)
'0xffffffbc'

OK. According to Z3 the value 0xffffffbc would pass both checks, thus, making a zero allocation. However, the equation we wrote is wrong. Why? Because the following comparison is unsigned and we’re making a signed comparison here:

if ( (unsigned int)(x - 69) > 0x63FFFBB )

For making an unsigned comparison we need to change the equation to the following one:

s.add(ULE(x-68, 0x63fffbb), x+68 == 0)

The function “ULE” performs an unsigned less or equal comparison. If we run now our final code:

>>> from z3 import *
>>> x = BitVec('x', 32)
>>> s = Solver()
>>> s.add(ULE(x-68, 0x63fffbb), x+68 == 0)
>>> s.check()
unsat

We will discover that forcing a zero allocation with the 1st check is *NOT* possible as the comparison is unsigned. It would be possible, though, if the comparison was a signed one.

Conclusion

SMT solvers “may not be” a good solution for whole program analysis, however, it helps a lot vulnerability researchers to determine if a bug candidate is actually a bug or not when performing static analysis. For the next time, instead of losing 1/2 hours trying to guess if it can be possible or not I’ll just check satisfiability with Z3 and I recommend you to do the same: humans are clumsy, machines are better for such tasks.