[SMT][Z3][Python] Integer overflow and SMT-solvers

This is a classic bug:

void allocate_data_for_some_chunks(int num)
{
#define MAX_CHUNKS 10

	if (num>MAX_CHUNKS)
		// throw error

	void* chunks=malloc(num*sizeof(CHUNK));

	...
};

Seems innocent? However, if a (remote) attacker can put negative value into num, no exception is to be throwed, and malloc() will crash on too big input value, because malloc() takes unsigned size_t on input. Unsigned int should be used instead of int for "num", but many programmers use int as a generic type for everything.

Signed addition

First, let's start with addition. a+b also seems innocent, but it is producing incorrect result if a+b doesn't fit into 32/64-bit register.

This is what we will do: evaluate an expression on two ALUs: 32-bit one and 64-bit one:

                                            +--------------+
a ---+----------------------------------->  |              |
     |                                      |  32-bit ALU  |  --- [sign extend to 64-bit] --->   |\
b -- | -+-------------------------------->  |              |                                     | \
     |  |                                   +--------------+                                     |  \
     |  |                                                                                        |   | (64-bit comparator)
     |  |                                   +--------------+                                     |  /
     +- | -- [sign extend to 64 bits] --->  |              |                                     | /
        |                                   |  64-bit ALU  |  ------------------------------->   |/
        +--- [sign extend to 64 bits] --->  |              |
                                            +--------------+

In other words, you want your expression to be evaluated on both ALUs correctly, for all possible inputs, right? Like if the result of 32-bit ALU is always fit into 32-bit register.

And now we can ask Z3 SMT solver to find such an a/b inputs, for which the final comparison will fail.

Needless to say, the default operations (+, -, comparisons, etc) in Z3's Python API are signed, you can see this here: https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py.

Also, we can find lower bound, or minimal possible inputs, using minimize():

from z3 import *

def func(a,b):
    return a+b

a32, b32, out32 = BitVecs('a32 b32 out32', 32)
out32_extended = BitVec('out32_extended', 64)
a64, b64, out64 = BitVecs('a64 b64 out64', 64)

s=Optimize()

s.add(out32==func(a32, b32))
s.add(out64==func(a64, b64))

s.add(a64==SignExt(32, a32))
s.add(b64==SignExt(32, b32))
s.add(out32_extended==SignExt(32, out32))
s.add(out64!=out32_extended)

s.minimize(a32)
s.minimize(b32)

if s.check()==unsat:
    print "unsat: everything is OK"
    exit(0)
m=s.model()

# from https://stackoverflow.com/questions/1375897/how-to-get-the-signed-integer-value-of-a-long-in-python
def toSigned32(n):
    n = n & 0xffffffff
    return n | (-(n & 0x80000000))

def toSigned64(n):
    n = n & 0xffffffffffffffff
    return n | (-(n & 0x8000000000000000))

print "a32=0x%x or %d" % (m[a32].as_long(), toSigned32(m[a32].as_long()))
print "b32=0x%x or %d" % (m[b32].as_long(), toSigned32(m[b32].as_long()))
print "out32=0x%x or %d" % (m[out32].as_long(), toSigned32(m[out32].as_long()))

print "out32_extended=0x%x or %d" % (m[out32_extended].as_long(), toSigned64(m[out32_extended].as_long()))

print "a64=0x%x or %d" % (m[a64].as_long(), toSigned64(m[a64].as_long()))
print "b64=0x%x or %d" % (m[b64].as_long(), toSigned64(m[b64].as_long()))
print "out64=0x%x or %d" % (m[out64].as_long(), toSigned64(m[out64].as_long()))


a32=0x1 or 1
b32=0x7fffffff or 2147483647
out32=0x80000000 or -2147483648
out32_extended=0xffffffff80000000 or -2147483648
a64=0x1 or 1
b64=0x7fffffff or 2147483647
out64=0x80000000 or 2147483648

Right, 1+0x7fffffff = 0x80000000. But 0x80000000 is negative already, because MSB is 1. However, add this on 64-bit ALU and the result will fit in 64-bit register.

How would we fix this problem? We can devise a special function with "wrapped" addition:

/* Returns: a + b */

/* Effects: aborts if a + b overflows */

COMPILER_RT_ABI si_int
__addvsi3(si_int a, si_int b)
{
    si_int s = (su_int) a + (su_int) b;
    if (b >= 0)
    {
        if (s < a)
            compilerrt_abort();
    }
    else
    {
        if (s >= a)
            compilerrt_abort();
    }
    return s;
}

