Metadata-Version: 2.4
Name: ariadne-re
Version: 0.1.0
Summary: A thread through the labyrinth of obfuscated binaries.
License: GPL-2.0-or-later
Project-URL: Homepage, https://github.com/0xPSYPrime/Ariadne
Classifier: License :: OSI Approved :: GNU General Public License v2 or later (GPLv2+)
Requires-Python: >=3.13
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: triton-library==1.0.0rc4
Requires-Dist: z3-solver>=4.13
Requires-Dist: capstone>=5.0
Dynamic: license-file

<div align="center">

<img src="assets/wordmark.svg" width="440" alt="Ariadne">

![Python](https://img.shields.io/badge/python-3.13-3776AB)
![Platform](https://img.shields.io/badge/target-Windows%20%7C%20Linux-5c6370)
![Powered by](https://img.shields.io/badge/powered%20by-Sogen%20%C2%B7%20Triton%20%C2%B7%20Bitwuzla-E0A43B)
![Status](https://img.shields.io/badge/status-research-orange)
![License](https://img.shields.io/badge/license-GPL--2.0--or--later-blue)

</div>

## What it is

Ariadne is a binary analysis toolkit for understanding programs that do not want
to be understood. It runs a target inside a userspace emulator with real Windows
DLLs, then reasons about what it did with symbolic execution. You get to watch a
binary behave, find the input it is waiting for, run a single function on its own,
and unwrap code hidden behind a binary, all without a full virtual
machine and without executing the sample natively.

It works on real 64-bit Windows PEs and Linux ELFs, including stripped, packed,
and heavily obfuscated ones. It targets x86_64 only. 32-bit x86 is not supported.

## How it fits together

Ariadne is really three tools working as one. Sogen runs the target as a real
process, with real Windows DLLs and real syscalls, so it is the ground truth for
what the program actually does. Triton rides alongside that run as a symbolic
shadow, turning the instructions that touch your input into symbolic expressions
instead of plain numbers. An SMT solver then answers questions about those
expressions, such as which input would send a branch the other way. Triton ships
with Bitwuzla, which Ariadne uses by default, and Z3 as a fallback.

On its own each piece has a gap. An emulator tells you what happened for one
input, but not why. A symbolic engine can reason
about many inputs, but it needs a faithful machine to run on, which is exactly
the hard part on Windows. A solver is powerful, but only as good as the
constraints you hand it. Put together they close each other's gaps. Sogen gives
Triton a real machine to shadow, Triton gives the solver constraints drawn from
real execution, and the solver gives Sogen the next input worth trying. That loop
is the whole toolkit, and it is where the value comes from.

## What it does

- **Observe behaviour.** Trace API calls, registers, memory, reads and writes, the
  call stack, imports, and code that unpacks itself at runtime.
- **Find the input.** Measure where and how a program takes input, then solve for
  an input that passes its checks.
- **Study a function.** Call one routine in isolation and learn what it computes,
  including whether a solver can invert it or whether it is a hash to work around.
- **See through anti-analysis.** Answer the usual debugger, timing, and sandbox
  checks so evasive samples keep running.
- **Devirtualize.** Recover the logic and control flow of VM-obfuscated functions,
  reading the interpreter concretely so the work stays small.

## How it works

Ariadne runs the program for real and watches one path at a time. As Sogen
executes, Triton keeps a shadow of the parts you care about. For every
instruction in scope it builds an expression over the input bytes instead of a
plain value. Anything outside that scope, such as a library call or a key schedule that
does not depend on the input, runs concretely at full speed and never enters the
shadow. The shadow is how Ariadne knows which parts of the program the input
reaches, and what it has been turned into along the way.

Each time the concrete run takes a conditional branch that depends on the input,
Ariadne records the condition. To reach a different path it takes one of those
recorded branches, asks the solver for an input that makes it go the other way while
keeping the earlier choices intact, then runs the program again with that input.
Step by step it walks outward into the binary, each run reaching a little
further, and each answer is a real input the program accepts rather than a guess.
This is the thread: the concrete run is the way in, and the recorded branches are
how it finds the way back to the parts it has not seen yet.

This is why path explosion is not the wall it usually is. A classic symbolic
engine tries to follow every branch of every path at once, and the number of
paths doubles at each branch until it explode. Ariadne never forks. It follows a
single concrete path per run and only revisits a branch when it has a concrete
reason to, so the cost grows with the branches it chooses to explore, not with
the exponential number of paths in the program. The heavy input-independent
machinery, including the dispatch loop of a virtual machine, runs concretely and
costs nothing symbolically, so the work the solver sees stays small.

## Roadmap

- [ ] Finish the unpacking feature. `observe_unpacked` still misses code that
      unpacks in place over a binary's own sections.
- [ ] Find stronger malware analysis use cases, such as trigger extraction,
      config and C2 decoding, and behavioural triage.
- [ ] Devirtualization: emit structured C from the recovered CFG and semantics.
- [ ] Devirtualization: handle more VM shapes (threaded and call-based dispatch,
      multi-head and struct-based VMs) beyond the single-dispatch case.
- [ ] Close CFG coverage automatically with concolic branch flipping, so you give
      a seed instead of a hand-picked list of inputs.
- [ ] Make input localization fully push-button, feeding `locate_input` straight
      into `recover_input` with no manual addresses.
- [ ] IDA plugin: a service so repeated queries do not re-emulate from
      scratch, and a "solve for an argument that return X value in a function" action.
- [ ] Evaluation: benchmark against angr and TritonDSE on a shared corpus.
- [ ] Improve linux binary analysis

## Why the name

In the Greek myth, Ariadne hands Theseus a ball of thread so he can walk into the
labyrinth, face what is inside, and still find his way back out. That is the job
here. The maze is an obfuscated binary, and the toolkit is the thread.

## Built with

- [Sogen](https://github.com/momo5502/sogen) (GPLv2), a syscall level userspace
  emulator for Windows and Linux, used to run the target with real system DLLs.
- [Triton](https://github.com/JonathanSalwan/Triton) (Apache-2.0), a dynamic
  symbolic execution library, used to lift and reason about what ran.
- [Bitwuzla](https://github.com/bitwuzla/bitwuzla) (MIT), the SMT solver Ariadne
  uses by default, bundled with Triton, used to turn constraints into inputs.
- [Z3](https://github.com/Z3Prover/z3) (MIT), an SMT solver, the fallback and
  usable directly.
- [Capstone](https://github.com/capstone-engine/capstone) (BSD), the disassembler
  Triton builds on.

## Inspired by

Concolic testing in the tradition of DART and SAGE, dynamic symbolic execution
tools such as [TritonDSE](https://github.com/quarkslab/tritondse), and the line
of work on symbolic deobfuscation of virtualized code. Ariadne brings that way of
working to real Windows binaries running on real DLLs.

Test targets are generated with [Tigress](https://tigress.wtf/), used only at
development time and not redistributed.

## A note from me

I do not consider myself a strong programmer. What I am is someone genuinely in
love with reverse engineering. A large part of this toolkit was built with the
help of AI tools, and I would rather say that directly than pretend otherwise. I
also want to be clear that I did not just let a model run on its own. I've read the
research and the engineering behind these ideas, and Ariadne only exists because
of the people who did that work first. So this note is a thank you to them. The
references below are the papers and tools Ariadne stands on, and the credit for
the hard ideas here belongs to their authors.

## References

Concolic and symbolic execution:

- P. Godefroid, N. Klarlund, K. Sen. [*DART: Directed Automated Random Testing.*](https://doi.org/10.1145/1065010.1065036) PLDI 2005.
- K. Sen, D. Marinov, G. Agha. [*CUTE: A Concolic Unit Testing Engine for C.*](https://doi.org/10.1145/1081706.1081750) ESEC/FSE 2005.
- P. Godefroid, M. Y. Levin, D. Molnar. [*Automated Whitebox Fuzz Testing*](https://www.microsoft.com/en-us/research/publication/automated-whitebox-fuzz-testing/) (SAGE). NDSS 2008.
- C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, D. Engler. [*EXE: Automatically Generating Inputs of Death.*](https://doi.org/10.1145/1180405.1180445) CCS 2006.
- C. Cadar, D. Dunbar, D. Engler. [*KLEE: Unassisted and Automatic Generation of High-Coverage Tests.*](https://llvm.org/pubs/2008-12-OSDI-KLEE.html) OSDI 2008.
- F. Saudel, J. Salwan. [*Triton: A Dynamic Symbolic Execution Framework.*](https://triton-library.github.io/) SSTIC 2015.
- L. de Moura, N. Bjorner. [*Z3: An Efficient SMT Solver.*](https://doi.org/10.1007/978-3-540-78800-3_24) TACAS 2008.

Deobfuscation and devirtualization:

- M. Sharif, A. Lanzi, J. Giffin, W. Lee. [*Automatic Reverse Engineering of Malware Emulators.*](https://doi.org/10.1109/SP.2009.27) IEEE S&P 2009.
- K. Coogan, G. Lu, S. Debray. [*Deobfuscation of Virtualization-Obfuscated Software: A Semantics-Based Approach.*](https://doi.org/10.1145/2046707.2046739) CCS 2011.
- B. Yadegari, B. Johannesmeyer, B. Whitely, S. Debray. [*A Generic Approach to Automatic Deobfuscation of Executable Code.*](https://doi.org/10.1109/SP.2015.47) IEEE S&P 2015.
- T. Blazytko, M. Contag, C. Aschermann, T. Holz. [*Syntia: Synthesizing the Semantics of Obfuscated Code.*](https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/blazytko) USENIX Security 2017.
- J. Salwan, S. Bardin, M. L. Potet. [*Symbolic Deobfuscation: From Virtualized Code Back to the Original.*](https://doi.org/10.1007/978-3-319-93411-2_17) DIMVA 2018.
- D. Xu, J. Ming, Y. Fu, D. Wu. [*VMHunt: A Verifiable Approach to Partially-Virtualized Binary Code Simplification.*](https://doi.org/10.1145/3243734.3243827) CCS 2018.
- R. David et al. [*QSynth: A Program Synthesis Based Approach for Binary Code Deobfuscation.*](https://github.com/quarkslab/qsynthesis) BAR 2020.

Tools and software Ariadne is built on:

- momo5502. [Sogen](https://github.com/momo5502/sogen), the syscall level userspace emulator that runs the target. Ariadne would not exist without it.
- Quarkslab and J. Salwan. [Triton](https://github.com/JonathanSalwan/Triton), the dynamic symbolic execution library.
- [Bitwuzla](https://github.com/bitwuzla/bitwuzla), the SMT solver used by default, bundled with Triton.
- Microsoft Research. [Z3](https://github.com/Z3Prover/z3), the SMT solver used as a fallback.

## Licensing and credits

Ariadne is licensed under the **GNU General Public License v2.0 or later**, the
same family as Sogen, so the toolkit and the Docker image that bundles Sogen are
distributed under one consistent license. See [LICENSE](LICENSE).

## Learn more

See the [wiki](wiki/Home.md) for what each capability does and small examples of
how to use it.
