ariadne-re 0.1.0

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 (GPLv2), a syscall level userspace emulator for Windows and Linux, used to run the target with real system DLLs.
• Triton (Apache-2.0), a dynamic symbolic execution library, used to lift and reason about what ran.
• Bitwuzla (MIT), the SMT solver Ariadne uses by default, bundled with Triton, used to turn constraints into inputs.
• Z3 (MIT), an SMT solver, the fallback and usable directly.
• 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, 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, 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. PLDI 2005.
• K. Sen, D. Marinov, G. Agha. CUTE: A Concolic Unit Testing Engine for C. ESEC/FSE 2005.
• P. Godefroid, M. Y. Levin, D. Molnar. Automated Whitebox Fuzz Testing (SAGE). NDSS 2008.
• C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, D. Engler. EXE: Automatically Generating Inputs of Death. CCS 2006.
• C. Cadar, D. Dunbar, D. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests. OSDI 2008.
• F. Saudel, J. Salwan. Triton: A Dynamic Symbolic Execution Framework. SSTIC 2015.
• L. de Moura, N. Bjorner. Z3: An Efficient SMT Solver. TACAS 2008.

Deobfuscation and devirtualization:

• M. Sharif, A. Lanzi, J. Giffin, W. Lee. Automatic Reverse Engineering of Malware Emulators. IEEE S&P 2009.
• K. Coogan, G. Lu, S. Debray. Deobfuscation of Virtualization-Obfuscated Software: A Semantics-Based Approach. CCS 2011.
• B. Yadegari, B. Johannesmeyer, B. Whitely, S. Debray. A Generic Approach to Automatic Deobfuscation of Executable Code. IEEE S&P 2015.
• T. Blazytko, M. Contag, C. Aschermann, T. Holz. Syntia: Synthesizing the Semantics of Obfuscated Code. USENIX Security 2017.
• J. Salwan, S. Bardin, M. L. Potet. Symbolic Deobfuscation: From Virtualized Code Back to the Original. DIMVA 2018.
• D. Xu, J. Ming, Y. Fu, D. Wu. VMHunt: A Verifiable Approach to Partially-Virtualized Binary Code Simplification. CCS 2018.
• R. David et al. QSynth: A Program Synthesis Based Approach for Binary Code Deobfuscation. BAR 2020.

Tools and software Ariadne is built on:

• momo5502. Sogen, the syscall level userspace emulator that runs the target. Ariadne would not exist without it.
• Quarkslab and J. Salwan. Triton, the dynamic symbolic execution library.
• Bitwuzla, the SMT solver used by default, bundled with Triton.
• Microsoft Research. 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.

Learn more

See the wiki for what each capability does and small examples of how to use it.