( https://github.com/llvm-mirror/compiler-rt/blob/master/lib/builtins/addvsi3.c )

Now I can simulate this function in Z3Py. I'm telling it: "find a solution, where this expression will be false":

s.add(Not(If(b32>=0, a32+b32<a32, a32+b32>a32)))

And it gives unsat, meaning, there is no counterexample, so the expression can be evaluated safely on both ALUs.

But is there a bug in my statement? Let's check. Find inputs for which this piece of LLVM code will call compilerrt_abort():

s.add(If(b32>=0, a32+b32<a32, a32+b32>a32))
a32=0x1 or 1
b32=0x7fffffff or 2147483647
out32=0x80000000 or -2147483648
out32_extended=0xffffffff80000000 or -2147483648
a64=0x1 or 1
b64=0x7fffffff or 2147483647
out64=0x80000000 or 2147483648

Safe implementations of other operations: https://wiki.sei.cmu.edu/confluence/display/java/NUM00-J.+Detect+or+prevent+integer+overflow. A popular library: https://github.com/dcleblanc/SafeInt.

Arithmetic mean

Another classic bug. This is a famous bug in binary search algorithms: 1, 2. The bug itself not in binary search algorithm, but in calculating arithmetic mean:

def func(a,b):
    return (a+b)/2
a32=0x1 or 1
b32=0x7fffffff or 2147483647
out32=0xc0000000 or -1073741824
out32_extended=0xffffffffc0000000 or -1073741824
a64=0x1 or 1
b64=0x7fffffff or 2147483647
out64=0x40000000 or 1073741824

We can fix this function using a seemingly esoteric Dietz formula, used to do the same, but without integer overflow:

def func(a,b):
    return ((a^b)>>1) + (a&b)

( Its internal workings is described in my https://yurichev.com/writings/SAT_SMT_by_example.pdf )

Z3 gives unsat for this function, it can't find counterexample.

Allocate memory for some chunks

Let's return to the allocate_data_for_some_chunks() function at the beginning of this post.

from z3 import *

def func(a):
    return a*1024

a32, out32 = BitVecs('a32 out32', 32)
out32_extended = BitVec('out32_extended', 64)
a64, out64 = BitVecs('a64 out64', 64)

#s=Solver()
s=Optimize()

s.add(out32==func(a32))
s.add(out64==func(a64))

s.add(a64==SignExt(32, a32))
s.add(out32_extended==SignExt(32, out32))
s.add(out64!=out32_extended)

s.minimize(a32)

if s.check()==unsat:
    print "unsat: everything is OK"
    exit(0)
m=s.model()

# from https://stackoverflow.com/questions/1375897/how-to-get-the-signed-integer-value-of-a-long-in-python
def toSigned32(n):
    n = n & 0xffffffff
    return n | (-(n & 0x80000000))

def toSigned64(n):
    n = n & 0xffffffffffffffff
    return n | (-(n & 0x8000000000000000))

print "a32=0x%x or %d" % (m[a32].as_long(), toSigned32(m[a32].as_long()))
print "out32=0x%x or %d" % (m[out32].as_long(), toSigned32(m[out32].as_long()))

print "out32_extended=0x%x or %d" % (m[out32_extended].as_long(), toSigned64(m[out32_extended].as_long()))

print "a64=0x%x or %d" % (m[a64].as_long(), toSigned64(m[a64].as_long()))
print "out64=0x%x or %d" % (m[out64].as_long(), toSigned64(m[out64].as_long()))


For which "a" values the expression a*1024 will fail? This is a smallest "a" input:

a32=0x200000 or 2097152
out32=0x80000000 or -2147483648
out32_extended=0xffffffff80000000 or -2147483648
a64=0x200000 or 2097152
out64=0x80000000 or 2147483648

OK, let's pretend we inserted a "assert (a<100)" before malloc:

s.add(a32<100)
a32=0x80000000 or -2147483648
out32=0x0 or 0
out32_extended=0x0 or 0
a64=0xffffffff80000000 or -2147483648
out64=0xfffffe0000000000 or -2199023255552

Still, an attacker can pass negative a=-2147483648, and malloc() will fail.

Let's pretend, we added a "assert (a>0)" before calling malloc():

s.add(a32>0)

Now Z3 can't find any counterexample.

Some people say, you should use functions like reallocarray() to be protected from integer overflows: http://lteo.net/blog/2014/10/28/reallocarray-in-openbsd-integer-overflow-detection-for-free/.

abs()

Also seemingly innocent function:

def func(a):
    return If(a<0, -a, a)
a32=0x80000000 or -2147483648
out32=0x80000000 or -2147483648
out32_extended=0xffffffff80000000 or -2147483648
a64=0xffffffff80000000 or -2147483648
out64=0x80000000 or 2147483648

This is an artifact of two's complement system. This is INT_MIN, and -INT_MIN == INT_MIN. It can lead to nasty bugs, and classic one is in naive implementations of itoa() or printf().

Suppose, you print a signed value. And you write something like:

if (input<0)
{
	input=-input;
	printf ("-"); // print leading minus
};

// print digits in (positive) input:
...

If INT_MIN (0x80000000) is passed, minus sign is printed, but the "input" variable still contain negative value. An additional check for INT_MIN is to be added to fix this.

This is also called "undefined behaviour" in C. The problem is that C language itself is old enough to be a witness of "old iron" -- computers which could represent signed numbers in other ways than two's complement representation: https://en.wikipedia.org/wiki/Signed_number_representations.

For this reason, C standard doesn't guarantee that -1 will be 0xffffffff (all bits set) on 32-bit registers. However, almost all hardware you can currently use and buy uses two's complement.

More about the abs() problem:

This can become a security issue. I have seen one instance in the vasprintf implementation of libiberty,
which is part of gcc, binutils and some other GNU software. vasprintf walks over the format string and 
tries to estimate how much space it will need to hold the formatted result string. In format strings, 
there is a construct %.*s or %*s, which means that the actual value should be taken from the stack. 
The libiberty code did it like this:

          if (*p == '*')
            {
              ++p;
              total_width += abs (va_arg (ap, int));
            }

This is actually two issues in one. The first issue is that total_width can overflow. The second issue 
is the one that is interesting in this context: abs can return a negative number, causing the code 
to allocate not enough space and thus cause a buffer overflow. 

( http://www.fefe.de/intof.html )

Games

A lot of video games are prone to integer overflow. Which are exploited actively by gamers. As of NetHack: https://nethackwiki.com/wiki/Integer_overflow, https://nethackwiki.com/wiki/Negative_gold.

Summary

What we did here, is we checked, if a result of an expression can fit in 32-bit register. Probably, you can use a narrower second "ALU", than a 64-bit one.

Further work

If you want to catch overflows on unsigned variables, use unsigned Z3 operations instead of signed, and do zero extend instead of sign extend.

Further reading

Understanding Integer Overflow in C/C++.

Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis.

C32SAT.

My other examples: SAT/SMT by Example.


→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.