one_gadget/aletheia/README.md

Aletheia

Empirically verify that one_gadget's gadgets actually launch a shell on a real machine. Aletheia loads a real libc, jumps a live process to a gadget offset with registers/stack crafted to satisfy that gadget's constraints, and checks that a real /bin/sh runs ls / and reproduces the host root.

This is dev-only verification tooling. It lives outside lib/ and bin/ so it is not part of the published gem.

Status

Verifies amd64, i386, arm, aarch64, riscv64 and MIPS (both byte orders; 61 PASS at level 2, strict). The backend is picked from the target ELF's machine, and the transport from the host arch: the arch that matches the host runs natively, the rest under qemu-user — so the same suite works on any host (an aarch64 host runs aarch64 natively and the others under qemu; an x86_64 host does the reverse). arm runs via stub self-injection (no gdbstub); its execve gadgets verify, but posix_spawn gadgets are SKIPped because qemu-arm lacks the clone3 syscall glibc uses to fork (see docs/DESIGN.md). Set ALETHEIA_FORCE_QEMU=1 to run a native arch under qemu too. riscv64 answers L2 only: gdb has no syscall catchpoint on that architecture, so nothing stops at the execve entry and the L0 signal goes unanswered — the verdict still comes from a real shell running ls /, which is what decides PASS anyway. MIPS has a backend per byte order, since each needs its own emulator and stub, and its musl fixtures are run as the stub's own libc rather than loaded beside it: musl recognises its own implementation and hands a second dlopen back the one already running, so it can only be verified by being the libc the stub comes up on. Other architectures plug in behind Aletheia::Arch — see docs/ADDING-AN-ARCH.md.

Prerequisites

• Ruby (same as one_gadget: >= 3.3), run from the one_gadget repo so ../lib is on the load path.
• gdb for native verification (the host's own arch).
• For a foreign target (e.g. amd64 libc on an aarch64 host): qemu-user, gdb-multiarch, and the target's cross-compiler (gcc-<arch>-linux-gnu). No flag — a foreign target auto-selects the qemu transport.
• The parking stub(s), built once (native + any cross stub whose toolchain is installed):

aletheia/build_stubs.sh

Usage

# Verify the top (level-0) gadgets of a libc (benign register defaults):
aletheia/bin/aletheia verify spec/data/aarch64-libc-2.43.so

# amd64 target on an aarch64 host runs under qemu-user automatically:
aletheia/bin/aletheia verify --level 1 spec/data/libc-2.23-*.so

# Verify EVERY gadget one_gadget finds (level 1):
aletheia/bin/aletheia verify --level 1 spec/data/aarch64-libc-2.43.so

# Completeness test: poison uncontrolled registers so unlisted
# dependencies fault (finds missing-constraint bugs):
aletheia/bin/aletheia verify --strict spec/data/aarch64-libc-2.24.so

# Restrict to specific offsets, machine-readable output:
aletheia/bin/aletheia verify --offset 0x4bc00,0x4bc04 --json spec/data/aarch64-libc-2.43.so

Reading the result

Per gadget: PASS / EXEC / FAIL / SKIP.

• PASS — the spawned shell actually ran ls / and listed the real root (L2). The strongest signal; it does not depend on one_gadget's own interpretation.
• EXEC — the gadget reached execve("/bin/sh") with a valid argv/envp (L0), but the harness could not drive ls / through this particular shell (e.g. a fixed -c command baked into libc). The gadget works; only the L2 drive is inconclusive. Not a failure.
• EXEC* (promotable) — an EXEC gadget that becomes a full L2 PASS once the uncontrolled register the code writes as argv[1] is nulled (which an attacker controls). Effectively a usable gadget; the harness proves it by retrying with uncontrolled registers nulled.
• FAIL — a complete, satisfied plan reached neither a shell nor any output. Under --strict this is a candidate one_gadget bug (usually a missing constraint); use discover.py to find the faulting instruction (see docs/DESIGN.md).
• SKIP — the satisfier could not build a plan (a harness limitation, not a verdict).

Exit code is nonzero only if some gadget FAILs (EXEC and SKIP do not).

See docs/FINDINGS.md for verified results and bugs, and docs/DESIGN.md for how it works.