Let’s automatically identify weird machines in software.

Combating software exploitation has been a cat-and-mouse game ever since the Morris worm in 1988. Attackers use specific exploitation primitives to achieve unintended code execution. Major software vendors introduce exploit mitigation to break those primitives. Back and forth, back and forth. The mitigations have certainly raised the bar for successful exploitation, but there’s still opportunity to get closer to provable security gains.

I discussed the use of weird machines to either bypass these mitigation barriers or prove a program is unexploitable as part of the DARPA Risers session to an audience of PMs and other Defense officials earlier this year at the D60 conference. Describing this problem concisely was difficult, especially to non-practitioners.

Why weird machines matter

Attackers look for weird machines to defeat modern exploit mitigations. Weird machines are partially Turing-complete snippets of code that inherently exist in “loose contracts” around functions and groups of functions. A loose contract is a piece of code that not only implements the intended program, but does it in such a way that the program undergoes more state changes than it should (i.e. the set of preconditions of a program state is larger than necessary). We want “tight contracts” for better security, where the program only changes state on exactly the intended preconditions, and no “weird” or unintended state changes can arise.

Unfortunately, loose contracts exist in most software and are byproducts of functionality such as linked-list traversals, file parsing, small single-purpose functions, and any other features that emerge from complex systems. Modern attackers leverage these unintended computations and build weird machines that bypass exploit mitigations and security checks. Let’s take a look at an example of a weird machine.

struct ListItem
{
    ListItem* TrySetItem(ListItem* new_item)
    {
        if (!m_next)
            m_next = new_item;

        return m_next;
    }

    struct ListItem *m_next = nullptr;
};

The function ListItem::TrySetItem looks to have these preconditions:

• You must pass this and item in, both as pointers
• this and item must be allocated and constructed ListItem instances

However, once machine code is generated the preconditions are actually:

• The this parameter must be a pointer to allocated memory of at least 8 bytes
• You must pass a second parameter (item) but it can be of any type

This is an example of a loose contract which is inherent to the way we write code. An attacker who has overwritten the m_next pointer can leverage this function to check to see if memory at an arbitrary address is set: if yes, then the attacker may leak the memory, if not, then the attacker may set the memory.

Tightening the contract

One type of loose contract is the “execution” contract, which is the set of possible addresses that are valid indirect branches in a program.

Windows NT in 1995 is an example of a loose execution contract, where all memory marked as ‘read’ also implied ‘execute.’ This included all data in the program – not just the code. In 2003, Microsoft tightened the execution contract when it introduced non-executable data (NX, DEP) in Windows XP SP2. Microsoft further improved the contract in 2006 when it introduced Address Space Layout Randomization (ASLR) in Windows Vista, which randomizes the location of executable code. 2016 saw the introduction of Control Flow Guard (CFG) with Windows 8.1/10, which validates forward-edges of indirect branches point to a set of approved functions.

In the chart below, it’s clear that few valid indirect destinations remain. This tight “execution” contract makes exploitation much more difficult and the need for weird machines greater, dramatically increasing the value of weird machines. If we can tighten the program contract more, it would make weird machines that much more difficult to identify.

What “weird” looks like

Identifying weird machines is a hard problem. How do we identify loose contracts when we don’t even know what the contract is in the first place? Automatically identifying these weird machines would allow us to triage properly whether a vulnerability is in fact exploitable and whether it would be unexploitable in the absence of weird machines.

One way to programmatically describe a weird machine is through Hoare triples. A Hoare triple describes how the execution of a piece of code changes the state of the computation: the preconditions necessary to move into a new state and the post conditions which describe how to leave a state. When we identify weird machines, we can tighten such contracts automatically by removing them or constraining the preconditions to be exactly what the state expects. This will get us one step closer to creating a program that’s provably secure.

Revisiting our example, we can add dynamic_casts to enforce the contract preconditions. If we analyze the snippet of code as a Hoare triple we notice that the preconditions for the function’s execution are loose, such that any address can be passed to the function. Furthermore, the post conditions are nonexistent such that once executing, the function will set or return memory regardless of program state.

struct ListItem
{
    ListItem* TrySetItem(ListItem* new_item)
    {
        if (!dynamic_cast<ListItem*>(this) ||
            !dynamic_cast<ListItem*>(new_item)) {
                // This path should not be allowed
                abort();
        }

        if (!m_next)
            m_next = new_item;

        return m_next;
    }

    struct ListItem *m_next = nullptr;
};

The dynamic_casts are runtime guards which check to validate that the function is operating on the intended pointers. This new function is decidedly not as useful in exploitation as it once was.

So how do we find them?

There are numerous difficult problems on the road to a solution. The first being scale. We don’t care about simple test cases, we care about real code deployed to billions of people today: browsers, operating systems, mail clients, messaging applications. Automatically identifying weird machines on these platforms is a significant challenge.

Given a set of possible execution paths and their pattern of object creation and access, we must identify program slices with specific and controllable side effects. These slices must themselves be Turing complete. The behavior of these “Turing thunks” may be different outside of their normal placement in the execution paths or with different data states. To scale our analyses, we can break the problem into subcomponents.

Starting with identification of Turing thunks, analyze their side effects, and determine their reachability. We can use data flow analysis and shape analysis to identify these “Turing thunks” and measure their side effects. The side effects of these identified weird machines will be measured to determine how these candidate weird machines compose. Alterations to the global state could alter the execution of subsequent weird machines. Data flow provides paths that are transformable based on controlled input. Shape analysis aids in reconstructing heap objects, layout, and the interactions between objects. This helps determine the input constraints necessary to generate a path of execution to a weird machine, as well as the heap state before and after execution of the weird machine.

Once candidates have been identified, it is possible to prioritize based on specific functionality and side effects. We can use symbolic and concolic execution to validate these candidates and machine learning to group candidates by behaviors, execution constraints, and side effects to make later querying easier.

The future of exploitation

In the end, weird machines are a fundamental tool in exploitation. As programs get more complex and mitigations pile on, the importance of weird machines only increases. Finding these Turing snippets and enumerating their properties in real-world programs will assist the next generation of exploitations and security.

Once we can automatically identify weird machines we will have the ability to remove these weird states, and determine the degree of exploitability of the program. We may also be able to prove a specific vulnerability is unexploitable.

Part of the solution to this is an improvement on the terminology, which needs to mature. The other part of the solution is further research into the problem space. While there was interest in the topic, I hope DARPA invests in this area in the future.

The tooling and systems to identify and classify weird machines doesn’t yet exist. We still have a lot to do, but the building blocks are there. With them we’ll come closer to solving the problems of tomorrow.

If you want to learn more about this area of research, I suggest you start with these publications:

• Weird machines, exploitability, and provable unexploitability
• Exploit Programming: From Buffer Overflows to “Weird Machines” and Theory of Computation
• Exploitation as Code Reuse: On the Need of Formalization
• The Weird Machines in Proof-Carrying Code