Introduction
Binary exploitation is a manual and cumbersome process. Nothing is Unreachable: Automated Synthesis of Robust Code-Reuse Gadget Chains for Arbitrary Exploitation Primitives by Nicolas Bailluet et al. provides a novel workflow for automatically chaining gadgets and taking control of a program given an initial lower-level vulnerability. This paper was presented at the 34th USENIX Security Symposium.
A Brief Exploitation Overview
Code-reuse attacks are done with the objective of gaining control of the stack in a program. In simple exploitation techniques, an attacker may inject malicious shellcode or overflow a buffer to change the instruction pointer (rip/eip) value to a controlled address. Using gadgets, short bundles of instructions already present in a program, an attacker can live-off-the-land (meaning, use the existing resources of a binary to exploit it).
Return-oriented programming (ROP) is the formal and more commonly-acquired definition of this method. For example, an attacker may use gadgets from the libc library ending with a return instruction to jump to their own inputted address on the stack. An attacker needs to control the code-pointer and some memory buffer that they will store the address of such gadgets in.
Gadget chains are merely chains of gadgets that are executed sequentially. The process of finding gadgets has been a manual undertaking, mostly through tools that search and isolate gadgets such as ROPgadget. However, it is fully down to the tester or attacker to determine which gadgets will suit their chain, making the selection a lengthy and complex one.
Previous mechanisms to mitigate the manual workload with creating a ROP chain relied on advanced heuristics that often limit and complicate path exploration. Symbolization has been an up-and-coming method, specifically Satisfiability Modulo Theories (SMT) solvers.
Symbolization & Satisfiable Modulo Theories (SMT) Solvers
These solvers handle boolean-structured theories, using abstractions (also called skeletons) to overapproximate satisfiability. A symbolic execution engine is given an unknown, unconstrained symbol which represents an unknown equality, and the solver tracks and builds equations that prove, over a single path, whether that equality was satisfied. The solver then holds these paths, each represented by a state.
Overapproximation is a technique for converting complex arithmetic formulas to more digestible, less limited sets of solutions.
The single most limiting factor in regards to symbolization is path explosion. Path explosion occurs when there are so many possible paths in a program that a solver engine cannot reach (no pun intended) a solution without running out of memory. This effectively crashes the engine and the solver times out. Larger programs with more branches are vulnerable to this consequence as each path will grow more complex, exponentially doubling the number of paths.
Symbolization sounds like a cookie-cutter solution on paper but is not all that helpful for many use cases. In addition, overapproximation introduces the problem of false positives because of broad mathematical constraints.
Taint propagation is an interesting technique to track how data flows within a program. This data, called a taint, originates from user input data which is often an entry point for injections and other malicious payload behaviour. These methods may be useful for tracking how memory ownership changed throughout a program, however, it does not address an underlying problem.
The Gap in Exploitation
From older exploitation techniques like stack buffer overflows and shellcode injection, to the newer Use-After-Free, heap overflow, and House of Heap exploits, an attacker must first establish a foothold in a system. The attacker MUST control a buffer and code-pointer, otherwise exploitation is not possible. Modern heap exploitation techniques provide an advantage over simple buffer methods, which is not requiring a fake call-stack.
An important consideration to make is that with robust protections like ASLR in place, an attacker will first have to leak an address to be able to calculate offsets.
Methodology
One-Shot Synthesis
ARCANIST is a tool proposed to automatically synthesize code-reuse attacks using gadget chains from arbitrary exploitation primitives. The workflow is illustrated in the figure below:
This approach supports stack-based vulnerability, heap-based vulnerability, and limited control layouts. It takes the provided layout as a parameter, assesses the usable regions and the registers mapped to them, and understands how to load gadgets. This is a sound synthesis based on robust reachability [1].
CVE-2022-46152
This vulnerability is found within the OP-TEE Trusted OS application development framework. Any versions prior to 3.19.0 are vulnerable to an Improper Validation of Array Index, where cleanup_shm_refs() is called by entry_invoke_command() and entry_open_session(), mapping to commands that can be executed from userland via the SMC feature. An argument called num_params is not validated, leading to an attacker being able to craft a malicious call that will cause an Out-of-Bounds (OOB) and possibly free fake objects in mobj_put() [2].
Because of this unique exploitation primitive, other verifiers may not be able to synthesize a chain to achieve control-flow hijacking.
In ARCANIST, the stack was targeted as a region for further exploitation. An attacker controls arguments passed to the smc, meaning they control some of the values pushed to the stack. For example, decrementing the return address can be done indefinitely. This is Layout 3, where an attacker has limited control over the stack. This differentiates ARCANIST from other synthesis procedures like SGC as it proposes better adaptability, and one-shot synthesis, even for more complex layouts.
ARCANIST uses robust gadget chain synthesis to understand if there is a sequence of gadgets that leads to execution being controlled by the attacker. The chain must be valid for all cases in the layout through robust reachability and component-based program synthesis, as shown in the figure below:
Given a problem and extracted translated gadgets, the formula builder reduces it to an SMT problem. Then, it is supplied to the SMT solver. If the solver finds a solution, it notes the values that are needed to achieve this path.
Extracting Gadgets
ARCANIST uses the bit-vectors theory to model CPU registers and operations and array of bit-vectors to model memory. Each state is represented as such:
Where is a bit-vector and is an array of 8-bit bit-vectors. This state is then split into predictable and unpredictable variables. Unpredictable variables are those the attacker doesn’t control initially. To transition from one state to another, gadgets are used.
For each gadget within a chain, there are several processing phases:
- Lifting: Translation to an intermediate representation, which shows the semantics and consequences of each instruction
- Control-Flow Graph (CFG) Construction: A CFG is constructed for each gadget, showing conditional flag handling and branch behaviours
- Gated Single Assignment (GSA) Form: The intermediate representation is converted into this. Each variable is labeled at every assignment, making them stateful
To make sure that gadgets execute properly, pre-condition checks are set. For example, to prevent undefined behaviour from occurring, the control-flow graph is used to enforce branching conditions. Memory operations are investigated to ensure that addresses an attacker accessed are all within the bounds of the program. This is necessary to ensure that attacker-used gadgets will not crash the program or cause it to behave unexpectedly. It uses a mayreach predicate that is true only if the data may reach further than that block. If so, pre-conditions need to be checked for that memory block.
In addition, post-conditions are set to encode semantics and taint propagation. Simply, it helps an attacker understand just how data moved throughout program execution. By encoding these semantics, they can then be inputted into an SMT solver, where it can be checked if a specific data input may satisfy exploiting a vulnerability. With this additional tracking, memory operations are also checked to ensure that taint is linked from input to result.
Memory blocks are considered as arrays. If there is a taint at an index in that array, it makes the entire block tainted. This example is the definition of taint propagation.
Symbolization Limitations
As discussed previously, path explosion is a possible consequence of using SMT solvers with larger binaries. Additionally, the search space for picking the gadgets to formulate an exploit grows larger. To take the SMT solver out of the black box, they use gadget library sampling.
Gadget library sampling involves randomly sampling a library into subsets, then simultaneously analysing different subsets, stopping once a viable gadget has been found.
Path explosion also occurs from many possible states occurring in memory writers. For symbolic memory writers where target addresses are unknown and constantly morphing at runtime, the parameter mem-write-ratio is defined to identify gadgets involving memory writes. The final batch attributed to the SMT solver involves a mix of gadgets with no memory writes (50%), some with 5% of memory writes (25%), and the rest with 10% of memory writes (25%) so unnecessary memory writes are pruned and do not incur performance overhead.
Implementation
ARCANIST was written in Python and uses PySMT as its solver and Ropper to extract gadgets. Gadgets are lifted from Binary Ninja’s intermediate representation tooling, and it supports x86, x86-64, and Arm architectures. It was evaluated on 10 CVEs to test precision and performance. In all cases, ARCANIST could synthesize gadget chains, from 537 gadgets to 67,986 gadgets. It took, almost always, at most 5 minutes for the analysis and exploitation to complete, with an outlier of 42 minutes.
In addition, ARCANIST was able to exploit CVE-2022-46152 (the OP-TEE vulnerability). This goes to show that previous tools were not able to formulate such long gadget chains unlike ARCANIST. Although there is still performance overhead with memory writes, path explosion consequences, and random sampling limitations, ARCANIST proposes a novel, automated way to exploit well-known code-reuse CVEs in an arguably more efficient way.