Nothing is Unreachable: Automated Synthesis of Robust Code-Reuse Gadget Chains for Arbitrary Exploitation Primitives

2025. 9. 18.

USENIX `25

Nicolas Bailluet, Emmanuel Fleury, Isabelle Puaut and Erven Rohou

Univ Rennes, Inria, CNRS, IRISA

Univ Bordeaux, CNRS, LaBRI

Timeline of Eternal Memory War

2

• The memory war continues as patches drive attack evolution
• As mitigations are introduced, memory exploitation trends are also evolved

Timeline of Eternal Memory War

3

• The memory war continues as patches drive attack evolution
• As mitigations are introduced, memory exploitation trends are also evolved

i.e. Shellcode injection

i.e. ret2libc, ROP

i.e. DOP, privilege escalation

NX

CFI

Timeline of Eternal Memory War

4

• The memory war continues as patches drive attack evolution
• As mitigations are introduced, memory exploitation trends are also evolved

i.e. Shellcode injection

i.e. ret2libc, ROP

i.e. DOP, privilege escalation

NX

CFI

Still some exploits shows that it’s valid

Motivation - Limitation of ROP

5

• ROP is still powerful attack, but the ability to chaining payload highly relies on attacker’s capabilities

• Which values, memory regions are attacker-controllable?
• What gadgets attacker can use?

• To overcome these problems, they suggest automated tools

- Without attacker’s capabilities

- Various memory layout

• Existing works tries to automatically generate ROP chain

But,

• It is only for stack layout
• It could rely on attacker-uncontrollable values 🡪 which led fail to generating

​

Background - ROP

6

• ROP (Return Oriented Programming)

• Code reuse attack that chains together existing code fragment
• Reuses code snippets (gadgets) already present in memory
• Make fake call-stack to hijack control-flow
• Usually used with memory corruption (e.g. stack buffer overflow)

Background – SMT Solver & Taint Propagation

7

• SMT(Satisfiability Modulo Theory) solvers determine the satisfiability of logical constraints �over background theories.

- They find whether variable values exist that satisfy given conditions.

- Traditional solvers are SAT (boolean Satisfiability Theory) 🡪 It only regards Boolean

- SMT can handle more various logical constraints

• Tatin propagation is analysis technique that internal program’s data-flow

🡪 Expect to how tainted data are propagated in the program

​

• Taint?

- Taint means that data from untrusted sources (e.g. user-input)

Threat Model

8

• Attacker can rewrite the code-pointer (e.g. memory corruption vuln)
• Attacker can bypass ASLR before running the attack
• NX/DEP is activated
• CFI mitigations are not enforced

• They do not aim for automated end-to-end exploit, �so they don’t focus on other exploit techniques

Novelty of ARCANIST

9

The attacker sets goal, then ARCANIST tells it is possible or not (if possible, it shows how to reach the goal)

To do this, they combine two concept; robust reachability & Component-based program synthesis

• Robust reachability

• Contrary to standard reachability, it tells whether a point in the program can be reached, � whatever the value of uncontrolled variables (only considered by controlled variables)
• It’s inspired by taint propagation

• Component-based program synthesis

• Finding a sequence of components (gadgets) that always fits specification

🡺 They build one-shot SMT queries with this two concept

Comparison between SOTA and ARCANIST

10

• Unsound synthesizer�: It’s unsound, because it rely on uncontrollable values

• Limited exploitation layout�: They only regard the stack

SOTA

Comparison between ARCANIST and SOTA (Cont’d)

11

One-shot SMT query

Robust reachability

• Robust synthesizer

: it takes into parameter the exact exploitation layout, so it knows exactly which regions it can use

ARCANIST

Workflow of ARCANIST

12

• Goal : initial state 🡪 attacker’s goal
• Exploitation Layout : Attacker’s (un)controllable values, register, memory regions, etc.

Workflow of ARCANIST (Cont’d)

13

• Gadget Extractor + Translator : Extract ROP gadgets from binary, then encode in SMT format
• Formula Builder : Generate SMT query with attacker’s context & binary information

Robust Gadget Chaining Problem

14

How to robustly chaining the gadgets whatever uncontrollable (or unpredictable) values

They define changing problem as formula

S : Specification (goal)

A : Assumption (initial state)

GS: How to achieve goal with no fail

p : controllable

u : uncontrollable

Robust Gadget Chaining Problem (Cont’d)

15

Definition

🡪 Could you reach the final state regardless of the u, after executing n gadgets?

GS: How to achieve goal with no fail

p : controllable

u : uncontrollable

SMT solver will judge the result with this formula

Evaluation

16

• Hardware Setup

- Intel® Xeon®Gold 5218 CPU 64 Cores @ 2.30 GHz, with 93 GB of RAM

• Competitors

- Existing models : Ropium, Angrop, SGC

Evaluation

17

fcall# : synthesize the function with # parameters

Thought about this paper

18

• Novel way to solve the complicated problems
• There are some real-world study to show its performance
• Good paper structure

• Strong assumption of threat model
• If CFI become more standard, it’ll become useless
• It relies on taint propagation, but it could be generate some errors

APPENDIX

19

Thank you

20