Project Aletheia - All gadgets are real (#399)

* Add Aletheia: empirical one_gadget verification harness

Verifies aarch64 gadgets by running them on real libc under gdb and
checking a live shell runs 'ls /'. Dev-only; excluded from the gem.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia findings: mark Finding 1 fixed, add Finding 2 (__sigaction act)

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia findings: note sigprocmask fix generalized across all arches

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia findings: Finding 2 (__sigaction act) fixed via deferred check

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia findings: fix landed as PR #323

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia: level-1 sweep — verify every gadget, layered L0/L2 oracle

Add --level so the harness checks every gadget one_gadget finds, not just
the top-scoring few. Extend the satisfier to handle branch relations
(reg==imm, !=, comparisons, &-mask), the argv/envp builder (array-literal
and pointer forms, with the -c command pointed at 'ls /'), and single
deref == NULL, with cost-ordered branch retry so interdependent
disjunctions pick a consistent branch; parse failures SKIP rather than crash.

Add a layered oracle: L0 confirms execve("/bin/sh") with a valid argv/envp
(syscall entry for execve, /proc/pid/exe for posix_spawn's vforked child),
L2 drives 'ls /'. New EXEC outcome = reached a shell but not L2-drivable,
so working-but-hard-to-drive gadgets aren't mislabelled FAIL. Stream results
and kill wedged gdb process groups so a sweep can't hang or lose output.

Full aarch64 level-1 sweep: 47/47 gadgets, zero FAILs (29 PASS, 18 EXEC).

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia: promote EXEC gadgets, fix posix_spawn pty race + exec detection

Hold the posix_spawn parent stopped (detach-on-fork off) so it can't race
the child on the shared pty, and detect the exec deterministically with a
"catch exec" (the child may run a fixed -c command and exit before a
/proc/pid/exe check). Together these turn most posix_spawn EXEC results
into real L2 PASSes.

Add EXEC promotion: retry an EXEC gadget with uncontrolled registers nulled.
When the code writes an uncontrolled register as argv[1], the benign fill
makes it a garbage string sh treats as a script; nulling it terminates argv
so the shell is interactive and runs 'ls /'. A promoted gadget (EXEC*) is
genuinely usable given that attacker-controlled input.

aarch64 level-1 sweep: 47 gadgets, 0 FAIL -- 42 PASS, 3 EXEC* (promotable),
2 EXEC (sh -c "--", a fixed libc command that can't be driven).

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Aletheia: drive `sh -c -- <cmd>` gadgets, all level-1 gadgets now usable

The do_system/posix_spawn argv can be {"sh","-c",<libc "--">,x21,...}. The
"--" only ends sh's option parsing, so the first controllable operand after
it (x21) is the actual command. Point the first register operand after -c
(skipping the "--"/global separator) at "ls /" instead of the immediate
next element. `sh -c -- "ls /"` then runs it, so the two gadgets that
previously ran a fixed `sh -c "--"` now PASS directly.

aarch64 level-1 sweep: 47 gadgets, all usable -- 44 PASS, 3 EXEC*
(promotable), 0 EXEC, 0 FAIL.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: cross-arch verification via qemu-user (amd64)

Separate transport (native gdb vs qemu-user gdbstub) from the arch/ABI
model, make park_stub self-describing (pre-allocated scratch + prints its
own libc base), and parameterize driver.py off the plan's arch block. The
Runner auto-detects the backend from the target ELF, so an amd64 libc on
an aarch64 host runs under qemu-user with no flag.

Satisfier gains stack-alignment (`rsp & 0xf == 0`) and arch-level register
normalization (amd64 `eax->rax`, `r8d->r8`). posix_spawn under qemu stays
with the parent and lets the forked child run free on the guest tty.

Validated on this aarch64 host: straight-line execve and posix_spawn both
PASS L2, a redirected-offset negative control FAILs, native aarch64 stays
green; libc-2.23 level-1 sweep 10/12 PASS, 0 FAIL.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: set XMM plan registers via 64-bit lanes

gdb-multiarch rejects `set $xmm0 = <int>` ("Invalid cast" -- an XMM register is a
vector union, not a scalar), so the driver crashed mid-setup for any plan pinning
an XMM lane (the satisfier's `(u64)xmm* == NULL` branch), and the gadget never ran.
Write the lanes directly instead. Fixes 5 spurious amd64 libc-2.31 FAILs
(0x51e45, 0x51e55, 0x8418c, 0x84192, 0x84199); that sweep is now 35 PASS, 1 SKIP.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: recognise a writable scratch slot already reads NULL

The satisfier processed `writable: rbp-0x78` (pinning rbp to a scratch write-area)
and then `[rbp-0x78] == NULL` as separate assignments, tried to re-point rbp to a
different scratch region, and skipped on the false conflict -- even though the
first assignment already lands [rbp-0x78] in zero-filled scratch (== NULL).

Teach `satisfied?` that a `== NULL`/`<= 0` deref off a scratch-pointing register
already holds when its target is in the zeroed region (clear of the seeded L2
command). Fixes the last amd64 libc-2.31 SKIP (0xe3d88); that sweep is now
36 PASS / 0 SKIP, native aarch64 unchanged.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: add i386 backend (qemu-user)

Arch::I386 (eax..ebp, esp/eip, qemu-i386, /usr/i686-linux-gnu sysroot, i386
syscall ABI for L0: eax/execve=11, ebx/ecx/edx). Satisfier gains i386's
"<reg> is the GOT address of libc" (base + PLTGOT offset, resolved by the
driver against the load base) and a dereferenced "[X] == 0" (== [X] == NULL).
build_stubs.sh cross-builds park_stub_i386 via i686-linux-gnu-gcc.

Verified end to end on a version-matched fixture (Debian glibc 2.43 i386):
6/6 level-1 gadgets PASS. Older i386 fixtures need a matching-version ld.so
(their init crashes under the 2.43 loader -- i386 is stricter than amd64 here).

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: per-version sysroots for older foreign libcs

An older i386 libc can't be dlopened under the default cross sysroot: its init
crashes under the newer ld.so, and a stub built with the modern toolchain needs
symbol versions the old libc lacks. build_sysroot.sh fetches the fixture's
matching libc6 + libc6-dev .debs (ubuntu), extracts a sysroot with the matching
ld.so, and cross-builds park_stub against that libc (older symbols only). The
transport auto-uses sysroots/<arch>-<major.minor>/ when present (matched on the
fixture's glibc version), with ALETHEIA_LD_PREFIX / ALETHEIA_STUB manual overrides.

All four older i386 fixtures (2.19, 2.23, 2.26, 2.27) now verify end to end.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: document per-version sysroots for older foreign libcs

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: build per-version sysroots on demand

The transport now rebuilds a missing sysroots/<arch>-<ver>/ when it needs one,
from the fixture's own Ubuntu package version -- gated on Arch#version_strict?
(i386 yes, amd64/aarch64 no) so amd64/aarch64 never trigger a needless build.
So the git-ignored sysroots/ can be deleted anytime to reclaim disk; the next
verify of an older i386 fixture rebuilds just what it needs.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: fix sysroot gating + hex deref-zero

- Only build a per-version sysroot when the fixture's glibc differs from the
  default cross sysroot's version (its ld_prefix libc); a toolchain-matched
  fixture (e.g. Ubuntu 2.43 under the 2.43 cross sysroot) uses the default, and
  a half-built sysroot (no park_stub) is no longer accepted.
- Recognise "[X] == 0x0" (hex zero) as a dereferenced-zero, like "[X] == 0".

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* aletheia: add arm (armhf/Thumb) backend

Adds Arch::Arm, cross-built park_stub_arm, and armhf per-version
sysroot support. execve gadgets verify end-to-end; posix_spawn L2
under investigation.

* aletheia: arm self-injection transport + emulator-syscall SKIP

arm runs via stub self-injection (no gdbstub): the stub applies the
plan and jumps to the gadget itself, keeping the run under plain
qemu-user. This fixes arm execve verification and was the diagnostic
that isolated the real posix_spawn blocker -- qemu-arm doesn't
implement clone3 (EABI 435), which glibc 2.43 posix_spawn forks with,
so no child ever spawns.

The oracle now reads qemu's -strace log and reports SKIP (harness
limitation) instead of FAIL when the emulator hits an unimplemented
syscall. arm: execve PASS, posix_spawn SKIP/blocked; amd64/i386/aarch64
unchanged.

* aletheia: temporary clone3->clone hack so qemu-arm can fork posix_spawn

qemu-arm doesn't implement clone3 (EABI 435), which glibc 2.43
posix_spawn forks with, so posix_spawn gadgets couldn't spawn a shell.
The stub redirects the libc __clone3 wrapper to a shim that translates
struct clone_args into the legacy clone (syscall 120) via glibc __clone.
Env-gated (ALETHEIA_CLONE3_HACK) and signature-guarded; wired into the
arm SelfInject transport. arm 0x3affc posix_spawn now verifies L2.

Remove once qemu-arm gains 32-bit clone3.

* aletheia: Finding 3 - arm missing GOT-base constraint (environ gadgets)

arm PIC gadgets that reach environ via the GOT (posix_spawn(...,environ))
require a GOT-base register = $base+got, but one_gadget's arm fetcher
seeds that register to resolve environ without emitting the constraint
(unlike i386's 'reg is the GOT address of libc'). Verified: 0x3afdc (r6)
and 0x543d2 (r7) both PASS once the register is pinned.

* aletheia: host-arch-independent transport selection

Pick Native vs Qemu/SelfInject from the host arch (uname -m vs each
backend's native_on?) instead of a per-arch flag, so every backend runs
natively on its own host and under qemu-user on any other. Give aarch64
a qemu config (qemu-aarch64) so it verifies under qemu on a non-aarch64
host; a native arch forced under qemu resolves QEMU_LD_PREFIX to the
host root. ALETHEIA_FORCE_QEMU exercises the qemu path for a native arch.

aarch64 2.43: 8/8 PASS both native and forced-qemu; amd64/i386/arm
routing unchanged.

* aletheia: per-version sysroots for aarch64 under qemu

Enables older aarch64 fixtures (that SIGILL under the host loader) to be
verified via ALETHEIA_FORCE_QEMU with a matched, on-demand sysroot:
- aarch64 is version_strict; build_sysroot.sh grows an aarch64 (arm64) case
- sysroot building is gated on the qemu transport (native runs load directly)
- default_libc_version reads the actual runtime prefix (host root vs cross sysroot)
- build_sysroot mirrors runtime libs under /usr/lib/<triplet> so a native arch's
  ld.so under qemu can't fall through to the host's newer libc

aarch64-2.27 (unloadable natively) now verifies: 12 PASS / 4 EXEC. Native
2.43 and foreign i386/arm unchanged.

* aletheia: Finding 4 - aarch64 execvpe frame-argv hides argv[1] constraint

aarch64-2.27 execvpe gadgets (0xa3234 family) build argv in the x29
frame: stp x1,x0,[x29,#64] => {"/bin/sh", x0, NULL}. argv[1] is the
incoming x0; the benign fill makes it a non-NULL empty string so sh
exits (EXEC, not promotable). Pinning x0=NULL yields {"/bin/sh",NULL}
and the gadget PASSes. one_gadget emits only the opaque
'x29+0x40 is a valid argv' (it tracks sp-relative stacks, not the frame
pointer), losing the x0==NULL requirement. Documented; fix needs
frame-relative argv tracking.

* aletheia: mark Findings 1, 3, 4 as fixed (docs were stale)

Findings 3 (arm GOT-base, #331) and 4 (aarch64 frame-argv, #333) had
merged fixes but still read 'not yet fixed'/'candidate'. Finding 1's
own 'Suggested fix' subsection also still said 'not yet applied' despite
the top-line Status already saying fixed (PR #323). Updated all three
to reflect the actual, verified, merged state.

* aletheia: fix three harness reliability bugs found via the aarch64-2.23 qemu discrepancy

Chasing a flaky execl gadget under forced-qemu aarch64 (PASS once,
then FAIL consistently) turned up three compounding harness bugs, not
a qemu or one_gadget issue:

1. catch exec corrupted qemu-aarch64 execution mid-function (SIGSEGV
   inside execl/execve). Only useful natively (the qemu transport
   never follows a posix_spawn child, so the catchpoint can't
   usefully fire there); now armed only when connect == "run".

2. Scratch headroom below sp (SP_OFFSET=0x2000) was too tight for a
   gadget landing inside a function whose own prologue allocates a
   large frame (aarch64 execl's ~8.4KB sub sp,sp,...). Silently
   absorbed by an adjacent mapping under native ASLR, faulted
   reliably (and ASLR-flakily) under qemu. Widened SCRATCH_SIZE/
   SP_OFFSET/WRITABLE_BASE (park_stub.c and discover.py's mmap kept
   in sync).

3. Per-version sysroot stubs went stale silently: stub_built? only
   checked existence, so editing park_stub.c (as in fix 2) left
   cached sysroot stubs running the OLD memory layout while the
   satisfier computed offsets against the NEW one -- a silent
   mismatch producing the exact flaky SIGSEGVs that motivated this
   investigation. Now rebuilds when park_stub.c is newer than the
   cached binary.

Verified clean after all three: native aarch64 8/8; forced-qemu
aarch64 2.23 9 PASS/2 EXEC (was flaky, now reliable across repeated
runs), 2.24 8/8, 2.27 13/13, 2.43 27 PASS/1 EXEC; amd64/i386 2.43
4/4 and 3/3; i386 2.19 (fresh per-version sysroot) 9/9; arm execve +
clone3-hack posix_spawn both PASS. Documented in docs/DESIGN.md.

* aletheia: satisfier accepts hex-zero constraint forms (== 0x0, <= 0x0)

one_gadget#334 (pointers use NULL, values use hex 0x0) changed how
zero-value comparisons render, but the satisfier's evaluate/satisfied?/
apply still only matched a bare '<= 0'. Any constraint using that form
(e.g. arm posix_spawn's file_actions check, (s32)[..] <= 0x0) silently
stopped being recognized as the easy zero-branch it always was and fell
through to the unsupported/relational path -- a satisfier regression
this surfaced as arm 0x543d2 flipping from PASS to SKIP.

Introduced a shared ZERO pattern (0 or 0x0+) and used it everywhere a
literal zero suffix was matched, including deref_zero's already-correct
but now-duplicated regex. Verified clean across every arch: aarch64
native 27 PASS/1 EXEC* (unchanged), amd64 11/11, i386 6/6, arm 0x543d2
back to PASS.

* aletheia: satisfier builds chained-dereference (deep-null) scratch state

Closes the 'harness needs a deeper argv/envp/arg0 builder' gap flagged
under Finding 3: a posix_spawn argv/envp passed as a pointer-to-pointer
(e.g. argv=[sp], needing [[sp]]==NULL i.e. argv[0]=NULL) isn't free like
a single sp-relative deref -- [sp] itself is zero-filled, so dereferencing
it AGAIN reads through NULL and faults. null_cost/apply's stack_reg? fast
path wrongly treated ANY deref depth as free; this was silently masked by
Finding 3's investigation using a hand-crafted plan, not the real
satisfier, until the full arm sweep exposed the actual FAILs.

Adds a Plan#mem field (scratch-relative pointer writes) and
Satisfier#apply_deep_null: builds a real pointer chain -- one write per
extra indirection level -- terminating in the always-zero STRING_POOL,
for both sp-relative and settable-register operands. Costed above a
single deref so it's only chosen when no cheaper branch exists (verified:
zero behavior change on amd64/i386/aarch64, where a cheaper branch always
already existed).

Wired through both transports: driver.py writes plan['mem'] via
write_memory (word_size added to each arch's driver_model for the 4 vs
8-byte write); park_stub.c's self-injection gets a new 'mem <off> <val>'
directive (arm, 4-byte). Validated the driver.py path directly by forcing
the deep-null branch on a real aarch64 gadget (PASS, full L2) before
tackling arm's harder C-stub path.

Result: arm libc-2.43's remaining 6 FAILs (0x3b000/2/4, 0xa42c8/4334/4338)
all PASS -- 10/10 gadgets, reliable across repeated runs. Full regression
clean: aarch64 native + qemu (all 4 fixture versions), amd64 11/11, i386
6/6, all unchanged.

* aletheia: cross-arch strict sweep + Finding 5 (i386 envp-via-stack)

First strict sweep across all four arches (previously only run on
aarch64 2.24/2.23). Near-clean: 62/64 level-1 gadgets pass -- amd64
11/11, i386-2.19 9/9, arm 10/10, aarch64 27 PASS + 1 known-promotable
EXEC.

Finding 5 (i386 2.43, 0xed234, not yet fixed): the gadget's first
instruction stores the uncontrolled register ecx into a stack slot a
later envp constraint requires to read NULL. check_envp only inspects
tracked stack content when the envp pointer itself is a bare stack
address (deref_count==0); here envp is [ebp-0x30] (deref_count==1, a
value READ from the stack), so it falls through to the generic opaque
fallback instead of surfacing that ecx==NULL is the real precondition.
Verified: ecx=0 makes the gadget PASS with full L2.

* aletheia: Finding 6 - untracked non-sp/bp register write hides argv content

The 3 known EXEC* (promotable) gadgets on aarch64 (0xc7a40 libc-2.43;
0x9b9e4, 0x9bc5c libc-2.23) all share one mechanism: the argv pointer
register (x4/x1/x0) is set outside the analyzed candidate window, so
within the window it's an opaque "incoming register" the emulator
can't resolve. A later stp writes an uncontrolled sibling register
(x0 for 0xc7a40) into argv[1] through it, but write-tracking is keyed
to exactly two special-cased registers (sp, and since Finding 4 a
named frame pointer) -- any other register's write falls into the
generic writable-only path, discarding what was actually stored.

Verified precisely: for 0xc7a40, setting ONLY x0=NULL (nothing else)
flips the result from EXEC to PASS with full L2.

Different severity than Findings 1/3/5 (true false positives -- a
fully satisfied plan still crashed): here the gadget genuinely does
reach a shell under every listed constraint; it just isn't reliably
interactive, and Aletheia already flags that honestly as EXEC* rather
than PASS. Documented with a fix plan (generalizing write-tracking to
arbitrary registers, which needs a new invalidation mechanism sp/bp
never required) but not implemented -- lower urgency and larger,
cross-arch scope than Findings 1-5, flagged for review before any
implementation.

* aletheia: satisfy compound "writable: [base]+imm" constraints

The operand parser only handled a dereference as a matched [..] pair
wrapping the whole string, so "writable: [rbp-0x78]+0x10" (offset from
a *dereferenced* value, e.g. a store through a pointer read off the
stack) failed to parse at all -- SKIPping the whole gadget (0xe5887 on
libc-2.27) rather than verifying it.

Fix: defer a compound writable constraint until its base's own
argv/envp constraint has run (order_compound_writable_last), and block
that constraint's NULL branch for the same base (@null_unsafe_bases):
with base == NULL, "[base]+imm" is a fixed low address -- a real
unmapped-page write, not a merely-untracked one -- so the cheaper NULL
branch must not be picked here. Once base resolves to a scratch
pointer, "[base]+imm" is satisfied for free (STRING_POOL/WRITABLE_STRIDE
comfortably cover any observed imm).

This also needed pointer_form/apply_pointer to handle a deref-1 "X is
a valid argv/envp" (write the scratch pointer into X's memory, not a
register) -- previously only a bare register (deref 0) was handled.

0xe5887 now empirically PASSes (was SKIP). No regressions across
aarch64 (2.23/2.24/2.43), amd64 (2.24/2.27/2.31/2.43), and i386
(2.26/2.27/2.43) -- amd64-2.19/2.26's pre-existing broken-harness FAILs
are unaffected (confirmed identical without this change).

* aletheia: fix native transport dlopen crash on a version-mismatched libc

Native aarch64-libc-2.27 crashed with SIGILL inside the HOST's own
ld.so (glibc 2.43) while calling the fixture's init: dlopen-ing a full
libc.so.6 as a secondary shared object binds glibc-private,
ld.so-internal symbols (_dl_exception_create, __tunable_get_val, ...)
that aren't ABI-stable across a 16-version gap. Confirmed with a plain
ctypes dlopen, no gdb/Aletheia involved.

The version-matched per-version sysroot (sysroots/<arch>-<ver>/) this
project already builds for cross-arch qemu runs is the fix -- it just
wasn't applied to native runs (the sysroot's own park_stub kept a
generic interpreter path that only qemu-user's QEMU_LD_PREFIX
redirects; a real execve has no such redirection, so it silently fell
through to the host's ld.so regardless). Two changes:

* transport.rb: `sysroot`'s need no longer gates on qemu_transport? --
  a native run is just as version-sensitive as qemu-user.
* build_sysroot.sh now also builds park_stub_native, a second copy
  whose interpreter is the sysroot's own ld.so (--dynamic-linker) with
  a matching runtime rpath, so the kernel loads it directly -- no
  hand-invoked interpreter, so GDB still treats it as a normal primary
  executable with immediately-resolvable symbols (no pending-breakpoint
  dance). Transport::Native picks it whenever sysroot is needed.

driver.py: `set breakpoint pending on` (defensive, for the above) and
`set sysroot` on a remote (qemu-user gdbstub) connection -- gdb's own
hint that reading a remote target's symbols over the wire instead of
from the local sysroot copy is slow; didn't fix the separate
amd64-2.19/2.26 crash it was aimed at, but is a genuine improvement
with no observed regression, so kept.

Aletheia: aarch64-2.27 is now 13/13 PASS (was 0/13), reproduced with a
fully wiped sysroots/ cache. No regression on aarch64-2.23/2.24/2.43,
amd64-2.43, or i386-2.27 (all re-swept after this change).

* aletheia: satisfy dereferenced equality to a nonzero literal

evaluate/satisfied?/apply's final fallback only handled a dereferenced
value required to be zero (deref_zero -> null_cost/apply_deref_null)
or a bare-register relation (parse_relation, LHS must be \w+, so a
bracketed "[base+imm]" never matches). "[base] == <nonzero>" fell
through both and SKIPped: libc-2.23's 0xcc610 reads a mode flag off
the stack (`mov esi, [rbp-0x50]`, never written within the window)
that a later branch requires to be exactly 1, rendering as
"[rbp-0x50] == 0x1" -- not covered by either path.

Added deref_literal (a single-deref operand plus its target integer,
tried after deref_zero so the zero case is untouched) and its
evaluate/satisfied?/apply legs. Unlike zero, a nonzero target has no
pre-existing zeroed region to point at, so apply_literal must actually
write it -- and since the base (rbp here) isn't constrained by
anything else in the gadget, it also has to pin the register to a
fresh scratch slot first (mirroring apply_deep_null's settable-register
branch), then set_mem the literal there.

0xcc610 now empirically PASSes (was SKIP). No regressions: amd64-2.23
is otherwise byte-for-byte identical to before (same single pre-existing
FAIL at 0xcc52f, unrelated), and aarch64-2.43/amd64-2.43/i386-2.27
re-swept clean (27/27, 11/11, 14/14).

* aletheia: fix arm-2.39 sysroot build + dlopen of a modern libc

Two bugs stacked to make every arm-2.39 gadget FAIL:

1. build_sysroot.sh assumed a split-usr .deb layout (libs in /lib/$triplet).
   glibc 2.39's Ubuntu package is merged-usr -- libs live only in
   /usr/lib/$triplet, no /lib/$triplet -- so the `ln .. $root/lib/$ldso`
   step hit "No such file or directory", `set -e` aborted, and park_stub
   never built. The transport then silently fell back to the generic
   pre-built park_stub_arm (linked against a DIFFERENT libc version).
   Fix: detect the layout and point /lib at usr/lib (as a real merged-usr
   root does) when /lib/$triplet is absent.

2. Even with the right stub, dlopen(target) failed: glibc >= 2.35's
   libc.so.6 imports an ld.so-private symbol (__nptl_change_stack_perm@
   GLIBC_PRIVATE) that only resolves for the PRIMARY libc, never a dlopen'd
   secondary. But a version-matched sysroot links the stub against a libc
   byte-identical to the target, so the target is already mapped as our
   primary libc. Fix: on dlopen failure, if the target file is identical to
   the loaded libc.so.6, use that mapping's base instead of erroring.
   (Older arm libcs lacked the import, so their dlopen happened to work --
   which is why 2.23/2.27 passed and only 2.39 broke.)

arm-2.39 execve gadget 0x88a48 now PASSes (was FAIL). The 6 posix_spawn
gadgets go FAIL -> SKIP: the dlopen bug had masked the separate, already
-known qemu-arm clone3 (syscall 435) limitation, now correctly surfaced.
No regressions: arm-2.23 (2/2), arm-2.27 (5/5), i386-2.27 (14/14),
native aarch64-2.27 (13/13) all rebuilt-sysroot-and-reswept clean, plus
aarch64-2.43 (27/27) and amd64-2.43 (11/11).

* amd64: fix version-matched sysroot for dlopen-of-secondary-libc crash

A big version gap between the runtime ld.so and a dlopen'd secondary
libc crashes amd64 just like the other arches (cf. arm-2.39): the
default cross sysroot's ld.so is far newer than fixtures like
2.19/2.26, and an old ifunc resolver invoked by a much-newer host
ld.so jumps to garbage (observed: SIGSEGV at a bogus 0x500000000,
reproducible via a raw qemu-x86_64 run with no gdb involved at all).

Flips amd64's version_strict? to true and teaches build_sysroot.sh
about the amd64 deb/triplet/ldso, plus symlinks the interpreter at
/lib, /lib64, and /usr/lib since observed PT_INTERP paths vary
(standard amd64 debs use /lib64, one fixture uses /usr/lib directly).

Also fixes transport.rb's Ubuntu-package-version parsing: a couple of
fixtures are plain glibc builds with no "Ubuntu GLIBC" banner to parse
a package version from, so build_sysroot silently never ran and the
mismatched default sysroot was used instead -- looked like a flaky
build failure until traced to the missing match. Falls back to a
small hand-recorded table (from a same-version sibling fixture that
does carry the banner) for the one affected fixture.

* satisfier: handle "reg is a valid pointer" constraint

one_gadget now emits "<reg> is a valid pointer" for a register a libc
call dereferences unconditionally (posix_spawnattr_setsigmask/
setsigdefault). Satisfy it like the bare-pointer argv/envp form: point
the register at readable scratch. Closes the amd64-2.31 0x51df8
strict-mode gap (FAIL -> PASS; sweep now 36/36 strict).

* satisfier: apply register-pinning writable before bounding relations

A "writable: reg+imm" and a "reg != 0" on the same register (libc-2.19
0xc1ca7 / libc-2.23 0xcc52f, which build argv in place at rax and also
branch on rax != 0) conflicted: applying the relation first pinned rax
to a bare literal 1, leaving the writable unsatisfiable (SKIP). Order
plain writable constraints first -- the scratch pointer they pin already
satisfies the != 0 (scratch_satisfies_relation?). Verdict diff across
all fixtures x levels x strict: 0xc1ca7 and 0xcc52f SKIP -> PASS, no
regressions.

Pairs with the one_gadget fix that emits "writable: rax" for these
in-place-argv gadgets.

* satisfier: handle the "readable: reg" constraint form

one_gadget now renders the readable-pointer constraint as "readable:
<reg>" (was "<reg> is a valid pointer"). Add a readable: case that
points the register at readable scratch (STRING_POOL), mirroring the old
pointer-form handling, and drop "pointer" from the argv/envp alternation.
0x51df8 still PASSes strict end-to-end.

* aarch64 arch: treat x29 as a general register, not a stack reg

Pairs with the one_gadget change that emits "writable: x29+imm" for
frame-pointer stores. x29 is not invariantly a valid stack address (like
amd64 rbp), so drop it from stack_regs: the satisfier now pins x29 to
writable scratch when a "writable: x29" constraint requires it, and
strict mode poisons an unconstrained x29. Resolves the frame-pointer
strict FAILs (2.27 0xa32e8/0xa32ec, 2.43 0xc7b00) -> full aarch64 sweep
now PASSes in both benign and strict.

* aletheia: scan for the clone3 site instead of a hardcoded offset

park_stub.c patch_clone3 hardcoded the __clone3 syscall-site offset
(0xb695e, one specific arm fixture), so it only fired for that build --
arm-2.39 (offset 0xb1abe) got "signature mismatch; not applied" and its
6 posix_spawn gadgets SKIPped on syscall 435. Scan the loaded target
libc at its base (bounded by the mapping end) for the unique
"push {r7}; movw r7,#435; svc 0" signature instead. Scanning the loaded
mapping (not the primary libc.so.6 file) is correct whether the fixture
is the primary libc or a dlopen'd secondary.

arm-2.39 posix_spawn gadgets now PASS (6 SKIP -> PASS); arm-2.43
(8c7af7f2, the old hardcoded target) still 10 PASS.

* satisfier: satisfy a libc-global ($base-relative) memory constraint

A branch condition on a libc global, e.g. libc-2.19 0xe654ds
"(s64)[$base+0x3c3e88] <= 0", used to SKIP: the satisfier tried to pin
$base as a register (it is not settable). Instead emit a base-relative
memory write (Plan#base_mem) and have driver.py write 0 to base+off in
the loaded libc before jumping. amd64-2.19s 10 such gadgets go
SKIP -> EXEC (they now reach execve; EXEC not PASS only because their
fixed argv is not ls-/-drivable).

Pairs with the one_gadget change that concretizes rip in compares so the
constraint reads $base rather than a raw rip.

* Model readable-on-load for uncontrolled dereferences

A load through a register the candidate never set up (an incoming register,
e.g. after entering mid-prologue) faults unless that register is a readable
pointer, but the emulator only modeled the loaded value, never the pointer.
Record `readable:` for such a load, deferred like a safe call's :deref so a
later store proving the base writable still discharges it.

Only genuinely uncontrolled loads are constrained: a pointer rooted at mapped
memory (stack, libc base, libc global) is skipped, since a value read from
there is reliably valid. i386's GOT base isn't seeded to $base during
emulation, so its GOT-relative readable is pruned in the fetcher, mirroring
the existing writable pruning.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: apply readables shallowest-deref-first

A nested readable (readable: [base+imm]) resolves its base through
mem_addr_off, which needs base already pointed at scratch by a shallower
readable/writable. Ordering readables shallow-first lets the aarch64 canary
gadgets (readable: x19+off then readable: [x19+off]) satisfy instead of skip.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Model readable-on-load for uncontrolled dereferences

A load through a register the candidate never set up (an incoming register,
e.g. after entering mid-prologue) faults unless that register is a readable
pointer, but the emulator only modeled the loaded value, never the pointer.
Record `readable:` for such a load, deferred like a safe call's :deref so a
later store proving the base writable still discharges it.

Only genuinely uncontrolled loads are constrained: a pointer rooted at mapped
memory (stack, libc base, libc global) is skipped, since a value read from
there is reliably valid. i386's GOT base isn't seeded to $base during
emulation, so its GOT-relative readable is pruned in the fetcher, mirroring
the existing writable pruning.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Disallow posix_spawn_file_actions_* calls in gadgets

A candidate that routes through a file-actions helper is now aborted rather
than accepted. Modeling these soundly is out of reach: the helper returns 0
(so the caller doesn't branch to an error path skipping posix_spawn) only for
a valid fd argument, its success also depends on a realloc that can fail or
fault on a bogus object, the file_actions struct is a glibc-internal
version-dependent layout, and a successful call injects a close/open/dup2 into
the child whose harmlessness depends on the fd. Drops 9 level-2-only gadgets
(2 FAIL, 7 SKIP under empirical verification; no shipped gadget, no PASS lost).

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: solve relations on memory operands

parse_relation only matches a bare register, so a comparison against a memory
operand ([$base+off] != 0, [rsp+0x28] != 0, [r0+8] != 0) had no satisfiable
disjunct and skipped the gadget. Generalize the == literal case to any
comparison operator, deriving the value to store from relation_witness, and
teach the memory read/write helpers about libc globals ($base+off), which the
driver already writes at base + off.

Also fixes apply_deref_null missing the $base case, which made
[$base+off] == 0x0 unsatisfiable while [$base+off] == NULL worked.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: solve register-to-register equality, and pick benign bound witnesses

Two independent causes of skips on settable registers:

* `x3 == x0` / `r3 != r1` compare two registers, which parse_relation (a
  register against an immediate) can't express. Pin whichever side is still
  free, matching or differing from the other as the operator requires.

* An upper bound pinned its register to the bound itself, so a co-occurring
  constraint on the same register conflicted and skipped the gadget --
  `(u64)rax <= 0xfffffffffffff000` alongside `eax == 0x0`. Any value in range
  works, so pick zero, which satisfies both.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: solve register-against-memory comparisons

`x3 == [x1+0x8]` / `r13d == [r14+0x70]` compare a register with a value read
from memory, which neither parse_relation (register against an immediate) nor
deref_relation (memory against an immediate) covers.

Whichever side is already settled drives the other: when the memory contents
are known -- a zero-filled scratch slot, or a value an earlier constraint
stored -- the register is pinned to match, instead of overwriting memory a
co-occurring constraint depends on (`[$base+off] != 0` pins the global, then
`x3 == [$base+off]` must take its value).

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: solve field reads off a pointer, and arm register role names

Constraints like `[[$base+0x1c2438]+0xe8] == 0x0` follow a pointer and read a
field off it. The operand parser had no room for the displacement applied
between the two dereferences (it raised), so every such gadget skipped; model
it as Operand#inner_imm and point the stored pointer at fresh scratch, where
the field lands in the zero fill.

Along the way:
* "must be nonzero" now stores a scratch pointer rather than the literal 1, so
  a location can satisfy `!= 0` and still be dereferenced by another constraint.
* a register compared against memory may carry a displacement (`r3-0x4e0 ==
  [r0+0x8]`); the register holds the matched value less that displacement.
* arm's `ip`/`fp`/`sl` role names resolve to r12/r11/r10, so constraints
  written that way are recognised as assignable registers.
* the self-inject plan grammar gained literal and libc-global writes, which it
  previously rejected outright.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: solve displaced operands and GOT-based argv elements

* A parenthesised sum is an operand, not a dereference: `(u64)(x0 + 0x1) <= 0x0`
  raised in the parser. Strip the grouping parentheses, and let a relation's
  left side carry a displacement -- the register then holds the witness less it.
* At one dereference a displacement adds to the value read (`[sp+0xc8]+0x1`),
  where at two it addresses a field; each is now applied accordingly.
* An i386 argv element off the GOT base is a fixed libc address (the real
  "sh"/"-c" string), so leave it be instead of re-pointing that register at
  scratch and conflicting with the GOT constraint that pinned it.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* docs: record the EXEC backlog and its categories

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Fix cmn-based compares: shifted immediates and unsigned conditions

Two problems made `cmn`-guarded gadgets carry constraints no attacker could
meet, so they looked unusable:

* `cmn x0, #0x1, lsl #12` compares against 0x1000, but the shift operand was
  dropped, leaving 0x1. Fold a constant shift into the operand, and abort the
  candidate on any modifier not modelled rather than silently dropping it.

* An unsigned condition after an add-based compare reads the carry out of the
  addition, not the sum's value: the carry is set exactly when lhs + rhs wraps,
  so the condition bounds lhs by -rhs instead of forcing the sum to zero. It
  now renders `(u64)x0 <= 0xfffffffffffff000` -- the same form amd64 already
  emits for this glibc "syscall didn't return -errno" check -- where before it
  said `(u64)(x0 + 0x1) <= 0x0`, pinning x0 to one value that contradicted the
  gadget's own `w0 == 0x0`. Signed and equality conditions do read the sum and
  keep the additive form.

Three aarch64 gadgets (2.23 0x3d3d8, 2.24 0x3c630, 2.27 0x3eee4) go from
unsatisfiable to verified PASS under Aletheia; shipped level 0/1 output is
unchanged.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: store the smallest "nonzero" witness, promoting only on demand

Satisfying `[rsp+0x2c] != 0` with a scratch pointer wrote a full word where the
code reads a narrower field, clobbering the neighbouring one: two libc-2.23
gadgets stopped reaching execve (FAIL) that otherwise get there.

Store 1 instead, and record the location so a constraint that actually
dereferences it can promote it to a pointer -- still nonzero, so the constraint
that pinned it holds either way. Keeps the nested `[[$base+off]+0xe8] == 0`
cluster passing while the narrow-field gadgets reach execve again.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: satisfy a writable target reached through a pointer

`writable: [rbp-0x48]` asks that the pointer *stored* at rbp-0x48 reference
writable memory -- it carries no trailing displacement, so it isn't the
compound form, and the plain path only accepted a bare register. Allocate the
slot if its base isn't placed yet and store a scratch pointer in it.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* x86: don't model segment-prefixed operands

A segment-prefixed operand reads thread-local storage. A store or load through
one already aborted (the operand parser rejects it), but a compare slipped
through as opaque text, emitting constraints like `fs:[r14] == 0x8` that name a
register the caller cannot set -- it is loaded from a libc global holding
errno's TLS offset.

Every gadget behind one tests errno == ENOEXEC on glibc's execvpe path, which
the caller would have to have arranged beforehand, so they all but never apply.
Rejecting the operand also matches the other arches, whose thread-pointer reads
(aarch64 mrs tpidr_el0, arm mrc p15) are unsupported instructions and already
abort. Drops 6 level-2-only gadgets; shipped level 0/1 output is unchanged.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* satisfier: solve comparisons between two memory operands

`[sp+0x10] == [[$base+0x1c2438]+0x70]` has a register on neither side, so
neither the register-vs-memory nor the memory-vs-literal path applies. Match
the value in memory on both sides, letting whichever side already reads a
known value drive the other so an earlier constraint's pin is preserved.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* arm: seed a GOT base only on lines the candidate executes

Emulation stops at the terminal call, but the GOT-base scan looked at the whole
candidate window, including whatever trailed past that call. A `[r3, r4]` load
sitting there was enough to seed r3 as the GOT base at the window's entry, where
the code actually holds a loop counter -- so a plain `r3 == 0x1` was rendered as
`$base+0xf4004 == 0x1`, a constraint nothing can satisfy (arm-2.27 0x73f54).

Restrict the scan to the executed part of the window. Only a real bl/blx to an
exec* entry ends it: a conditional branch within the same function carries a
similar-looking target symbol but isn't a call.

Level 0/1 output is unchanged; 13 level-2 entries lose a GOT constraint they
never needed, their correctly-rendered counterparts having existed all along.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* arm: seed a GOT base only on lines the candidate executes

Emulation stops at the terminal call, but the GOT-base scan looked at the whole
candidate window, including whatever trailed past that call. A `[r3, r4]` load
sitting there was enough to seed r3 as the GOT base at the window's entry, where
the code actually holds a loop counter -- so a plain `r3 == 0x1` was rendered as
`$base+0xf4004 == 0x1`, a constraint nothing can satisfy (arm-2.27 0x73f54).

Restrict the scan to the executed part of the window. Only a real bl/blx to an
exec* entry ends it: a conditional branch within the same function carries a
similar-looking target symbol but isn't a call.

Level 0/1 output is unchanged; 13 level-2 entries lose a GOT constraint they
never needed, their correctly-rendered counterparts having existed all along.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Bound a candidate window where it is emulated, not where it is read

The previous commit taught the arm GOT scan to stop at the terminal call, which
put knowledge of where a path ends in the one place that happened to notice.
A window is bounded by where emulation stops, so bound it once, in find: every
reader -- emulate and its overrides, the dedup key -- can then treat each line
it is given as one that runs.

The boundary uses the same rule the emulator stops on rather than the looser
scan that locates call sites: that one also matches the posix_spawn setup
helpers, which emulation runs through, so cutting there would drop the call the
gadget is built around.

Output is byte-identical at every level.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Track the rewritten window-bounding change

The branch was squashed into a single commit that bounds the window in find and
leaves the arm fetcher untouched; take that shape here.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Forget caller-saved registers across a call

The emulator carried a call's argument and scratch registers through it, so a
branch on what the callee left behind read as a condition the caller could
arrange: `call __close` then `test eax, eax` became `eax == 0x0`, a precondition
no caller can meet, and the same shape appears after the posix_spawn setup
helpers.

Drop those registers at each accepted call, per the ABI's calling convention,
and refuse to render a branch that reads one -- there is nothing to say about a
value nobody chose. The return register is set to zero instead: these calls are
accepted on the basis that they succeed, so a branch on the result resolves, and
a path needing the failing side contradicts itself and drops.

Level 0/1 output is unchanged; 13 level-2 paths that existed only through such a
branch are gone, and every surviving constraint is byte-identical.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

* Ask for the NULL a callee needs, instead of walking away

__sigaction leaves oldact alone only when it is NULL, and the emulator
demanded that zero already be there. A register or stack slot the caller
picks can be made NULL, so say so and keep the gadget; only a value that
can never be NULL still aborts.

Recovers 31 gadgets at level 1 and 125 at level 2; level 0 is unchanged
and nothing is lost.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Say a required zero once

A branch testing the pointer and the NULL requirement on it ask for the
same zero, so a gadget carrying both stated it twice.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Read a slot back as what the gadget put in it

A load took the dereference at face value even where the candidate had
just stored there, so a constraint on the slot named the value it held on
entry -- which the gadget has already replaced.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Let a NULL element end the argv it terminates

A register another constraint pins to NULL is a valid argv element -- the
one that ends the array -- but the builder tried to make every register
element a string and gave up on the conflict.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Name the mask a gadget applies, instead of giving up on it

An and was unsupported, so a candidate reaching one was abandoned. Model
it: fold the concrete case, name the symbolic one as the operation
itself, and record the flags a following branch reads.

Recovers 11 gadgets at level 1 and 39 at level 2; nothing is lost.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Plan the masks a gadget applies

one_gadget now names a mask it cannot fold, and four shapes of that had
no rule here: a masked value against a non-zero target, a negated one, a
masked read through a pointer, and an address rounded down for alignment.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Read a 32-bit alignment mask as one

Complementing the mask over 64 bits made i386's 0xfffffff0 look like a
field selector rather than the rounding it is. Judge it by the alignment
it rounds to instead, which is width-independent.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Resolve a rounded pointer wherever it names an address

A gadget aligning a pointer mentions the rounding in every constraint
about that address, not only the writable one. Resolve it to the pointer
in each address context, and leave it alone where the mask is a
requirement on bits instead.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Fill an argv the gadget takes from memory

Only register elements were seeded, so an array staged on the stack
stayed zero-filled and the shell got no command. Put the pointer where
each element is read from, fill an array the gadget supplies no strings
for as sh -c <cmd>, and prefer building one over the empty-argv branch:
an empty argv proves only that execve happened.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Leave the choice of argv shape alone

Preferring a built argv cost eight gadgets that a short one had made
observable, while preferring the short one costs those a built argv
catches. Which shape yields a witnessable shell is a property of the
gadget, so it belongs in a retry rather than in a cost.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Build the argv shapes a shell can be driven from

Every controllable element was given a string, so the shell read the one
after argv[0] as a script name and exited. Verified against a real
/bin/sh which shapes stay drivable, and build those: a string at argv[0],
the command where the gadget supplies -c, and the terminator otherwise.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Say which descriptors a gadget closes

A gadget that closes a descriptor on its way to the exec costs the caller
something its constraints never mention. Name the close as the code
performs it, and say what the descriptor must avoid so the spawned shell
keeps its I/O.

Only a descriptor the caller chooses is modelled: one fixed in the code
is nobody's to change, and no path that reaches a terminal call closes
one.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Give a gadget a spare descriptor to close

A descriptor a gadget closes but does not constrain read as 0 out of the
zeroed scratch, so the gadget closed the shell's stdin and nothing could
be driven through it -- an accident of this harness, not a property of
the gadget. Put a spare one there instead, as an exploit would, and leave
alone any descriptor a constraint speaks for.

Write it as a 4-byte field: two descriptors sit 4 bytes apart, and a
word-sized write of one zeroed the other.

Converts 122 of the 142 EXEC verdicts to PASS.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Read the shell option however the gadget spells it

On i386 PIC the -c a gadget passes is a libc global off the GOT
register, not the literal string. Read as an ordinary element it
terminated the array exactly where the command goes, and the shell exited
with "-c requires an argument". Take a fixed string past argv[0] as the
option, whatever it looks like.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Show the string a gadget reaches through the GOT

i386 PIC reaches a libc global through the GOT register, so a fixed
string read as <reg>-<off> where every other arch resolves it and prints
its content. What that register holds is known -- the gadget's own
constraint states it is the PLTGOT -- so read the string from there too.

The -c a gadget passes the shell is now visible as such, rather than
looking like an argv element the caller supplies. 31 elements across the
corpus; no gadget gained or lost.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Stop inferring the shell option

one_gadget now shows the string a gadget reaches through the GOT, so the
-c it passes arrives as a literal like every other fixed string. The rule
that inferred it from position no longer has anything to infer.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>

* Track the argv a gadget builds through a derived pointer

A candidate that rounds a pointer down, or loads one from its frame, and
then builds argv in place had those stores go untracked: no register named
the base. Its argv read as opaque, offering a NULL disjunct its own store
to argv[0] overwrites.

* aletheia: close the EXEC backlog

Strict level-2 is 1163 PASS / 0 EXEC / 0 FAIL / 0 SKIP across all 21
fixtures. Record the three causes that emptied it.

* Keep one store for everything a candidate writes

sp_based_stack, bp_based_stack, reg_based_stack and value_based_stack were
the same Hash with the same default proc, differing only in how they were
keyed and invalidated. Measured across the fixtures, those differences did
nothing: get_corresponding_stack never sees an offset expression (53k calls,
zero), so the substring routing is dead, and a register's key already
follows its value, so the identity guard only ever discarded a history that
was still good -- fragmenting the writes of a post-increment store loop.

Key one store by how the base renders. i386 2.19 0xb58c6 gains the argv it
builds, in place of a NULL disjunct its own store to argv[0] overwrites.

* Model the data-processing instructions ARM shares

aarch64 modelled eight instructions and not nop; a candidate could end on a
no-op with execve still ahead of it. Add the bitwise and shift family both
ARM families spell alike -- and orr eor bic mvn lsl lsr -- in ArmFamily, on
the operator fold now shared from Processor and adopted by X86's and.

Two defects this surfaced, both of which let an invalid gadget through:
a compare rendered a register's folded value in decimal while immediates
were hex, so "0x1 == 0x1" read as "1 == 0x1" and escaped the trivial-relation
check; and that check only compared its two sides textually, so it could
not settle "r1 == r1+0x4" either.

* WIP: name ARM registers as objdump prints them (sl/fp/ip)

* aletheia: resolve a register's role name before addressing the stub

The stub addresses registers by number, and the plan writer pulled that
number straight out of the register's name. A name with no digits -- arm's
sl/fp/ip -- yielded nil and was silently skipped, so the gadget ran without
a value its constraints required and the miss was reported as the gadget's
fault. Normalise through the arch's alias map, and raise rather than skip.

* Name the ARM registers as objdump prints them

objdump never prints the numbered name of an ARM register that has a role
name: r10-r15 always appear as sl/fp/ip/sp/lr/pc. Only the last three were
listed, so any instruction touching sl/fp/ip aborted its candidate as
naming an invalid register -- across the fixtures, sl/fp/ip appear 19421
times and r10/r11/r12 never.

Recovers 37 gadgets at level 2 and 3 at level 1, all verified.

* Model ARM arithmetic on a register operand

add/sub aborted unless the second operand was an immediate, so a candidate
computing a pointer from two registers -- the commonest of all the remaining
blockers, 1225 on aarch64 and 1065 on arm -- ended there. A sum of two
unknowns is no offset from either, so name it as the operation it is, the
way the data-processing family already does.

The stack pointer is the exception: every tracked slot is keyed on it, and
a variable-size frame would put the array a gadget builds at an address only
a caller-supplied register decides, which no constraint states.

Both families had their own add/sub; they now share one in ArmFamily, which
also gives arm the shifted-operand form and aarch64 the 2-operand shorthand.

Recovers 44 gadgets at level 2, none lost.

* A value derived from a libc global is not that global

global_var? asked only whether a rendered value mentions the libc base, so
once arithmetic on a register could be named, "(r3 + $base+0x73fa2)" read as
a fixed global -- and its argv element was resolved to whatever string sits
at that address, hiding that the caller's r3 decides which byte it is. The
gadget then claimed an argv[0] of "/bin/sh" it does not have.

An address plus an unknown names no particular byte; only a bare offset from
the base does.

* Steer a store through (reg + $base+imm) into libc's spare writable data

The satisfier could not place an address only a register decides, so every
gadget carrying one SKIPped. Pin the register to the literal that lands the
sum in the tail of libc's own writable segment, past .bss -- mapped, zeroed,
and used by nothing.

14 gadgets across the four arm fixtures become plannable; 10 verify PASS at
strict level 2. Operands of that shape are refused everywhere else, so no
other constraint is planned as if the fixed address weren't there.

* Place an argv element built from a register and a fixed libc address

apply_argv_list could not place one and skipped it silently, leaving the
register the driver had poisoned as argv[0]: execve took an unmapped pointer
and the gadget reported FAIL for a plan that was never complete.

Steer it into libc's spare data like a store target -- the zero fill is the
valid empty string argv[0] has to be. An element that has to be NULL instead,
or one on a register the plan cannot set, is now refused rather than skipped,
so its gadget SKIPs.

arm-2.27 strict level 2: 38 PASS / 9 FAIL / 3 SKIP -> 44 PASS / 1 FAIL / 5 SKIP.

* Resolve a base sum by pinning its register, once, up front

A (reg + $base+imm) used as an address is the same address whatever reads it,
so pin the register in one pre-pass and let every operand built on it read as
the plain $base+off it has become. That replaces the per-constraint special
cases with one rewrite, and reaches shapes they never covered: a read through
the sum, a chained read, a readable target.

An address-shaped sum inside a disjunction is refused rather than pinned --
giving a poisoned register a valid value for a branch that is then rejected
would weaken the strict test.

Also: a register holding a resolved non-scratch address is no longer mistaken
for a scratch pointer, and the two-operand relation patterns no longer assume
an operand has no spaces in it.

6 more gadgets plan across arm-2.39 and libc-2.43 (arm); all 10 verify PASS.

* Name the value that cancels a libc address the gadget adds

A (reg + $base+imm) required to be NULL cannot be steered: only the negation
of the libc address makes it vanish, and that is not known until the library
is loaded. Add it as a third resolved plan value alongside a scratch and a
load-base offset, resolved by the stub ('reg <n> n <hex>') and by driver.py.

Ranked below the array builder: taking the NULL branch empties an argv, and
which shape yields an observable shell varies per gadget, so cost must not be
what decides it.

The last 8 SKIPs in the corpus become plans, and all 8 verify PASS. The
satisfier now plans every gadget one_gadget reports, on every fixture.

* Ask whether a value is a fixed offset from the libc base

The test for a libc global was "mentions the base, and is not an operation",
so the half that knew about the base lived at the four call sites and the
helper they shared decided only whether the value rendered as "(a op b)" --
a predicate named for a global it never looked for.

A global renders as the base plus an offset and nothing else, so match that
directly. Same answer on every value that reaches it across the 21 fixtures;
output is byte-identical at levels 0, 1 and 2.

* Don't claim the GOT base a candidate establishes itself

seed_got_registers replays the 'ldr rB, [pc]; add rB, pc' pair that set up a
GOT base register before the window. When the window OPENS with that add, the
pair was replayed and then emulated again: rB ended up holding the GOT plus
another whole load base, while resolve went on stating 'rB is the GOT address
of libc' about the register's entry value. arm-2.27's 0x73f2a faulted on the
very load the constraint was meant to protect.

Skip a register the window establishes before its own use, and state what the
load needs instead. The pc bias is settled from the whole candidate up front
too: it was only ever learned from a line already seen, so the first
instruction -- the one whose pc an 'add rX, pc' reads -- was judged with no
evidence. A32 shows neither a width suffix nor a 2-byte stride and keeps the
whole-word bias.

Found by Aletheia; 0x73f2a now verifies PASS at strict level 2. The corpus
changes by two lines at levels 0/1/2: the gadget's constraints, and its
reappearance at level 1, where it had been deduplicated against 0x73f2c for
having been given that same wrong constraint list.

* Drop constraints another constraint already settles

A gadget could ask for the same thing twice, and could offer an option its own
list rules out. A dereference already requires its address to be readable, so a
readable: beside it repeats it; and an address required to be mapped memory is
never NULL, so a "== NULL" option for it can never be taken -- the reader was
being offered a choice that isn't one.

Both rules need the constraint doing the settling to hold outright. Inside a
"||" it is one option among several: "[r8] == NULL || r8 == NULL || r8 is a
valid envp" can be met without reading r8 at all, so a readable: r8 beside it
is load-bearing.

Across the 21 fixtures this drops 97 repeated readable: constraints and 28
impossible NULL options over 105 gadgets, and loses no gadget. A readable:
costs a gadget 5x its score, so the trimmed set moves too: three gadgets that
were dominated by one which only looked like it asked for something else now
show up, and one whose neighbour is now visibly strictly easier drops out. The
default output is unchanged on every fixture.

* Establish a nested readable's own base

order_constraints relied on a shallower readable/writable to point the base
register at scratch before a "readable: [base+imm]" could place its pointer.
That shallower constraint is implied -- reading the pointer AT an address
requires the address readable -- so one_gadget no longer emits it, and
mem_addr_off returned nil: aarch64-2.27 0xa3228/0xa322c went to
"unsupported-or-unsat" with no gadget having changed.

Point the base at scratch when nothing else already has. The plan comes out
exactly as it did when the shallower constraint drove it (x19 -> scratch+0x100).

* Read a dereference as saying its address is mapped

The pass knew an address was mapped memory only when a readable:/writable:
said so. A constraint that dereferences an address says the same thing: the
access has to land somewhere, and address zero is never mapped. So a
"[$base+0x11052c] != 0x0" sitting beside "[[$base+0x11052c]+0xa4] == 0x0" was
asking for what the line under it already requires.

An access near an address settles it too, since a NULL one cannot reach out of
the first page -- bounded by the smallest page, so a far enough offset still
has to be asked for. Readability is not: a dereference nearby says the page it
lands on is mapped, not the one the address itself sits on.

Drops 51 more constraints across the 21 fixtures, taking the longest lists from
9 to 8. No gadget changes at any level.

* Window past the call, where predecessors also live

The window around a terminal call reached 0x2000 back and 0x80 forward, the
forward figure being "enough to cover the call instruction itself". But the walk
running backwards does not mean what it reaches lies behind: a branch
predecessor can sit after the call, in a loop or a later block that jumps back
into the region. arm is the only architecture windowed today and it was losing
28 gadgets on arm-2.39 for want of 0x400 forward.

Measure both directions the same way -- window every architecture against its
own full disassembly across the corpus -- and gadgets start being lost below
0x400 either way (105 at 0x80 forward). A window too small also invents gadgets,
since the line before the first of a window is the last of another and nothing
about it follows. 0x4000 each way leaves 16x, and still disassembles about a
fifth of a libc: terminal calls cluster into a handful of merged windows, so a
wider one costs little.

Recovers those 28 gadgets. Nothing else changes on the 21 fixtures, at any
level.

* Stop two harness slips from reporting a gadget's fault

Both would report against a gadget something that was never about it.

The qemu -strace log and the shell's own output were read as text, but a gadget
builds its argv out of whatever the libc holds at the address it uses, and the
strace prints it. One invalid byte and every later match?/include? raises, which
verify catches and files as "SKIP harness error" against a gadget that ran fine.
Read both as bytes.

And a plan assigned a register under whichever name the constraint spelled, so
arm's fp and r11 -- one register -- were two entries. set_reg exists to refuse a
second, conflicting value for a register; under two names it never saw the
conflict, and the stub would quietly apply whichever came last. Resolve the name
where the plan is read and written.

Every arm fixture still verifies whole under strict (37, 50, 87, 86), as does
aarch64-2.43 (143).

* Keep walking past instructions that decide nothing

A memory barrier orders accesses without changing one, and a landing pad marks
where an indirect branch may arrive: neither is anything to an emulator that
tracks values, yet both stopped a candidate dead. A byte load is nearly as
harmless -- the address is read like any other load, so what the caller must
arrange about it is recorded the same way, but one byte of a word is not a value
this emulator can name, so the register holds what a call would have left and a
path that goes on to depend on it is abandoned rather than described wrongly.

777 dmb, 263 bti, and ldrb the largest unsupported instruction left on either
arm arch (45 aarch64 candidates, 97 arm). Two gadgets follow, both on arm; the
rest of those paths now stop at a call instead.

* Hold the harness to the same style as the gem

Nothing had ever linted aletheia/, so it had drifted: multi-line endless method
definitions, a conditional where a guard clause reads better, a comparison
written as a hash iteration, OpenStruct standing in for a gadget in the specs.
Rubocop autocorrected most of it.

The rest needed deciding rather than correcting. A plan pinning a register to
the literal zero is now asked for by name, since the value there can as easily
be a pointer, a value only the driver can compute, or nothing at all -- which is
why it could not simply become .zero?. The operand parser was called Operand_ to
keep it out of the way of the Operand it produces; it is OperandParser now, and
says what it is. The gadget the specs hand the satisfier is a named struct: what
they pass is the constraint list under test, and building it through one_gadget
would let its own pruning rewrite it first.

* Build the harness with the gem

The harness has lived beside the gem without being part of its build: rubocop's
patterns and rspec's both stop at the top-level lib/ and spec/, so nothing on
this branch was linted or run by `rake`. That is fine for a branch nobody merges
and wrong for one that is going to land.

Lint aletheia/ with everything else, and run its own specs -- 55 of them, all
gdb-free -- with the suite: 215 examples becomes 270. Coverage stays a promise
about the gem, since most of the harness only runs under gdb and qemu against
real libcs, which CI has none of.

The gem package is unaffected: the gemspec globs lib/ and bin/ from the root, so
it picks up none of this.

* Reach the harness from the repository it verifies

Running Aletheia meant knowing where its binary lives and what flags it wants,
which is fine for whoever wrote it and a wall for everyone else. Give it a rake
task that takes the output level and what to run it against -- an architecture,
a path, a glob, or nothing for every libc the specs ship -- and reports what
came back per libc, with the offset and reason for anything that did not verify.

Verification is always strict there: whatever a gadget's constraints do not name
is poisoned, so an incomplete constraint list fails instead of passing by luck.
That is the only way to run it that answers the question worth asking.

* Say in the README that the gadgets are checked by running them

Constraints are only worth as much as they are complete, and nothing in the
README said how anyone knows they are. Point at Aletheia, say what it does to a
gadget -- arrange what the constraints ask for, poison everything they don't,
require a real shell to come back and list the root -- and show the two commands
that run it.

---------

Co-authored-by: Claude Opus 4.8 <[email protected]>
This commit is contained in:
david942j
2026-08-23 16:25:42 +08:00
committed by GitHub
co-authored by Claude Opus 4.8
parent 94d9178406
commit b45c1786ba
28 changed files with 4523 additions and 2 deletions
+1
View File
@@ -2,3 +2,4 @@
--order rand
--require spec_helper
--warning
--pattern {spec,aletheia/spec}/**/*_spec.rb
+17
View File
@@ -44,6 +44,23 @@ call, following conditional branches both ways. When a gadget is only reachable
The article introducing how I develop this tool can be found [on my blog](https://david942j.blogspot.com/2017/02/project-one-gadget-in-glibc.html).
### Checked by running them
Constraints are only worth as much as they are complete, so the gadgets this repository
ships are verified by being run. [Aletheia](aletheia/README.md) loads the libc in a live
process, arranges exactly what a gadget's constraints ask for, poisons every register and
page they *don't* mention, jumps to the offset, and requires a real `/bin/sh` to come back
and list the root directory. A gadget whose constraint list is missing something fails
there instead of passing by luck -- which is how several missing constraints were found.
```bash
bundle exec rake aletheia:verify # every libc under spec/data, level 0
bundle exec rake "aletheia:verify[1, aarch64]" # one output level, one architecture
```
Aletheia is development tooling: it lives outside `lib/` and `bin/`, so it is not part of
the published gem.
## Usage
### Command Line Interface
+17
View File
@@ -44,6 +44,23 @@ call, following conditional branches both ways. When a gadget is only reachable
The article introducing how I develop this tool can be found [on my blog](https://david942j.blogspot.com/2017/02/project-one-gadget-in-glibc.html).
### Checked by running them
Constraints are only worth as much as they are complete, so the gadgets this repository
ships are verified by being run. [Aletheia](aletheia/README.md) loads the libc in a live
process, arranges exactly what a gadget's constraints ask for, poisons every register and
page they *don't* mention, jumps to the offset, and requires a real `/bin/sh` to come back
and list the root directory. A gadget whose constraint list is missing something fails
there instead of passing by luck -- which is how several missing constraints were found.
```bash
bundle exec rake aletheia:verify # every libc under spec/data, level 0
bundle exec rake "aletheia:verify[1, aarch64]" # one output level, one architecture
```
Aletheia is development tooling: it lives outside `lib/` and `bin/`, so it is not part of
the published gem.
## Usage
### Command Line Interface
+7 -2
View File
@@ -5,6 +5,7 @@ require 'rspec/core/rake_task'
require 'rubocop/rake_task'
require 'yard'
import 'tasks/aletheia.rake'
import 'tasks/builds/generate.rake'
import 'tasks/builds/list.rake'
import 'tasks/readme.rake'
@@ -12,11 +13,15 @@ import 'tasks/readme.rake'
task default: %i[readme rubocop spec builds:list]
RuboCop::RakeTask.new(:rubocop) do |task|
task.patterns = ['lib/**/*.rb', 'spec/**/*.rb', 'bin/*', 'tasks/**/*.rake']
task.patterns = ['lib/**/*.rb', 'spec/**/*.rb', 'bin/*', 'tasks/**/*.rake', 'aletheia/**/*.rb', 'aletheia/bin/*']
task.options += ['--force-exclusion', 'lib/one_gadget/builds/*.rb']
end
RSpec::Core::RakeTask.new(:spec)
RSpec::Core::RakeTask.new(:spec) do |task|
# The harness's own unit specs run with the suite; +.rspec+ says the same for a
# bare +rspec+, which this task does not read.
task.pattern = '{spec,aletheia/spec}/**/*_spec.rb'
end
YARD::Rake::YardocTask.new(:doc) do |t|
t.files = Dir['lib/**/*.rb'] - Dir['lib/one_gadget/builds/*.rb']
+4
View File
@@ -0,0 +1,4 @@
/park_stub
*.log
/park_stub_*
/sysroots/
+74
View File
@@ -0,0 +1,74 @@
# Aletheia
Empirically verify that [one_gadget](https://github.com/david942j/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, and aarch64. 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. 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.
+63
View File
@@ -0,0 +1,63 @@
#!/usr/bin/env ruby
# frozen_string_literal: true
# Aletheia -- empirically verify that one_gadget gadgets launch a real shell.
# Usage:
# aletheia verify <libc.so> [--offset 0x4bc00[,0x4bc04...]] [--json]
require 'optparse'
HERE = File.expand_path('..', __dir__) # aletheia/
$LOAD_PATH.unshift(File.join(HERE, 'lib'))
$LOAD_PATH.unshift(File.expand_path('../lib', HERE)) # repo one_gadget lib
require 'aletheia/runner'
$stdout.sync = true # flush per line so a killed sweep keeps its partial output
options = { offsets: nil, json: false, strict: false, level: 0 }
parser = OptionParser.new do |o|
o.banner = 'Usage: aletheia verify <libc.so> [options]'
o.on('--offset LIST', 'Comma-separated gadget offsets to check (default: all)') do |v|
options[:offsets] = v.split(',').map { |s| Integer(s, s.start_with?('0x') ? 16 : 10) }
end
o.on('--strict', 'Poison uncontrolled registers (test constraint completeness)') do
options[:strict] = true
end
o.on('--level N', Integer, 'one_gadget level: 0 = top gadgets (default), 1 = all') do |v|
options[:level] = v
end
o.on('--json', 'Emit JSON-lines instead of a table') { options[:json] = true }
end
parser.parse!(ARGV)
command = ARGV.shift
abort parser.help unless command == 'verify'
target = ARGV.shift
abort "target libc required\n\n#{parser.help}" unless target && File.file?(target)
require 'json'
# Stream each result as it is produced, so a long sweep shows progress and a
# killed run keeps its partial output.
printer = lambda do |r|
if options[:json]
puts JSON.generate(r)
else
label = r[:result] == 'EXEC' && r[:promotable] ? 'EXEC*' : r[:result]
puts format('%-10s %-6s %s', r[:offset], label, r[:effect])
puts " reason: #{r[:reason]}" if r[:reason]
end
end
results = Aletheia::Runner.new(target: target, strict: options[:strict])
.run(offsets: options[:offsets], level: options[:level], &printer)
unless options[:json]
tally = results.group_by { |r| r[:result] }.transform_values(&:size)
puts "\n#{tally.map { |k, v| "#{k}=#{v}" }.join(' ')}"
end
# EXEC (reached execve("/bin/sh") but not L2-drivable) is a working gadget, not a
# failure; only a true FAIL (no shell at all) sets a nonzero exit.
exit(results.any? { |r| r[:result] == 'FAIL' } ? 1 : 0)
+33
View File
@@ -0,0 +1,33 @@
#!/bin/sh
# Build the park_stub helper for each architecture Aletheia can drive on this
# host. The native stub always builds; a cross stub builds only when its
# cross-compiler is installed. Binaries are host-specific build artifacts (see
# .gitignore), so run this once after checkout / after editing park_stub.c.
#
# ./build_stubs.sh
set -eu
cd "$(dirname "$0")"
build() {
cc="$1" out="$2"
if command -v "$cc" >/dev/null 2>&1; then
"$cc" -O0 -g -o "$out" park_stub.c -ldl
echo "built $out (via $cc)"
else
echo "skip $out ($cc not installed)"
fi
}
# Native host arch.
case "$(uname -m)" in
aarch64) build cc park_stub_aarch64 ;;
x86_64) build cc park_stub_x86_64 ;;
*) echo "unknown host arch $(uname -m); build a stub manually" >&2 ;;
esac
# Cross stubs for foreign targets driven under qemu-user.
[ "$(uname -m)" = aarch64 ] && build x86_64-linux-gnu-gcc park_stub_x86_64
[ "$(uname -m)" = x86_64 ] && build aarch64-linux-gnu-gcc park_stub_aarch64
build i686-linux-gnu-gcc park_stub_i386 # i386 (32-bit) is always cross-built
build arm-linux-gnueabihf-gcc park_stub_arm # armhf (32-bit) is always cross-built
exit 0
+107
View File
@@ -0,0 +1,107 @@
#!/bin/sh
# Build a per-version sysroot + park_stub for a foreign libc whose version differs
# too much from the host cross toolchain to dlopen directly (an older libc's init
# crashes under a newer ld.so; the stub also needs that libc's older symbols).
#
# Fetches the matching libc6 + libc6-dev .debs (the fixtures come from ubuntu),
# extracts them into sysroots/<arch>-<major.minor>/, and cross-builds park_stub
# against that libc so it only references its (older) symbol versions. The
# transport auto-uses sysroots/<arch>-<major.minor>/ when it exists (matched on
# the fixture's glibc version); otherwise the arch's default cross sysroot is used.
#
# ./build_sysroot.sh i386 2.27-3ubuntu1
set -eu
cd "$(dirname "$0")"
arch="${1:?usage: build_sysroot.sh <i386> <ubuntu-libc6-version>}"
ver="${2:?usage: build_sysroot.sh <i386> <ubuntu-libc6-version>}"
short=$(echo "$ver" | grep -oE '^[0-9]+\.[0-9]+')
case "$arch" in
i386) deb_arch=i386; triplet=i386-linux-gnu; cc=i686-linux-gnu-gcc; ldso=ld-linux.so.2 ;;
arm) deb_arch=armhf; triplet=arm-linux-gnueabihf; cc=arm-linux-gnueabihf-gcc; ldso=ld-linux-armhf.so.3 ;;
aarch64) deb_arch=arm64; triplet=aarch64-linux-gnu; cc=aarch64-linux-gnu-gcc; ldso=ld-linux-aarch64.so.1 ;;
amd64) deb_arch=amd64; triplet=x86_64-linux-gnu; cc=x86_64-linux-gnu-gcc; ldso=ld-linux-x86-64.so.2 ;;
*) echo "unsupported arch $arch" >&2; exit 2 ;;
esac
dl=-l:libdl.so.2
root="sysroots/$arch-$short"
rm -rf "$root"; mkdir -p "$root"
base='https://launchpad.net/ubuntu/+archive/primary/+files'
tmp=$(mktemp -d)
for pkg in libc6 libc6-dev; do
f="${pkg}_${ver}_${deb_arch}.deb"
echo "fetch $f"
curl -sfL --max-time 120 -o "$tmp/$f" "$base/$f"
dpkg-deb -x "$tmp/$f" "$root"
done
rm -rf "$tmp"
# Normalise split-usr vs merged-usr layouts so both /lib/$triplet and
# /usr/lib/$triplet resolve to the runtime libs no matter which the .deb used.
# A native arch's ld.so (running under qemu on a host of the same arch) may probe
# /usr/lib/$triplet before /lib/$triplet, while the target's baked interpreter
# path is /lib/$ldso -- both must land inside the sysroot or qemu falls back to
# the HOST's newer libc and the versions clash.
if [ -d "$root/lib/$triplet" ]; then
# Split-usr (older debs): libs in /lib; mirror them under /usr/lib.
mkdir -p "$root/usr/lib/$triplet"
for so in "$root/lib/$triplet"/*.so*; do
[ -e "$so" ] && ln -sf "../../../lib/$triplet/$(basename "$so")" \
"$root/usr/lib/$triplet/$(basename "$so")"
done
else
# Merged-usr (newer debs, e.g. glibc >= ~2.36): libs live only in /usr/lib;
# point /lib at it (as a real merged-usr root does) so /lib paths resolve too.
ln -sfn usr/lib "$root/lib"
fi
# qemu resolves the stub's interpreter (its own PT_INTERP path) against
# QEMU_LD_PREFIX=$root. The conventional path is /lib/$ldso, but amd64 .debs use
# /lib64/$ldso, and a fixture built by a nonstandard toolchain/prefix has been
# seen using /usr/lib/$ldso directly (no triplet dir) -- symlink all three; they're
# cheap, and only the one path a given target's PT_INTERP actually names matters.
mkdir -p "$root/usr/lib"
[ -e "$root/usr/lib/$ldso" ] || ln -sf "$triplet/$ldso" "$root/usr/lib/$ldso"
# /lib and /lib64 as alternate interpreter locations: skip /lib when it's
# already the merged-usr symlink to usr/lib (from the layout step above) --
# usr/lib/$ldso just above already covers /lib/$ldso transparently through it,
# and a *fresh* real symlink here, one level short, would point at the wrong
# place (relative to where it actually lands once the kernel follows /lib).
if [ ! -L "$root/lib" ]; then
mkdir -p "$root/lib"
[ -e "$root/lib/$ldso" ] || ln -sf "../usr/lib/$triplet/$ldso" "$root/lib/$ldso"
fi
mkdir -p "$root/lib64"
[ -e "$root/lib64/$ldso" ] || ln -sf "../usr/lib/$triplet/$ldso" "$root/lib64/$ldso"
libdir="$root/usr/lib/$triplet"
# -nostdinc: use ONLY the sysroot's headers (plus gcc's own builtins), so an old
# features.h isn't paired with the toolchain's newer sys/cdefs.h.
gcc_inc=$("$cc" -print-file-name=include)
"$cc" --sysroot="$root" -B"$libdir" -L"$libdir" -L"$root/lib/$triplet" \
-nostdinc -isystem "$gcc_inc" -isystem "$root/usr/include" \
-isystem "$root/usr/include/$triplet" \
-O0 -g park_stub.c -o "$root/park_stub" \
-Wl,-Bdynamic,-rpath-link,"$root/lib/$triplet" $dl
# A second, natively-invokable copy. The park_stub above keeps a generic
# interpreter path that qemu-user redirects into this sysroot via
# QEMU_LD_PREFIX; a real (non-qemu) execve has no such redirection, so on a
# host whose own arch matches this sysroot's, dlopen-ing the target libc
# through the HOST's ld.so hits glibc-private, version-sensitive symbols
# (_dl_exception_create and friends) -- the exact mismatch this sysroot exists
# to avoid. This copy instead embeds the sysroot's OWN ld.so as its
# interpreter and a matching runtime rpath, so the kernel loads it directly
# with no redirection needed (see Transport::Native).
abs_root=$(cd "$root" && pwd)
"$cc" --sysroot="$root" -B"$libdir" -L"$libdir" -L"$root/lib/$triplet" \
-nostdinc -isystem "$gcc_inc" -isystem "$root/usr/include" \
-isystem "$root/usr/include/$triplet" \
-O0 -g park_stub.c -o "$root/park_stub_native" \
-Wl,-Bdynamic,--dynamic-linker,"$abs_root/lib/$ldso" \
-Wl,-rpath,"$abs_root/lib/$triplet:$abs_root/usr/lib/$triplet" $dl
echo "built $root (glibc $short) + park_stub + park_stub_native"
+89
View File
@@ -0,0 +1,89 @@
# Constraint-discovery helper: run one gadget under poison and, on a fault,
# report the faulting instruction (relative to libc base) and the registers it
# touched -- the concrete lead for "which precondition did one_gadget omit?".
#
# Run under: gdb -nx -q -batch -x discover.py --args ./park_stub <target-libc.so>
# Params via env: ALETHEIA_PLAN (json), ALETHEIA_TARGET.
import gdb
import json
import os
import struct
plan = json.load(open(os.environ["ALETHEIA_PLAN"]))
offset = int(plan["offset"], 0)
gdb.execute("set pagination off")
gdb.execute("set confirm off")
gdb.execute("break pause")
gdb.execute("run")
pid = gdb.selected_inferior().pid
def base_of(basename):
lo = None
for line in open("/proc/%d/maps" % pid):
parts = line.split()
if len(parts) >= 6 and parts[5].split("/")[-1] == basename:
start = int(parts[0].split("-")[0], 16)
lo = start if lo is None else min(lo, start)
return lo
target_base = os.path.basename(os.environ.get("ALETHEIA_TARGET", ""))
base = base_of(target_base) or base_of("libc.so.6")
gadget = base + offset
scratch = int(gdb.parse_and_eval("(void*)mmap(0, 0x20000, 3, 0x22, -1, 0)")) & 0xFFFFFFFFFFFFFFFF # keep in sync with Satisfier::SCRATCH_SIZE
gdb.selected_inferior().write_memory(scratch + 0x200, b"ls /\x00")
# Fill uncontrolled registers the same way the driver does for this plan.
if plan.get("poison_default"):
fill = 0xDEAD0000
elif plan.get("benign_default"):
fill = scratch + 0x100
else:
fill = None
if fill is not None:
for i in range(31):
gdb.execute("set $x%d = %#x" % (i, fill))
for reg, val in plan.get("regs", {}).items():
if isinstance(val, dict) and "scratch_off" in val:
val = scratch + val["scratch_off"]
gdb.execute("set $%s = %#x" % (reg, int(val) & 0xFFFFFFFFFFFFFFFF))
# Scratch-relative memory writes (cf. driver.py) -- aarch64-only here, always 8 bytes.
for off, val in plan.get("mem", {}).items():
off = int(off)
if isinstance(val, dict) and "scratch_off" in val:
val = scratch + val["scratch_off"]
gdb.selected_inferior().write_memory(scratch + off, struct.pack("<Q", int(val) & 0xFFFFFFFFFFFFFFFF))
gdb.execute("set $sp = %#x" % (scratch + plan.get("sp_offset", 0x10000))) # keep in sync with Satisfier::SP_OFFSET
gdb.execute("set $pc = %#x" % gadget)
gdb.write("BASE=%#x GADGET=%#x SCRATCH=%#x\n" % (base, gadget, scratch))
gdb.execute("set follow-fork-mode child")
gdb.execute("catch syscall execve execveat")
gdb.execute("continue")
# On reaching execve, report its arguments before the image is replaced.
try:
nr = int(gdb.parse_and_eval("$x8"))
if nr in (221, 281):
path = gdb.execute("x/s $x0", to_string=True).strip()
gdb.write("EXECVE path=%s argv=%#x envp=%#x\n"
% (path, int(gdb.parse_and_eval("$x1")) & 0xFFFFFFFFFFFFFFFF,
int(gdb.parse_and_eval("$x2")) & 0xFFFFFFFFFFFFFFFF))
except gdb.error:
pass
# If we get here via a signal, report the fault site.
try:
pc = int(gdb.parse_and_eval("$pc")) & 0xFFFFFFFFFFFFFFFF
gdb.write("FAULT_PC=%#x (base+%#x)\n" % (pc, pc - base))
gdb.write("FAULT_INSN=%s\n" % gdb.execute("x/i $pc", to_string=True).strip())
gdb.write("--- context ---\n")
gdb.write(gdb.execute("x/3i $pc", to_string=True))
for i in range(31):
gdb.write("x%d=%s " % (i, gdb.execute("p/x $x%d" % i, to_string=True).split('=')[1].strip()))
gdb.write("\n")
except gdb.error as e:
gdb.write("no-fault-context (%s)\n" % e)
+95
View File
@@ -0,0 +1,95 @@
# Adding an architecture backend
Aletheia is arch-parameterized. aarch64 is the reference backend and amd64 is fully wired
(driven under qemu-user on an aarch64 host). Adding another arch (i386, arm) is a new backend
object plus a cross-built stub — the satisfier, oracle, transport, and reporting are reused
unchanged.
## How the pieces fit
- **`lib/aletheia/arch/<name>.rb`** — the only arch-specific code: register model, ABI, and the
`driver_model` hash serialized into the plan.
- **Transport** (`lib/aletheia/transport.rb`) is chosen automatically from the backend's `qemu`:
`nil` -> run natively under `gdb`; a config hash -> run under `qemu-<arch> -g <port>` with a
gdbstub and attach `gdb-multiarch`. No CLI flag — `Runner` maps the target ELF's machine to a
backend via `ARCHES` and the backend decides the transport.
- **`driver.py`** is arch-neutral: it reads register names, `sp`/`pc`, and syscall numbers from
the plan's `arch` block (`driver_model`), so the same driver serves every arch.
- **`park_stub`** is self-describing (pre-allocates scratch, prints its own libc base), so the
driver needs no inferior `mmap` and no `/proc` access from a possibly-remote debugger — this is
what makes the qemu-user path work.
## Backend object
Add `lib/aletheia/arch/<name>.rb` mirroring `arch/amd64.rb`, describing:
- `gprs` — assignable registers.
- `stack_regs` — registers naming a live stack address (an equality-to-NULL on `sp+imm` is
unsatisfiable). Only the true stack pointer; a frame pointer the gadget lets the attacker
control is a normal GPR.
- `sp` / `pc`.
- `native_on?(machine)` — whether the target runs natively on this host's `uname -m`.
- `normalize_reg(reg)` — fold a sub-register view onto its full register (aarch64 `w0 -> x0`,
amd64 `eax -> rax`, `r8d -> r8`); setting the full register sets the low bits.
- `stub_binary` — the `park_stub_<arch>` this backend runs.
- `qemu` — `nil` for a native arch, else `{ 'bin', 'ld_prefix', 'gdb_arch' }` (the emulator,
the sysroot providing the stub's own ld.so + libc, and the gdb architecture to select).
- `driver_model` — GPR list, `sp`, `pc`, `gdb_arch`, `sysno_reg`, `execve_syscalls`, and the
execve arg registers (`path_reg`, `argv_reg`, `envp_reg`).
Register it in `Runner::ARCHES` keyed by `OneGadget::Helper.architecture`'s symbol.
## Stub
Cross-build the stub once (or after editing `park_stub.c`):
```
./build_stubs.sh # native stub + any cross stub whose toolchain is installed
```
A foreign arch needs its cross-compiler (`gcc-<arch>-linux-gnu`) and, at run time, `qemu-user`
plus `gdb-multiarch`. `QEMU_LD_PREFIX` (the backend's `ld_prefix`) must point at a sysroot whose
`ld.so`/`libc.so.6` matches the stub's own arch — the cross toolchain's sysroot works because the
stub `dlopen`s the *target* fixture separately.
## Older foreign libcs (per-version sysroots)
The default cross sysroot only loads fixtures close to its own glibc version. An *older* libc
fails two ways: its init crashes under the newer `ld.so`, and the modern-toolchain stub needs
symbol versions the old libc lacks (e.g. i386 `dlopen@GLIBC_2.34`). Build a matching sysroot:
```
./build_sysroot.sh i386 2.27-3ubuntu1 # fetch that libc6 + libc6-dev, cross-build a stub
```
It fetches the fixture's `libc6`/`libc6-dev` `.deb`s (the fixtures come from ubuntu; the version
is in the fixture's `GNU C Library (Ubuntu GLIBC …)` string), extracts `sysroots/<arch>-<ver>/`
with the matching `ld.so`, and links `park_stub` against that libc.
The transport uses `sysroots/<arch>-<major.minor>/` for a fixture of that glibc version, and
**builds it on demand** when missing — but only for an arch that needs it (`version_strict?`, i.e.
i386, not amd64) and a Ubuntu-sourced fixture. So `sysroots/` (git-ignored) can be deleted anytime
to reclaim disk; the next verify rebuilds what it needs. `ALETHEIA_LD_PREFIX` / `ALETHEIA_STUB`
override manually. (Debian-sourced older fixtures would need their `.deb`s fetched differently —
not handled yet; the default cross sysroot covers the toolchain-matched version.)
## posix_spawn note
`do_system` gadgets fork a child that execs the shell. Natively, gdb follows the child and drives
it. Over a qemu-user gdbstub a single stub can't debug both fork sides, so the driver stays with
the parent and lets the child run free on the guest tty — the L2 `ls /` check on the pty is the
arbiter either way. The driver picks the mode from the transport (`connect == "run"`).
## Fixtures and expectations
amd64/i386 fixtures already live in `spec/data/libc-*.so`. Verify against those and record results
in `docs/FINDINGS.md`.
## Checklist
- [ ] `arch/<name>.rb` with the register/ABI model and `driver_model`.
- [ ] `qemu` config (or `nil`) and a cross-built `park_stub_<name>`.
- [ ] registered in `Runner::ARCHES`.
- [ ] a passing run on one straight-line execve gadget, then the full set.
- [ ] a negative control (a valid plan redirected to a non-shell offset) that FAILs.
- [ ] findings recorded.
+220
View File
@@ -0,0 +1,220 @@
# Aletheia design
For a future maintainer (human or agent) picking this up cold. Read this, then
`FINDINGS.md`, then the source under `lib/aletheia/`.
## What is being verified
one_gadget derives each gadget's `offset`, `effect`, and `constraints` by *static*
emulation. Aletheia checks the claim empirically: if you jump to `base+offset` with state
that satisfies the constraints, does a working shell actually start?
## The pipeline
```
bin/aletheia
-> Runner (lib/aletheia/runner.rb)
enumerate gadgets: OneGadget.gadgets(file:, force_file:true, details:true)
for each gadget:
Satisfier (lib/aletheia/satisfier.rb) constraints -> injection Plan (JSON-able)
Oracle (lib/aletheia/oracle.rb) run the plan, decide PASS/FAIL
|
v
gdb -nx -batch -x driver.py --args park_stub <libc.so> (on a pty)
driver.py (gdb-Python):
break at pause (libc fully initialized), read load base from /proc/pid/maps
mmap zeroed scratch; fill uncontrolled regs (benign or poison); apply plan regs;
set sp into scratch; set pc = base+offset; follow-fork child; continue
Oracle drives the pty: writes `ls /` + `exit`, validates output vs Dir.children('/')
```
`park_stub.c` `dlopen`s the target libc and parks in `for(;;) pause();`. Parking after
init means relocations/TLS are done and `environ` is populated, and we hijack a thread
whose state is disposable — we overwrite pc/sp/regs and point sp at fresh scratch, so we
never corrupt the loader.
## Transports (how the process is run and injected)
`Transport.for` picks one from the *host* arch (`uname -m` vs each backend's `native_on?`),
not a per-arch flag, so a backend runs natively on its own host and under qemu-user on any
other. All share the self-describing `park_stub` (it reports its own load base + scratch, so
the debugger needs no inferior calls or `/proc` access):
- **Native** — the arch is the host's: one `gdb` runs the stub directly.
- **Qemu** — a foreign arch: `qemu-user -g` exposes a gdbstub, `gdb-multiarch` attaches and
injects. This is where L0's `catch exec` and the fork-following live. `QEMU_LD_PREFIX` is
the arch's cross sysroot (`/usr/<triplet>`) — or the host root `/` when a *native* arch is
forced under qemu (see below).
- **SelfInject** — no gdb at all: the stub reads the plan from `$ALETHEIA_SELFINJECT` and
applies it itself (a small asm trampoline loads the registers/sp and branches to the
gadget), so the whole run stays under plain `qemu-user`. Used by arm because qemu-arm's
gdbstub kills the fork'd child of a `posix_spawn` gadget, so the L2 shell never survives
the gdb path. Trade-off: no gdb means no L0 signal, so a SelfInject gadget is judged on
L2 alone (PASS) or its absence. qemu runs with `-strace` so the oracle can see an
unimplemented-syscall abort and report SKIP rather than FAIL.
Set `ALETHEIA_FORCE_QEMU=1` to route a *native* arch through the Qemu transport too — e.g. to
exercise the aarch64 qemu path on an aarch64 host. Both agree gadget-for-gadget (the aarch64
2.43 set is 8/8 PASS native and forced-qemu).
## The oracle: layered L0 + L2
`driver.py` runs the injected gadget and reports two signals:
- **L0** (deterministic): the gadget reaches `execve("/bin/sh")` with a readable argv/envp.
A straight-line `execve`/`execl` stops at the syscall entry, where the `"/bin/sh"` path
and pointers are checked directly. A `posix_spawn` execs in a vforked child that runs
straight through to the new image, so there L0 instead confirms `/proc/pid/exe` is a shell.
- **L2** (the golden signal): the spawned shell actually ran `ls /` over a pty and the output
matches the live `Dir.children('/')`.
Outcomes: **PASS** = L2; **EXEC** = L0 without L2 (the gadget works, but the harness can't
drive `ls /` through that shell — a fixed `-c` command from a libc global, an uncontrolled
`argv[1]` that `sh` treats as a script name, or a `posix_spawn` parent/child tty race);
**FAIL** = neither (a candidate one_gadget bug, especially under `--strict`); **SKIP** = the
satisfier produced no plan, or the emulator couldn't run the gadget (e.g. qemu-user hit a
syscall it doesn't implement — see the clone3 limitation below). EXEC exists because "reaches a
shell" and "we can drive that shell" are different questions — conflating them would mislabel
working gadgets as failures.
**Promotion (EXEC\*)**: an EXEC gadget is retried with the uncontrolled registers nulled
(`null_default`). Many EXEC results are only inconclusive because the code writes an
uncontrolled register as `argv[1]`, and the benign fill makes it a garbage-but-readable string
that `sh` treats as a script name and exits. Nulling that register terminates argv, so the
shell is interactive and runs `ls /`. If the null-fill retry PASSes, the gadget is reported
EXEC\* — genuinely usable given that (attacker-controlled) input. If it still can't drive (a
fixed `-c` command from a libc constant), it stays EXEC.
## Independence principle (important)
The tool under verification must not be its own judge. So:
- **The verdict is empirical only**: PASS iff a real shell ran `ls /` and returned the real
root. No part of the decision consults one_gadget's belief about its constraints.
- The operand parser (`lib/aletheia/operand.rb`) is written from scratch, not reused from
the emulator's `Lambda.parse`, so an emulator parsing bug can't mask itself in the checker.
- Bugs are expected to live in the constraint list — most often a *missing* constraint.
## The satisfier
`Satisfier#satisfy` is the inverse of one_gadget's `gadget.rb#calculate_score`: same
category dispatch, but it emits assignments instead of scores. For each constraint it
splits on ` || `, scores each disjunct's cost (nil = unsatisfiable / unsupported), and
takes the cheapest satisfiable branch. Memory model: one zeroed scratch region, `sp` set
to `scratch + sp_offset`, so sp-relative NULL/writable requirements are free.
Categories handled today: `writable: <reg+imm>` (point the register into a scratch
write-area), `<op> == NULL` / `<op> <= 0x0` (bare reg -> 0; sp+imm -> unsatisfiable, so the
other branch wins; a *single* sp-relative deref -> free via zero-fill). `is a valid
argv/envp` (the full array-literal/content builder) is scored expensive and not built --
every fixture so far always has a cheaper branch available.
**Chained dereferences** (`[[X]] == NULL`, or deeper -- posix_spawn's argv/envp when
passed as a pointer-to-pointer, e.g. `argv=[sp]` with `[[sp]] == NULL` meaning "argv[0] is
NULL") are NOT automatically free like a single deref: `[X]` (the first level) is
zero-filled, so dereferencing it *again* reads through NULL and faults. `apply_deep_null`
builds a real pointer chain instead -- one `plan.mem` scratch write per extra level of
indirection, terminating in the always-zero `STRING_POOL` -- so every level is a genuine,
valid pointer. Costed above a single deref (it needs a scratch write the free case
doesn't), so it's only chosen when no cheaper branch exists. `plan.mem` is applied by
`driver.py` (a `write_memory` call per entry, arch-width via `word_size`) and by
`park_stub.c`'s self-injection (a `mem <off> <val>` directive, arm-only, 4-byte writes) --
see `Transport::SelfInject#plan_text` and `self_inject()`'s grammar comment in park_stub.c.
## Benign vs poison (the completeness test)
`driver.py` fills registers the plan doesn't set. **Benign** points them at readable
scratch (reproduces a gadget under favorable state). **Poison** (`--strict`) sets them to
an unmapped address so any *unlisted* dereference faults — this is what turns "the gadget
works if you're lucky" into "the constraint list is complete". A poison fault with a fully
satisfied plan is a candidate missing-constraint bug.
## Constraint-discovery loop
When a satisfied plan FAILs (esp. under poison), find the real precondition:
1. `discover.py` runs the plan under poison and, on the fault, prints the faulting
instruction relative to base and all GPRs. That is the concrete lead.
2. Set the implicated register to a plausible value, re-run; iterate until `ls /` works.
The delta between the failing and passing plan *is* the missing constraint.
3. Root-cause in one_gadget (emulator/fetcher) and record in `FINDINGS.md`.
`docs/FINDINGS.md`'s Finding 1 is a worked example (missing `sigprocmask` `set`-pointer
constraint, traced to `emulators/arm_family.rb`'s `inst_bl` checker).
## Result discriminator
A FAIL is a one_gadget bug only if the plan was **complete, conflict-free, and fully
satisfied**. A SKIP / conflict / unsatisfiable-branch / environment error (e.g. a libc
that won't `dlopen`) is a harness limitation, not a verdict on the gadget.
## Harness reliability fixes
Bugs in Aletheia itself, not in one_gadget -- found the same way as a real finding (a
result that looked wrong until traced to ground), but the defect was in the harness's own
model. Recorded because `--strict` is only a trustworthy verdict on one_gadget once the
harness underneath it is trusted; a harness bug here would otherwise get misread as a
one_gadget bug there.
- **`catch exec` corrupted qemu-aarch64 execution.** Landing mid-function via the gdbstub
with an exec catchpoint armed made some straight-line `execve`/`execl` gadgets SIGSEGV
inside libc under the qemu transport (reproduced: clean without the catchpoint, corrupts
with it). It was only ever useful natively anyway (it exists to catch a vforked
`posix_spawn` child's exec, and the qemu transport deliberately never follows the
child -- `follow-fork-mode parent` -- so the catchpoint could never usefully fire there).
Fixed: only armed when `connect == "run"` (native).
- **Scratch headroom below `sp` was too tight.** `SP_OFFSET` (0x2000) left only 8KB below
`sp` before the scratch mmap's start. A gadget landing inside a function whose *own*
prologue allocates a large frame after the jump (aarch64 `execl`'s
`sub sp,sp,#0x2000; sub sp,sp,#0xd0`, ~8.4KB) could write past that boundary. Silently
absorbed by an adjacent mapping under native ASLR (so it never showed up natively), but
qemu-user's stricter layout faulted reliably -- and inconsistently across runs, since it
hinged on ASLR luck either way. Fixed: `SCRATCH_SIZE`/`SP_OFFSET`/`WRITABLE_BASE` widened
(128KB scratch, 64KB headroom below `sp`); `park_stub.c` and `discover.py`'s standalone
mmap kept in sync (see the "keep in sync" comments at each).
- **Per-version sysroot stubs went stale silently.** A per-version sysroot's `park_stub` is
a cross-compile of `park_stub.c` cached under `sysroots/<arch>-<version>/`. `stub_built?`
only checked existence, not currency -- so editing `park_stub.c` (e.g. the `SCRATCH_SIZE`
fix above) left every already-built sysroot stub running the *old* layout while the
satisfier computed offsets against the *new* one, a silent mismatch that manifested as
seemingly random SIGSEGVs on exactly the arches/versions with a cached sysroot. Fixed:
`stub_built?` also compares mtimes and rebuilds when `park_stub.c` is newer.
Net effect of the three together (they compounded, which is why this took real digging to
untangle): an aarch64-2.23 `execl` gadget was flaky under qemu — passed once, then failed
consistently — purely from ASLR luck on the headroom bug, misleadingly close to "looks like
qemu itself is unreliable." It was two harness bugs plus a stale-cache issue, not qemu, not
one_gadget. All three are now covered by rerunning every fixture (native + `ALETHEIA_FORCE_QEMU=1`)
after any `park_stub.c`/`satisfier.rb` change -- see the per-arch counts these fixes were
verified against in the commit that introduced this section.
## Known limitations
- **qemu-arm can't verify `posix_spawn` gadgets.** glibc 2.43's `posix_spawn` forks with
the `clone3` syscall (arm EABI 435), which qemu-arm 10.2 doesn't implement — it returns
ENOSYS, no child spawns, and `do_system` aborts on `wait4 == ECHILD`. So arm `posix_spawn`
gadgets are reported SKIP (the SelfInject `-strace` detects the unknown syscall); arm
`execve` gadgets (a plain syscall) verify fine. qemu-x86_64 does implement `clone3`, which
is why amd64/i386 `posix_spawn` gadgets PASS. This clears the moment qemu-arm gains 32-bit
`clone3` support (or on real arm hardware) — no Aletheia change needed.
- Older libcs may not `dlopen` standalone under the host loader (e.g. `aarch64-libc-2.27.so`
aborts with SIGILL on glibc 2.43). Run them under qemu with `ALETHEIA_FORCE_QEMU=1`: a
per-version sysroot (matching ld.so, cross-built stub) is fetched on demand, so 2.27 now
verifies. A non-Ubuntu fixture (no fetchable deb, e.g. the 2.24) instead falls back to the
host loader, which works only when it can load that libc.
- **An address written as `(reg + $base+imm)`** -- arm code that offsets a PC-relative
address by a caller-controlled register (`add r1, pc`). Where the sum lands is the
register's to decide, so each register used that way is pinned once, up front, to put
its sums in libc's own spare writable data: the tail of the last page of its writable
segment (`Runner#spare_writable`), which is mapped, zeroed and used by nothing. Every
operand built on it then reads as the plain `$base+off` it has become, which the rest
of the satisfier already resolves -- so a store, a read, a chained read and a readable
target all work without a case of their own (`Satisfier#steer_base_sums`).
The sum required to be **NULL** instead -- written `(reg + $base+imm) == NULL`, or
implied by an argv *terminator* -- cannot be steered anywhere: only `-(base + imm)`
makes a libc address vanish, and that value is not known until the library is loaded.
The plan names it (`{'neg_base_off' => imm}`) and the driver and stub resolve it, the
way they already do a scratch or load-base offset. It is ranked below the array
builder, so emptying an argv stays a last resort rather than a cost preference.
- `x29`/frame-chain assumptions: poison leaves x29 poisoned; if a gadget needs a valid
frame this shows up as a fault — treat with the discovery loop before calling it a bug.
+48
View File
@@ -0,0 +1,48 @@
# EXEC backlog (closed)
`EXEC` means the gadget **reached `execve`/`posix_spawn`** but the level-2 oracle
never got a shell to run `ls /`. Unlike `SKIP` (no plan could be built) an EXEC
run proves the gadget works up to the exec; what's missing is a shell we can
drive. These were worked through one category at a time, the way the SKIP
categories were.
The backlog is empty. The strict level-2 sweep over all 21 fixtures is
**1163 PASS / 0 EXEC / 0 FAIL / 0 SKIP**: every gadget one_gadget reports, on
every architecture, drives a real interactive shell under poisoned registers.
## What emptied it
Three causes, in the order they were found. The first two were the harness
observing badly; the third was a real one_gadget imprecision.
**Empty argv from the cheap NULL branch.** A constraint like
`[rsp+0x50] == NULL || {[rsp+0x50], ...} is a valid argv` has two satisfiable
disjuncts, and the satisfier took the cheaper one -- yielding a shell with no
`argv[0]`, which execs fine but gives the pty nothing to drive. Fixed by
preferring the array branch when the operand being constrained is the exec's
own argv, and by teaching the satisfier the five argv shapes a shell actually
accepts.
**The harness closing the shell's own stdin.** 122 of the remaining 142. A
gadget calling `close(<unconstrained descriptor>)` had that descriptor read as
0, so the spawned shell lost the pty it was supposed to be driven through. The
descriptor is the caller's to choose, so one_gadget now says so (a `caveats`
line) and the harness plans a spare one. A word-vs-dword plan write, which
zeroed an adjacent field, hid 20 more behind the same symptom.
**argv built through a pointer no register names.** The last 4. A candidate that
rounds a pointer down (`and rsi, ~0xf`) or loads one from its frame
(`mov rax, [rbp-0x48]`) and then writes argv in place had those stores go
untracked, because the emulator keyed write history to register names only. The
argv fell back to the opaque `[ptr] == NULL || ... is a valid argv`, whose first
disjunct the gadget's own store to `argv[0]` overwrites, while the real
requirement -- `argv[1]`, an incoming register -- went unstated. Fixed by giving
a derived pointer a write history of its own; see
`Processor#value_based_stack` / `#resolve_address`.
## Method
Same loop as the SKIP work: categorise by the *first* thing that blocks
observation, fix the largest category, re-sweep, re-categorise. A category
splits once its top blocker is removed -- each of the three above was invisible
until the one before it was gone.
+398
View File
@@ -0,0 +1,398 @@
# Aletheia findings
Verification runs of one_gadget's aarch64 output against real, natively-executed
libc. Two run modes:
- **default (benign)** — registers the constraints don't govern point at readable
zeroed scratch. Reproduces a gadget under favorable state.
- **`--strict` (poison)** — those registers are set to an unmapped address, so any
*unlisted* dependency faults. This is the completeness test for the constraint list.
## Summary
| fixture | gadgets | benign | strict (poison) |
| --- | --- | --- | --- |
| aarch64-libc-2.43.so | 8 (posix_spawn) | 8 PASS | 8 PASS |
| aarch64-libc-2.24.so | 3 (execve) | 3 PASS | 1 PASS, 2 FAIL |
| aarch64-libc-2.23.so | 3 (execve) | 3 PASS | 1 PASS, 2 FAIL |
Every gadget launches a real, working `/bin/sh` under benign state (validated by the
shell running `ls /` and reproducing the host root). The 2.43 set is also complete
under poison. The strict failures were candidate one_gadget bugs (Findings 1 and 2), both fixed in
PR #323. With the fix, strict is **all PASS** across the
2.43/2.24/2.23 fixtures (one_gadget reports the reliable entry points, and the constraint
lists are complete).
## Level-1 sweep (every gadget)
With `--level 1`, one_gadget emits every gadget it finds (not just the top-scoring few). After
the PR #323 fixes, the full aarch64 sweep is:
| fixture | level-1 gadgets | PASS | EXEC* (promotable) | EXEC (hard) | FAIL |
| --- | --- | --- | --- | --- | --- |
| aarch64-libc-2.43.so | 28 | 27 | 1 | 0 | 0 |
| aarch64-libc-2.24.so | 8 | 8 | 0 | 0 | 0 |
| aarch64-libc-2.23.so | 11 | 9 | 2 | 0 | 0 |
**All 47 gadgets are verified usable — 44 PASS, 3 EXEC\*, zero unpromotable EXEC, zero FAIL.**
Every gadget reaches `execve("/bin/sh")` with a valid argv/envp; 44 are driven to run `ls /`
directly, and the other 3 are **promotable** (EXEC*).
Two argv shapes needed care to drive:
- **`sh -c <cmd>` (do_system / posix_spawn).** The command operand is a controllable register,
so the harness points it at an `"ls /"` string. When the argv is `{"sh", "-c", $base+..., x21}`
and that libc constant is `"--"`, the `--` merely ends `sh`'s option parsing, so the *next*
operand (`x21`, controllable) becomes the command — point `x21` at `"ls /"` and `sh -c -- "ls /"`
runs it. These now PASS directly.
- **`execve("/bin/sh", <reg>, ...)` (execvpe / 2.43 conditional).** The code writes an
uncontrolled register as `argv[1]`, which the benign fill sets to a garbage-but-readable
string `sh` treats as a script name. Nulling that register (which an attacker controls)
terminates argv, so the shell is interactive and runs `ls /`. The harness proves this by
retrying with uncontrolled registers nulled (reported EXEC*). The satisfier can't set that
register itself because it isn't named in the constraints (it's argv content the code writes),
so these stay EXEC* rather than PASS.
Strong empirical evidence that one_gadget's aarch64 level-1 output is sound: every gadget
reaches a real `/bin/sh` and yields a shell that actually runs commands.
## Finding 1 — missing constraint: sigprocmask `set` pointer must be readable
**Status: fixed** in PR #323 (emits `<set> == NULL` when
`set` isn't provably mapped). Under strict mode this fully fixes `0x3c92c`/`0x3d6d4`
(they now PASS). `0x3c934`/`0x3d6dc` gain the correct `x21 == NULL` too, but still FAIL
strict for a second, independent reason — see Finding 2.
The same defect existed on **all four architectures** (the `sigprocmask => {}` safe-call
entry is shared logic), so the fix is cross-arch: a shared `Processor#dispatch_safe_call`
marks `sigprocmask`'s `set` argument `:readable` and emits `<set> == NULL` when it isn't
provably mapped, applied via `arm_family.rb` (ARM/AArch64) and `x86.rb` (amd64/i386). On
amd64 the `set` register is `rbp`; on i386 it is a bare register too. The change is purely
additive at `level: 1` (no gadgets gained or lost across any fixture); at the default
`level: 0` it re-ranks — the harder entries (now carrying `set == NULL`) correctly fall
below the cleaner entry of the same `do_system`, which the default still shows.
**Gadgets:** `0x3c92c`, `0x3c934` (libc-2.24); `0x3d6d4`, `0x3d6dc` (libc-2.23).
Constraint form: `execve("/bin/sh", sp+0x58, environ)` with only
`writable: x19+…`, `writable: x20+0x4`, `x4 == NULL || {…}`.
**Symptom (strict mode):** SIGSEGV at `sigprocmask+28` (`ldr x19, [x1]`), before ever
reaching `execve`, with the fully-satisfied plan.
**Root cause (verified):** on the path from the gadget the code does
`mov x1, x21; bl sigprocmask` (`0x3c95c`/`0x3d704`). `x21` is never written on the
gadget path, so it is a precondition: it is `sigprocmask`'s `set` argument, which the
function dereferences unconditionally (`ldr x19, [x1]`, then `tst`). one_gadget lists
**no constraint on x21**. Setting `x21` to a readable pointer makes the gadget PASS
under poison — proving the omission (and only that) is the defect.
**Why one_gadget misses it:** the emulator's call handler treats `sigprocmask` as an
unconditionally-safe pass-through. In `lib/one_gadget/emulators/arm_family.rb`
(`inst_bl`), the checker is:
```ruby
checker = { 'sigprocmask' => {}, '__sigaction' => { 2 => :zero? } }
```
The empty hash for `sigprocmask` asserts no requirement on its arguments, but the real
function dereferences `set` (arg index 1). The correct model would require that arg to
be a readable pointer (emit e.g. `x21 is a readable pointer`, or a constraint that the
`set` argument is valid), analogous to how `__sigaction`'s arg 2 is required to be zero.
**Discriminator:** this is a genuine one_gadget imprecision, not a harness limitation —
the plan was complete and conflict-free, satisfied every listed constraint, and failed
only because of an input the constraint list does not mention. Impact: these gadgets are
less reliable than advertised; a return-to-one-gadget attempt with an arbitrary `x21`
crashes in `sigprocmask` instead of spawning a shell.
**Not affected:** `0x3c970`/`0x3d718` (`execve("/bin/sh", x22, environ)`) jump in *after*
the `sigprocmask` call, so they carry no such dependency and PASS under poison.
### Fix applied (PR #323)
`sigprocmask`'s `set` argument is modelled in `arm_family.rb`'s `inst_bl` checker, emitting
`<set> == NULL` when it isn't provably mapped, instead of treating the call as
argument-agnostic. Regression expectations added to `spec/one_gadget_aarch64_spec.rb`.
## Finding 2 — missing constraint: __sigaction `act` pointer (subtler)
**Gadgets:** `0x3c934` (libc-2.24), `0x3d6dc` (libc-2.23). **Status: fixed** in PR #323
(folded in with Finding 1's fix).
**Symptom (strict mode, with Finding 1 fixed):** SIGSEGV at `__libc_sigaction+36`
(`ldr x3, [x1], #8`), before `execve`.
**Root cause:** these entry points sit one instruction after the `add x1, x20, #8` that
sets up `__sigaction`'s `act` argument, so on this path `act` (x1) is an uncontrolled
incoming register that `__sigaction` dereferences. one_gadget requires `__sigaction`'s
`oldact` (arg 2) to be NULL but places no requirement on `act` (arg 1).
**Why it's subtler than Finding 1:** the sibling `0x3c92c` reaches `__sigaction` with
`act = x20+8`, and `x20` is already `writable`-constrained — so there `act` is valid and
must NOT be constrained to NULL. But the emulator processes the `__sigaction` call *before*
the later store that records `writable: x20`, so a naive "emit `act == NULL` when the base
isn't known-mapped" check would over-constrain `0x3c92c` (a false, over-tight constraint —
the opposite bug). A correct fix needs to consider constraints discovered later in the same
candidate (e.g. defer the pointer-safety check to post-emulation, cross-referencing the
final `writable` set), so it is left for a separate change.
**Resolution:** the `:readable` safe-call check was made *deferred* — resolved in
`Processor#finalize_deferred_reads` after emulation, when the full `writable:` set is known.
So `act = x20+8` (with `x20` writable) is recognised as mapped and left unconstrained, while
`act = x1` (bare, uncontrolled) gets `x1 == NULL`. That gives `0x3c934` its true, harder
constraint set, and `trim_gadgets` then drops it in favour of the dominating, reliable
`0x3c930` (`act` set up via `x20+8`). Aletheia `--strict` on libc-2.24 is now **3/3 PASS** —
the emitted set is complete. Same shape on libc-2.23 (`0x3d6dc` → `0x3d6d8`).
## Finding 3 — missing constraint: arm GOT-base register (environ gadgets)
**Gadgets:** `0x3afdc`, `0x543d2` (arm libc-2.43-8c7af7f2). **Status: fixed**, one_gadget#331.
**Constraint form:** `posix_spawn(..., environ)` — the envp argument is the libc global
`environ`. Listed constraints govern only the argv/attrp (e.g. `{"sh","-c","--",r9,...}
is a valid argv`, `r7 == NULL || (u16)[r7] == NULL`). **No constraint names the GOT base.**
**Symptom:** SIGSEGV at NULL before ever reaching `posix_spawn`, with the fully-satisfied
plan. Disasm at `0x3afdc`: `ldr r1, [pc, #416]` (GOT offset of `environ`), `ldr r1, [r6, r1]`
(GOT-base + offset), `ldr r3, [r1, #0]` — the last deref faults because `r6` isn't the GOT.
**Root cause (verified):** in ARM PIC, `environ` is reached through a GOT-base register that
glibc loads in the function prologue (`ldr rX, [pc]; add rX, pc`) — *outside* the gadget
window. The register is a precondition: it must hold `$base + got` (the libc `.got` base).
Setting it makes the gadget PASS (a real shell runs `ls /`):
| gadget | GOT-base reg | with `reg = $base + 0x12fe38` |
| --- | --- | --- |
| `0x3afdc` | `r6` (`ldr r1, [r6, r1]`) | PASS |
| `0x543d2` | `r7` (`ldr r2, [r7, r2]`) | PASS |
The register differs per gadget, so the constraint must name the right one.
**Why one_gadget misses it:** the arm fetcher already *detects* these registers and replays
their prologue setup so the emulator can resolve `environ` — `Fetchers::Arm#seed_got_registers`
seeds each GOT-base register with `$base + got` before emulating the candidate. But that
seeded assumption is never surfaced as a constraint. Contrast i386, whose fetcher derives the
GOT-base register from the (GOT-relative) `/bin/sh` pointer and emits
`"#{@base_reg} is the GOT address of libc"` (`Fetchers::I386#resolve`). arm should do the
same for the register(s) whose seeded GOT value flows into a resolved global.
**Discriminator:** a genuine imprecision, not a harness limitation — the plan satisfied every
listed constraint and failed only on an input the list omits. Impact: a return-to-one-gadget
attempt with an uncontrolled GOT-base register crashes before `posix_spawn` instead of
spawning a shell.
### Fix applied (one_gadget#331)
`Fetchers::Arm` now records which seeded GOT-base register(s) were actually dereferenced to
resolve a global that appears in the final effect/constraints, and emits
`"<reg> is the GOT address of libc"` for each (mirroring i386, reusing the existing
`Satisfier` support for that constraint). Verified: both gadgets PASS with the fix applied
(Aletheia re-run after the code change). Locked in by `arm-libc-2.43-8c7af7f2` in
`spec/one_gadget_arm_spec.rb` (one_gadget#332).
**Not the GOT issue:** the other level-1 posix_spawn FAILs on this fixture (`0x3b000`,
`0x3b002`, `0x3b004`, `0xa42c8`, `0xa4334`, `0xa4338`) did not reference `environ`; they
were a **harness limitation, not a one_gadget bug** -- the satisfier couldn't build a
chained dereference (`argv=[sp]` needs `[[sp]] == NULL`, i.e. argv[0]=NULL, which requires
a real pointer at `[sp]`, not the zero-fill a *single* deref gets for free). Fixed by
`Satisfier#apply_deep_null` (see DESIGN.md's satisfier section); all 10 of this fixture's
level-1 gadgets now PASS, including these six.
## Finding 4 — imprecise constraint: frame-built argv hides an `argv[1]` requirement
**Gadgets:** `0xa3234`, `0xa3238`, `0xa3240`, `0xa32e8` (aarch64 libc-2.27, in `execvpe`).
**Status: fixed**, one_gadget#333. Surfaced once 2.27 became loadable under qemu
(`ALETHEIA_FORCE_QEMU=1`, see Known limitations).
**Constraint form:** `execve("/bin/sh", x29+0x40, <envp>)` with argv reported only as
`[x29+0x40] == NULL || x29+0x40 == NULL || x29+0x40 is a valid argv`. **No constraint on the
value that becomes `argv[1]`.**
**Symptom:** the gadget reaches `execve("/bin/sh", ...)` (so L0 passes, reported EXEC) but the
shell isn't drivable and isn't promotable. At the `execve`, the argv array is actually
`{"/bin/sh", "", NULL}` — a *non-NULL empty* `argv[1]` — so `sh` treats `""` as a script name
(`sh: 0: cannot open : No such file`) and exits.
**Root cause (verified):** on the `[x1] == 0` branch the code builds argv in the frame:
`add x1, x21, #0x7d0` (`"/bin/sh"`), then `stp x1, x0, [x29, #64]` — so `argv[0] = "/bin/sh"`,
`argv[1] = x0`, `argv[2] = NULL`. `argv[1]` is the incoming register `x0`; the benign fill makes
it a readable pointer to an empty string. Pinning `x0 = NULL` makes argv `{"/bin/sh", NULL}` and
the gadget **PASSes** (a real shell runs `ls /`). So the true precondition is `x0 == NULL` (or
`x0` a valid arg), which the listed constraints omit.
**Why one_gadget misses it:** the emulator tracks `sp`-relative stacks (for which it *does* emit
precise per-element argv constraints like `argv[1] == NULL || {...}`), but here argv is built at
`x29 + 0x40` off the *frame pointer*, which the candidate enters uninitialised. Writes into that
frame aren't tracked, so instead of `{"/bin/sh", x0, ...}` it falls back to the opaque
`x29+0x40 is a valid argv` — which is satisfiable by pointing the register at empty scratch even
though the code overwrites that memory. The `argv[1] = x0` requirement is lost.
**Discriminator:** not a harness limitation — the plan satisfied every listed constraint and the
gadget still yields a broken shell; adding the unlisted `x0 == NULL` fixes it. Impact: a
return-to-one_gadget with an uncontrolled `x0` gets a shell that immediately exits.
### Fix applied (one_gadget#333)
Frame-pointer-relative stores are now tracked (mirroring x86's existing `bp_based_stack`,
added as a shared `arm_family.rb` facility so any arch can opt in; aarch64 enables it with
`x29`), so the emitted constraint names `argv[1]`'s source register:
`x0 == NULL || {"/bin/sh", x0, NULL} is a valid argv` — the same shape the `sp`-relative case
already had. Verified: all four gadgets went from EXEC to PASS under Aletheia. Also
harmonized a latent inconsistency: the `sp`-relative twin `0xa321c` already had the precise
form, so the trimmer now dedups the two into one gadget.
## Cross-arch strict-mode sweep
With the harness reliability bugs fixed (see DESIGN.md's "Harness reliability fixes") and
the deep-null satisfier capability in place, `--strict` was run on every arch's current
libc for the first time (previously only run on aarch64 2.24/2.23, where it found Findings
1/2). Near-total: 62 of 64 level-1 gadgets across five fixtures PASS clean (the other 2
are the known-promotable aarch64 EXEC and Finding 5 below).
| fixture | gadgets | result |
| --- | --- | --- |
| amd64 2.43 | 11 | 11 PASS |
| i386 2.43 | 6 | 5 PASS, **1 FAIL** (Finding 5) |
| i386 2.19 | 9 | 9 PASS |
| arm 2.43 | 10 | 10 PASS |
| aarch64 2.43 | 28 | 27 PASS, 1 EXEC (known-promotable, see the level-1 sweep above) |
## Finding 5 — missing constraint: an uncontrolled register clobbers a later NULL-checked stack slot
**Gadget:** `0xed234` (i386 libc-2.43-7a08e84a). **Status: candidate bug, not yet fixed.**
Found via the strict-mode sweep above; three sibling entries into the same shared tail
(`0xed237`, `0xed240`, `0xed300`) all PASS.
**Constraint form:** `execve("/bin/sh", ebp-0x28, [ebp-0x30])` with
`[[ebp-0x30]] == NULL || [ebp-0x30] == NULL || [ebp-0x30] is a valid envp` governing envp.
**No constraint mentions `ecx`.**
**Symptom (strict):** a fully-satisfied plan still FAILs -- `edx` (the syscall's real envp
argument) reads `0xDEAD0000` (the poison fill) instead of NULL at the `execve` syscall.
**Root cause (verified):** the candidate's first instruction is
`mov %ecx, -0x30(%ebp)` -- it writes the (uncontrolled, poisoned) register `ecx` into the
exact stack slot the envp constraint later requires to read zero. Later,
`mov (%edx), %ebx` / the shared tail at `0xed300`+ reloads envp from that same slot into
`edx` for the syscall. So `ecx`'s value *is* the syscall's envp, but nothing in the
constraint list says so. Setting `ecx = 0` (NULL) makes the gadget PASS -- a real shell
runs `ls /` (confirmed via direct register probe: `edx` reads `0x0` at the syscall instead
of `0xDEAD0000`, and the full oracle run reports PASS with L2 satisfied).
**Why one_gadget misses it:** `Fetchers::Base#check_envp` only inspects tracked stack
content (`get_corresponding_stack`) when the envp pointer *itself* is a bare stack address
(`deref_count.zero?`). Here envp is `[ebp-0x30]` -- a value **read from** the stack
(`deref_count == 1`, since execve's envp argument comes from dereferencing that slot), not
the stack address itself. `check_envp`'s stack branch requires
`lmda.deref_count.zero? && stack_register?(lmda.obj)`, which is false here (deref_count is
1), so it falls through to the generic "opaque pointer" fallback -- which doesn't inspect
*what* `x86.rb`'s `bp_based_stack` already knows is stored at that slot (the Lambda for the
unresolved register `ecx`) and so never proposes `ecx == NULL` as the real precondition.
**Discriminator:** not a harness limitation -- the plan was complete, conflict-free, and
fully satisfied every listed constraint; it failed only on an input (`ecx`) the constraint
list never mentions. Impact: a return-to-one_gadget with an uncontrolled `ecx` reaches
`execve("/bin/sh", ...)` with a garbage `envp` pointer instead of the advertised NULL.
### Suggested fix (for review, not yet applied)
Extend `check_envp` (and likely `check_argv`'s analogous stack-lookup, `check_stack_argv`,
for the same shape on the argv side) to also inspect tracked stack content one level deeper
when the pointer itself is a single dereference of a stack-relative expression -- i.e.,
when `Lambda.parse(envp_ptr).deref_count == 1` and the *underlying* address is stack-relative,
look up `get_corresponding_stack`'s content at that slot. If the tracked content is an
unresolved register (not a concrete value), emit `<that register> == NULL || ...` instead of
the opaque double-deref form. This is the same class of gap as Finding 4 (frame-relative
writes existing but not being surfaced as constraints) applied to `bp_based_stack` reads
instead of `x29`-relative writes.
## Finding 6 — imprecise constraint: an untracked write through an "incoming" register hides an argv-content requirement
**Gadgets:** `0xc7a40` (aarch64 libc-2.43, `execve("/bin/sh", x4, x6)`); `0x9b9e4`
(aarch64 libc-2.23, `execve("/bin/sh", x1, x20)`); `0x9bc5c` (aarch64 libc-2.23,
`execve("/bin/sh", x0, x20)`). **Status: candidate imprecision, scoped but not yet fixed
(see fix plan below) -- pending review.** All three are the "3 EXEC*" already counted in
the Level-1 sweep summary above (found before this investigation named the mechanism);
this documents *why* they're EXEC* and what a real fix would need.
**Severity, and how this differs from Findings 1/3/5:** those were true false positives --
a *fully satisfied* plan still crashed before ever reaching a shell. Here, the gadget
genuinely **does** reach `execve("/bin/sh", ...)` and spawn a real shell (L0 passes, a
process image gets replaced) under every listed constraint; the gap is that the shell
isn't reliably *interactive* unless an unlisted register also happens to be NULL. Aletheia
already flags this honestly as EXEC* (promotable under attacker control), not PASS -- so
no one is misled into thinking these gadgets are unconditionally safe. It's the same
*class* of gap as Finding 4 (a real precondition for reliable use isn't surfaced), not the
same severity as Findings 1/3/5.
**Constraint form (0xc7a40):** `writable: x4`, `x2 == 0x1`,
`[x4] == NULL || x4 == NULL || x4 is a valid argv`, envp similarly on `x6`. **No mention of `x0`.**
**Root cause (verified):** the candidate's own code writes the argv array through `x4`:
```
c7a40: adrp x5, ...
c7a44: add x7, x5, #0x258 ; x7 = "/bin/sh" pointer
c7a48: stp x7, x0, [x4] ; argv[0] = x7, argv[1] = x0
...
c7a64: bl execve
```
`argv[1]` is the **uncontrolled register `x0`**, written moments before the call. Under
benign fill `x0` is a readable-but-garbage pointer (not NULL), so `sh` treats it as a
script filename and exits non-interactively -- exactly the "reaches a shell but isn't
drivable" EXEC signature. Confirmed empirically: setting **only** `x0 = NULL` (nothing
else touched) flips the result to PASS with full L2. The other two gadgets are the
identical shape (`x1`/`x0` as the argv pointer, an adjacent register as the untracked
`argv[1]` write).
**Why one_gadget misses it:** `x4` (or `x1`/`x0` in the siblings) is set to its real value
(`sp`, in `0x9b9e4`'s case -- see below) **outside** the analyzed candidate window; one_gadget's
fetcher does a backward, per-candidate walk, so within `0xc7a40`'s own window `x4` is just an
opaque "incoming register" (`Lambda.new('x4')`, unresolved). The emulator's write-tracking
(`sp_based_stack`, and since Finding 4, a named frame-pointer `bp_based_stack`) is keyed to
exactly two *special-cased* registers. A write through any *other* register --
`stp x7, x0, [x4]` here -- falls into the generic `add_writable` path, which records "x4
must be writable" but discards *what* got written, so `argv[1]`'s true source (`x0`) is
invisible by the time the fetcher resolves the call's arguments.
(Verified this isn't secretly a "the window should include the assignment" case: in
`0x9b9e4`'s sibling window, `x1` really is set via `mov x1, sp` one instruction before the
window starts -- if that instruction were in-window, the *existing* sp-tracking would
already get this right. It's specifically the window boundary that hides it, not a gap in
the sp-tracking itself.)
**Discriminator:** an imprecision, not a false positive (see Severity above) -- but the
constraint list still doesn't name the real precondition for a reliably-interactive shell.
### Suggested fix (for review, not yet applied -- larger than Findings 4/5)
Generalize write-tracking from the two special-cased registers (`sp`, and the named frame
pointer) to *any* register: a per-register-name write history (`Hash.new { |h,r| h[r] = {} }`),
populated by every `str`/`stp`, consulted the same way `check_argv`/`check_envp` already
consult `sp_based_stack`/`bp_based_stack`. The added complexity Findings so far haven't
needed: **invalidation**. `sp`/frame-pointer are safe to track globally because they're
essentially never reassigned to something else mid-function; an arbitrary register can be
(`mov x4, x9` later in the same window would make old `x4`-keyed entries stale and wrong to
reuse). Register writes happen at several call sites across each arch's emulator (`inst_mov`,
`inst_add`, `inst_adrp`, `inst_ldr`, post-index writeback), not one chokepoint, so a safe
implementation needs either routing all of them through a shared setter that clears that
register's write history on reassignment, or an equivalent invalidation hook. Cross-arch
(aarch64.rb, arm.rb, x86.rb all have their own register-write sites). Given the severity is
"imprecise, not false-positive" and all three known instances are already correctly flagged
EXEC* (not silently trusted), this is lower urgency than Findings 1-5 were -- worth doing for
completeness, but with real design/review needed before implementation given the
cross-cutting change and the new invalidation-correctness requirement.
## Reproduce
```
# benign (all PASS):
aletheia/bin/aletheia verify spec/data/aarch64-libc-2.24.so
# strict completeness test (2 FAIL):
aletheia/bin/aletheia verify --strict spec/data/aarch64-libc-2.24.so
```
Note: `aarch64-libc-2.27.so` aborts with SIGILL if `dlopen`ed under the glibc-2.43 host
loader, so verify it under qemu with a matched loader:
```
ALETHEIA_FORCE_QEMU=1 aletheia/bin/aletheia verify --level 1 spec/data/aarch64-libc-2.27.so
```
A per-version sysroot (the 2.27 ld.so + a stub cross-built against it) is fetched on demand;
the fixture then loads and its level-1 gadgets verify (12 PASS / 4 EXEC).
+190
View File
@@ -0,0 +1,190 @@
# gdb-Python driver: inject a satisfier plan and let the gadget run.
#
# Transport-agnostic: connects natively (`run`) or to a qemu-user gdbstub
# (`target remote`), reads the libc base + scratch address the self-describing
# park_stub wrote to $ALETHEIA_STUB_OUT (no inferior mmap, no /proc from gdb),
# then injects the plan and runs. Register names / syscall numbers come from the
# plan's "arch" block, so the same driver serves every architecture.
import gdb
import json
import os
import re
import struct
MASK = 0xFFFFFFFFFFFFFFFF
plan = json.load(open(os.environ["ALETHEIA_PLAN"]))
arch = plan["arch"]
offset = int(plan["offset"], 0)
gdb.execute("set pagination off")
gdb.execute("set confirm off")
# A version-matched sysroot run execs the stub via its own ld.so, so the stub's
# symbols (aletheia_park included) aren't known until the loader maps it after
# `run` starts -- "pending" defers resolving the breakpoint to that point,
# instead of erroring out immediately for want of a defined symbol.
gdb.execute("set breakpoint pending on")
if arch.get("gdb_arch"):
gdb.execute("set architecture %s" % arch["gdb_arch"])
# A remote (qemu-user gdbstub) target's libraries live locally too (the same
# path qemu resolved them from via QEMU_LD_PREFIX); reading their symbols over
# the remote protocol instead of straight from disk is slow and, for some old
# binaries, has been observed to corrupt gdb's own state entirely (a bogus
# jump target and SIGSEGV before the plan is ever injected). `set sysroot`
# points gdb at the local copies it already has.
if os.environ.get("ALETHEIA_SYSROOT"):
gdb.execute("set sysroot %s" % os.environ["ALETHEIA_SYSROOT"])
# Park at the stub's marker, then bring the inferior to it (native runs it;
# a remote target is already running and just needs `continue`).
gdb.execute("break aletheia_park")
connect = os.environ.get("ALETHEIA_CONNECT", "run")
if connect == "run":
gdb.execute("run")
else:
gdb.execute("target remote %s" % connect)
gdb.execute("continue")
info = open(os.environ["ALETHEIA_STUB_OUT"]).read()
base = int(re.search(r"ALETHEIA_BASE=(0x[0-9a-fA-F]+)", info).group(1), 16)
scratch = int(re.search(r"ALETHEIA_SCRATCH=(0x[0-9a-fA-F]+)", info).group(1), 16)
gadget = base + offset
gdb.write("ALETHEIA base=%#x gadget=%#x scratch=%#x\n" % (base, gadget, scratch))
# Seed the L2 command; a `sh -c <cmd>` gadget points its command slot here so the
# shell runs `ls /` itself. Keep in sync with the satisfier's COMMAND_POOL.
gdb.selected_inferior().write_memory(scratch + 0x200, b"ls /\x00")
# Default fill for registers the plan doesn't set: benign (readable scratch),
# poison (unmapped -> unlisted derefs fault), or null (0 -> argv terminates).
POISON = 0xDEAD0000
if plan.get("poison_default"):
fill = POISON
elif plan.get("null_default"):
fill = 0
elif plan.get("benign_default"):
fill = scratch + 0x100
else:
fill = None
if fill is not None:
for r in arch["gprs"]:
gdb.execute("set $%s = %#x" % (r, fill))
def set_reg(reg, val):
# gdb rejects `set $xmm0 = <int>` (an XMM register is a vector union, not a
# scalar). The satisfier only ever pins an XMM lane to a u64 (a `(u64)xmm*`
# constraint), so write the 64-bit lanes directly.
if reg.startswith("xmm"):
gdb.execute("set $%s.v2_int64[0] = %#x" % (reg, val & MASK))
gdb.execute("set $%s.v2_int64[1] = 0" % reg)
else:
gdb.execute("set $%s = %#x" % (reg, val & MASK))
for reg, val in plan.get("regs", {}).items():
if isinstance(val, dict):
if "scratch_off" in val:
val = scratch + val["scratch_off"] # a scratch pointer
elif "base_off" in val:
val = base + val["base_off"] # a libc load-base offset (i386 GOT)
elif "neg_base_off" in val:
val = -(base + val["neg_base_off"]) # cancels a libc address the gadget adds
set_reg(reg, int(val))
# Scratch-relative memory writes (a pointer value, keyed by the offset to write
# it at) -- built by the satisfier for a chained dereference like `[[sp]]`,
# where the first level needs a real pointer rather than the zero-fill a single
# dereference relies on. See Satisfier#apply_deep_null.
word_size = arch.get("word_size", 8)
word_fmt = {4: "<I", 8: "<Q"}[word_size]
word_mask = (1 << (word_size * 8)) - 1
for off, val in plan.get("mem", {}).items():
off = int(off)
fmt, mask = word_fmt, word_mask
if isinstance(val, dict) and "scratch_off" in val:
val = scratch + val["scratch_off"]
elif isinstance(val, dict) and "int32" in val:
# A 4-byte field, e.g. a file descriptor. Writing a full word here would
# run over the neighbouring field -- two adjacent descriptors are 4 bytes
# apart, and a word-sized write of one zeroes the other.
val, fmt, mask = val["int32"], "<i", 0xffffffff
gdb.selected_inferior().write_memory(scratch + off, struct.pack(fmt, int(val) & mask))
# Libc-global writes (keyed by base-relative offset): a constraint on a $base+off
# memory value, e.g. `(s64)[$base+off] <= 0`, satisfied by writing that global.
for off, val in plan.get("base_mem", {}).items():
if isinstance(val, dict) and "scratch_off" in val:
val = scratch + val["scratch_off"]
gdb.selected_inferior().write_memory(base + int(off), struct.pack(word_fmt, int(val) & word_mask))
sp = scratch + plan.get("sp_offset", 0x2000)
gdb.execute("set $%s = %#x" % (arch["sp"], sp))
gdb.execute("set $%s = %#x" % (arch["pc"], gadget))
if arch.get("thumb"):
gdb.execute("set $cpsr = ($cpsr | 0x20)") # arm: enter Thumb state (CPSR T bit)
# posix_spawn forks a child that execs the shell. Natively, gdb follows the child
# and drives it directly. Over a qemu-user gdbstub, a single stub can't debug both
# sides of a fork, so let the child run free (it inherits the guest tty) and stay
# with the parent -- L2 on the pty is the arbiter either way.
try:
if connect == "run":
gdb.execute("set follow-fork-mode child")
gdb.execute("set detach-on-fork off")
else:
gdb.execute("set follow-fork-mode parent")
gdb.execute("set detach-on-fork on")
except gdb.error:
pass
def readable(addr):
if addr == 0:
return True # NULL argv/envp is accepted by execve (empty)
try:
gdb.selected_inferior().read_memory(addr, 8)
return True
except gdb.MemoryError:
return False
SHELLS = ("dash", "bash", "sh", "busybox", "zsh")
def execd_shell(pid):
try:
return os.path.basename(os.readlink("/proc/%d/exe" % pid)) in SHELLS
except OSError:
return False
# L0: the deterministic "reaches a shell" signal. A straight-line execve stops at
# the syscall entry, where we verify the "/bin/sh" path and readable argv/envp;
# posix_spawn runs through to the new image, caught by `catch exec` -- but only
# natively, where the vforked child is followed (`follow-fork-mode child` above).
# Over a qemu-user gdbstub the child is never followed, so `catch exec` can only
# ever fire in the (non-execing) parent -- useless there, and qemu-aarch64's
# gdbstub SIGSEGVs some straight-line execl() paths when it's armed regardless
# (reproduced: works cleanly without it, corrupts execl with it).
gdb.execute("catch syscall execve execveat")
if connect == "run":
try:
gdb.execute("catch exec")
except gdb.error:
pass
gdb.execute("continue")
l0 = False
try:
if int(gdb.parse_and_eval("$" + arch["sysno_reg"])) in arch["execve_syscalls"]:
path = gdb.execute("x/s $" + arch["path_reg"], to_string=True)
argv = int(gdb.parse_and_eval("$" + arch["argv_reg"])) & MASK
envp = int(gdb.parse_and_eval("$" + arch["envp_reg"])) & MASK
l0 = ('"/bin/sh"' in path) and readable(argv) and readable(envp)
except gdb.error:
pass
if not l0 and connect == "run":
l0 = execd_shell(gdb.selected_inferior().pid)
gdb.write("ALETHEIA_L0=%s\n" % ("pass" if l0 else "fail"))
# Let the shell run for the L2 (`ls /`) check on the tty.
gdb.execute("delete")
gdb.execute("continue")
+60
View File
@@ -0,0 +1,60 @@
# frozen_string_literal: true
module Aletheia
module Arch
# AArch64 backend: the reference architecture. All arch-specific facts the
# satisfier, driver, and oracle need live here so a new architecture is a
# new backend object rather than edits scattered across the harness.
module AArch64
module_function
def name = 'aarch64'
# General-purpose registers the satisfier may assign.
def gprs = (0..30).map { |i| "x#{i}" }
# Only +sp+ invariantly names a live stack address that can't be NULL; the
# frame pointer +x29+ is a general register the attacker controls in these
# gadgets (like amd64's +rbp+), so a store through it carries an explicit
# +writable: x29+imm+ constraint rather than being assumed valid.
def stack_regs = %w[sp]
def sp = 'sp'
def pc = 'pc'
# Whether this backend can run the target libc natively on the host.
# @param [String] host_machine value of +uname -m+
def native_on?(host_machine) = host_machine == 'aarch64'
# Under qemu, an older aarch64 libc needs a per-version sysroot (its ld.so
# differs too much from the host's); the native run loads it directly.
def version_strict? = true
# gdb register expression for GPR +name+ (e.g. "x0" -> "$x0").
def gdb_reg(name) = "$#{name}"
# Normalise a 32-bit view to its 64-bit register.
# @example +w21+ -> +x21+, +wzr+ -> +xzr+
def normalize_reg(reg) = reg.sub(/\Aw(\d+|zr)\z/, 'x\1')
# park_stub binary for this arch (built by the build helper).
def stub_binary = 'park_stub_aarch64'
# qemu-user transport config. Used when aarch64 is the *foreign* arch (a
# non-aarch64 host), or when +ALETHEIA_FORCE_QEMU+ drives it under qemu on an
# aarch64 host -- there the transport resolves the runtime prefix to the host
# root instead of this cross sysroot.
def qemu
{ 'bin' => 'qemu-aarch64', 'ld_prefix' => '/usr/aarch64-linux-gnu',
'gdb_arch' => 'aarch64' }
end
# Register/syscall model the gdb driver needs (serialized into the plan).
def driver_model
{ 'gprs' => gprs, 'sp' => sp, 'pc' => pc, 'gdb_arch' => 'aarch64', 'word_size' => 8,
'sysno_reg' => 'x8', 'execve_syscalls' => [221, 281],
'path_reg' => 'x0', 'argv_reg' => 'x1', 'envp_reg' => 'x2' }
end
end
end
end
+60
View File
@@ -0,0 +1,60 @@
# frozen_string_literal: true
module Aletheia
module Arch
# amd64 (x86-64) backend. Runs under qemu-user on a non-x86 host; the
# transport/driver are arch-neutral, so only this register/ABI model differs.
module Amd64
module_function
def name = 'amd64'
# General-purpose registers the satisfier may assign / the driver fills.
def gprs = %w[rax rbx rcx rdx rsi rdi rbp r8 r9 r10 r11 r12 r13 r14 r15]
# Only rsp names a live stack address that can't be NULL; rbp is a general
# register the attacker controls in these gadgets.
def stack_regs = %w[rsp]
def sp = 'rsp'
def pc = 'rip'
def native_on?(host_machine) = host_machine == 'x86_64'
# A big enough version gap breaks dlopen just like the other arches (cf.
# i386): the default cross sysroot's own ld.so is glibc 2.43, and dlopen-ing
# a libc as old as 2.19/2.26 as a *secondary* object crashes -- an ifunc
# resolver (compiled against that old glibc's internal CPU-feature-detection
# ABI) gets invoked by the much-newer host ld.so and jumps to garbage
# (observed: SIGSEGV at a bogus 0x500000000, even with no gdb involved at
# all). A version-matched sysroot avoids the whole ABI gap.
def version_strict? = true
def gdb_reg(name) = "$#{name}"
E2R = { 'eax' => 'rax', 'ebx' => 'rbx', 'ecx' => 'rcx', 'edx' => 'rdx',
'esi' => 'rsi', 'edi' => 'rdi', 'ebp' => 'rbp', 'esp' => 'rsp' }.freeze
private_constant :E2R
# Normalise a 32-bit view to its 64-bit register; setting the full register
# sets the low 32 bits, so an +eax+ constraint is satisfied via +rax+.
# @example +eax+ -> +rax+, +r8d+ -> +r8+
def normalize_reg(reg) = E2R[reg] || reg.sub(/\Ar(\d+)d\z/, 'r\1')
def stub_binary = 'park_stub_x86_64'
# qemu-user transport: emulator binary, the sysroot providing the stub's own
# ld.so + libc (QEMU_LD_PREFIX), and the gdb architecture to select.
def qemu
{ 'bin' => 'qemu-x86_64', 'ld_prefix' => '/usr/x86_64-linux-gnu',
'gdb_arch' => 'i386:x86-64' }
end
def driver_model
{ 'gprs' => gprs, 'sp' => sp, 'pc' => pc, 'gdb_arch' => 'i386:x86-64', 'word_size' => 8,
'sysno_reg' => 'rax', 'execve_syscalls' => [59, 322],
'path_reg' => 'rdi', 'argv_reg' => 'rsi', 'envp_reg' => 'rdx' }
end
end
end
end
+59
View File
@@ -0,0 +1,59 @@
# frozen_string_literal: true
module Aletheia
module Arch
# 32-bit ARM (armhf) backend. Runs under qemu-user; like i386 the exec*
# arguments reach the kernel in registers (the EABI syscall ABI: number in
# +r7+, args +r0..r2+). Modern armhf libc is Thumb-2, so the driver enters
# gadgets in Thumb state (+thumb+ in {#driver_model}).
module Arm
module_function
def name = 'arm'
# General-purpose registers the satisfier may assign / the driver fills.
def gprs = (0..12).map { |i| "r#{i}" }
# Only sp names a live stack address that can't be NULL.
def stack_regs = %w[sp]
def sp = 'sp'
def pc = 'pc'
# AAPCS role names objdump prints for the high general-purpose registers.
ALIASES = { 'sl' => 'r10', 'fp' => 'r11', 'ip' => 'r12' }.freeze
# Resolve a role name to the register it denotes, so a constraint written
# as +ip != 0x0+ is recognised as being about an assignable register.
def normalize_reg(reg) = ALIASES[reg] || reg
def native_on?(host_machine) = %w[armv7l armv6l arm].include?(host_machine)
# arm runs via stub self-injection rather than a gdbstub: qemu-arm's
# gdbstub kills the fork'd child of a posix_spawn gadget, so the L2 shell
# never runs. The stub applies the plan and jumps itself, keeping the whole
# run under plain qemu-user where the child survives (see {Transport::SelfInject}).
def self_inject? = true
# Like i386, an older armhf libc needs a per-version sysroot (its init
# crashes under a newer ld.so); the toolchain-matched version uses the default.
def version_strict? = true
def gdb_reg(name) = "$#{name}"
def stub_binary = 'park_stub_arm'
def qemu
{ 'bin' => 'qemu-arm', 'ld_prefix' => '/usr/arm-linux-gnueabihf',
'gdb_arch' => 'arm' }
end
def driver_model
{ 'gprs' => gprs, 'sp' => sp, 'pc' => pc, 'gdb_arch' => 'arm', 'word_size' => 4,
'sysno_reg' => 'r7', 'execve_syscalls' => [11, 387],
'path_reg' => 'r0', 'argv_reg' => 'r1', 'envp_reg' => 'r2',
'thumb' => true }
end
end
end
end
+51
View File
@@ -0,0 +1,51 @@
# frozen_string_literal: true
module Aletheia
module Arch
# i386 (x86-32) backend. Like {Amd64}, runs under qemu-user on a non-x86 host;
# only the register/ABI model differs. The exec* arguments reach the kernel in
# +ebx/ecx/edx+ (the 32-bit syscall ABI), even though the libc call takes them
# on the stack.
module I386
module_function
def name = 'i386'
# General-purpose registers the satisfier may assign / the driver fills.
def gprs = %w[eax ebx ecx edx esi edi ebp]
# Only esp names a live stack address that can't be NULL.
def stack_regs = %w[esp]
def sp = 'esp'
def pc = 'eip'
def native_on?(host_machine) = %w[i386 i486 i586 i686].include?(host_machine)
# i386's loader/libc reject a version-mismatched libc (an older fixture's init
# crashes under a newer ld.so), so an older fixture needs a per-version sysroot
# (see {Transport::Base#sysroot}). amd64 tolerates the mismatch and does not.
def version_strict? = true
def gdb_reg(name) = "$#{name}"
# i386 constraints already name the 32-bit registers, so no folding is needed.
def normalize_reg(reg) = reg
def stub_binary = 'park_stub_i386'
# qemu-user transport: emulator binary, the sysroot providing the stub's own
# ld.so + libc (QEMU_LD_PREFIX), and the gdb architecture to select.
def qemu
{ 'bin' => 'qemu-i386', 'ld_prefix' => '/usr/i686-linux-gnu',
'gdb_arch' => 'i386' }
end
def driver_model
{ 'gprs' => gprs, 'sp' => sp, 'pc' => pc, 'gdb_arch' => 'i386', 'word_size' => 4,
'sysno_reg' => 'eax', 'execve_syscalls' => [11, 358],
'path_reg' => 'ebx', 'argv_reg' => 'ecx', 'envp_reg' => 'edx' }
end
end
end
end
+91
View File
@@ -0,0 +1,91 @@
# frozen_string_literal: true
module Aletheia
# An independent parser for the operand expressions that appear inside
# one_gadget constraint strings, e.g. +x0+, +sp+0x218+, +[sp+0x50]+,
# +(u16)[sp+0x218]+, +x20+0x338+, +$base+0x16b250+, +environ+, +NULL+.
#
# Deliberately written from scratch rather than reusing the emulator's own
# +Lambda.parse+: the tool under verification must not supply the semantics
# used to check it. This keeps a bug in one_gadget's parser from silently
# propagating into the verifier. (A cross-check against +Lambda.parse+ is
# cheap and can be layered on top when desired.)
# +inner_imm+ is the displacement applied *between* two dereferences, as in
# +[[$base+0x1c2438]+0xe8]+ (follow a pointer, then read a field off it): the
# address is +[reg+imm] + inner_imm+. It is 0 for every single-level operand,
# where +imm+ alone describes the displacement.
# +base_imm+ is a fixed libc address added to the register, as in
# +(r1 + $base+0x2d364)+: the value is +reg + $base+base_imm + imm+. It is 0
# for every operand that names no such address.
Operand = Struct.new(:reg, :imm, :deref, :cast_bits, :inner_imm, :base_imm) do
# @return [Boolean] a bare register with no displacement and no dereference.
def bare_reg?
!reg.nil? && imm.zero? && deref.zero?
end
# @return [Boolean] a plain integer literal (no register, no dereference).
def literal?
reg.nil? && deref.zero?
end
end
# Reads one of those expressions into an {Operand}. Kept apart from the struct
# so the value and the syntax that produces it stay separable.
module OperandParser
module_function
NUM = /0x[0-9a-fA-F]+|\d+/
# A register added to a fixed libc address, optionally displaced further.
# @example +(r1 + $base+0x2d364)+, +(r2 + $base+0x5048c)+0x8+
BASE_SUM = /\A\(([a-zA-Z_]\w*) \+ \$base\s*([+-]\s*#{NUM})\)\s*([+-]\s*#{NUM})?\z/
# @param [String] str
# @return [Aletheia::Operand]
def parse(str)
s = str.strip
cast = nil
if (m = s.match(/\A\(([su])(\d+)\)/))
cast = m[2].to_i
s = s[m[0].length..].strip
end
deref = 0
while s.start_with?('[') && s.end_with?(']')
deref += 1
s = s[1..-2].strip
end
# Matched before the grouping parentheses are stripped: for a base sum they
# are what delimits it from a trailing displacement.
if (m = s.match(BASE_SUM))
return Operand.new(m[1], displacement(m[3]), deref, cast, 0, displacement(m[2]))
end
# A parenthesised sum, e.g. the `(x0 + 0x1)` of `(u64)(x0 + 0x1) <= 0x0`:
# the parentheses only group, they don't dereference.
s = s[1..-2].strip while s.start_with?('(') && s.end_with?(')')
return Operand.new(nil, 0, deref, cast, 0, 0) if s == 'NULL'
return Operand.new(nil, Integer(s), deref, cast, 0, 0) if s.match?(/\A-?(?:#{NUM})\z/)
# A displacement off a dereferenced value, e.g. `[$base+0x1c2438]+0xe8`
# (what remains of `[[$base+0x1c2438]+0xe8]` once the outer brackets are
# stripped). One such level is modelled; anything deeper is not needed.
if (m = s.match(/\A(\[.+\])\s*([+-]\s*(?:#{NUM}))?\z/))
inner = parse(m[1])
raise ArgumentError, "unparseable operand: #{str.inspect}" unless inner.deref == 1 && inner.inner_imm.zero?
return Operand.new(inner.reg, inner.imm, deref + inner.deref, cast, displacement(m[2]), inner.base_imm)
end
m = s.match(/\A(\$?[a-zA-Z_][a-zA-Z0-9_]*)\s*([+-]\s*(?:#{NUM}))?\z/)
raise ArgumentError, "unparseable operand: #{str.inspect}" unless m
Operand.new(m[1], displacement(m[2]), deref, cast, 0, 0)
end
# The integer a matched displacement denotes, 0 when the operand carries none.
# @param [String, nil] text
# @return [Integer]
def displacement(text)
text ? Integer(text.gsub(/\s+/, '')) : 0
end
end
end
+139
View File
@@ -0,0 +1,139 @@
# frozen_string_literal: true
require 'pty'
require 'json'
require 'timeout'
require 'tempfile'
require_relative 'transport'
require_relative 'arch/aarch64'
module Aletheia
# The success oracle. Launches the target libc under gdb with the plan
# injected, then drives the spawned shell over a pty and validates that it can
# run +ls /+ and reproduce the host's real root directory. That empirical
# result -- a real shell listing the real filesystem -- is what decides PASS,
# independent of anything one_gadget reports.
class Oracle
HERE = File.expand_path('..', __dir__) # aletheia/lib
ROOT = File.expand_path('..', HERE) # aletheia/
Result = Struct.new(:result, :reason, :base, :shell_output, :seen, :expected, :l0,
keyword_init: true)
def initialize(target:, arch: Arch::AArch64, quorum: %w[bin etc usr lib proc dev tmp var],
startup_wait: 2, io_timeout: 6)
@target = target
@arch = arch
@transport = Transport.for(arch, target)
@startup_wait = startup_wait
@io_timeout = io_timeout
real_root = Dir.children('/')
@expected = quorum.select { |d| real_root.include?(d) }
end
# @param [Aletheia::Satisfier::Plan] plan
# @return [Aletheia::Oracle::Result]
def run(plan)
plan_hash = plan.to_h.merge(arch: @arch.driver_model)
Tempfile.create(['aletheia-plan', '.json']) do |f|
f.write(JSON.generate(plan_hash))
f.flush
drive(f.path)
end
end
private
def drive(plan_path)
master, slave = PTY.open
log_path = tempfile_path('aletheia-gdb', '.log')
stub_out = tempfile_path('aletheia-stub', '.txt')
# Own process group(s) so a wedged inferior can be killed wholesale.
pids = @transport.launch(plan_path: plan_path, stub_out: stub_out, slave: slave, log: log_path)
slave.close
begin
Timeout.timeout(@startup_wait + 2) do
sleep @startup_wait
master.write("ls /\n")
master.write("exit\n")
end
rescue Errno::EIO, Timeout::Error
# fall through to reading whatever is available
end
output = read_all(master)
reap(pids)
# Read as bytes: qemu's -strace prints an argv the gadget built out of
# whatever the libc holds there, which is not text, and every later
# match? / include? on the log would raise on the invalid encoding --
# arriving as a "harness error" against a gadget that ran fine.
log = File.binread(log_path)
[log_path, stub_out].each do |p|
File.unlink(p)
rescue StandardError
nil
end
base = log[/ALETHEIA base=(0x[0-9a-f]+)/, 1]
l0 = log.include?('ALETHEIA_L0=pass')
seen = @expected.select { |d| output.include?(d) }
common = { base: base, shell_output: output, seen: seen, expected: @expected, l0: l0 }
if !@expected.empty? && seen.sort == @expected.sort
# L2: the spawned shell actually listed the real root.
Result.new(result: 'PASS', reason: nil, **common)
elsif l0
# The gadget reached execve("/bin/sh") with valid args, but the harness
# could not drive `ls /` through this shell (e.g. a fixed `-c` command,
# an uncontrolled argv[1], or a posix_spawn parent/child tty race).
Result.new(result: 'EXEC', reason: 'execve("/bin/sh") reached; shell not L2-drivable', **common)
elsif (sysno = log[/Unknown syscall (\d+)/, 1])
# The emulator (qemu-user, -strace) hit a syscall it doesn't implement, so
# the gadget couldn't run to a shell. A harness limit, not a gadget verdict.
# @example qemu-arm lacks clone3 (435), which glibc posix_spawn forks with.
Result.new(result: 'SKIP', reason: "qemu could not emulate syscall #{sysno} (harness limitation)", **common)
else
Result.new(result: 'FAIL', reason: 'no execve("/bin/sh") and no shell output', **common)
end
end
# A fresh temp file path (created empty, closed) for a subprocess to write.
def tempfile_path(prefix, suffix)
f = Tempfile.create([prefix, suffix])
path = f.path
f.close
path
end
# Wait briefly for each pid to exit; kill any wedged process group wholesale so
# we never block the sweep. Reap the driver first, then the emulator.
def reap(pids)
Array(pids).each do |pid|
Timeout.timeout(3) { Process.wait(pid) }
rescue Timeout::Error
begin
Process.kill('-KILL', Process.getpgid(pid))
rescue StandardError
nil
end
begin
Process.wait(pid)
rescue StandardError
nil
end
rescue Errno::ECHILD
nil
end
end
def read_all(master)
# Bytes again (see #drive): a shell fed a garbage argv can echo anything.
buf = +''.b
Timeout.timeout(@io_timeout) { loop { buf << master.readpartial(4096).b } }
buf
rescue Errno::EIO, EOFError, Timeout::Error
buf
end
end
end
+132
View File
@@ -0,0 +1,132 @@
# frozen_string_literal: true
require 'json'
require 'elftools'
require 'one_gadget'
require_relative 'arch/aarch64'
require_relative 'arch/amd64'
require_relative 'arch/i386'
require_relative 'arch/arm'
require_relative 'satisfier'
require_relative 'oracle'
module Aletheia
# Ties the pieces together: enumerate a libc's gadgets, satisfy each into a
# plan, run the oracle, and aggregate machine-readable results.
#
# A gadget is reported as:
# PASS - the spawned shell listed the real root (see {Oracle})
# FAIL - a complete, satisfied plan still failed to yield a working shell
# (a candidate one_gadget bug -- most often a missing constraint)
# SKIP - the satisfier could not produce a plan (a harness limitation, not
# a verdict on the gadget)
class Runner
ARCHES = { amd64: Arch::Amd64, i386: Arch::I386, arm: Arch::Arm, aarch64: Arch::AArch64 }.freeze
# The mapping granularity a loader rounds a segment up to. The smallest any
# target uses, so the spare tail it implies is mapped whatever the real page
# size turns out to be (a larger page only rounds further up).
PAGE_SIZE = 0x1000
def initialize(target:, arch: nil, strict: false)
@target = target
@arch = arch || arch_of(target)
@satisfier = Satisfier.new(@arch, got_offset: got_offset(target),
spare_writable: spare_writable(target), strict: strict)
@oracle = Oracle.new(target: target, arch: @arch)
end
# Pick the arch backend from the target ELF's machine.
def arch_of(target)
ARCHES.fetch(OneGadget::Helper.architecture(target)) do |m|
raise ArgumentError, "unsupported architecture: #{m}"
end
end
# The libc PLTGOT file offset, for i386's GOT-base constraint; nil when absent.
def got_offset(target)
File.open(target) do |f|
ELFTools::ELFFile.new(f).segment_by_type(:dynamic)&.tag_by_type(:pltgot)&.value
end
rescue StandardError
nil
end
# Libc offsets that are mapped writable but that libc itself does not use: the
# tail of the last page of its writable segment, past the end of .bss. The
# loader rounds that segment up to a page boundary and zero-fills the
# remainder, so the tail is real memory nothing else reads or writes -- the
# one place a store the harness must steer somewhere can go without
# corrupting the libc that is about to run.
# @return [Range, nil] nil when the segment ends on a page boundary, leaving
# no tail (the constraint then has nowhere to go, and its gadget SKIPs).
def spare_writable(target)
end_of_data = File.open(target) do |f|
ELFTools::ELFFile.new(f).segments_by_type(:load).select(&:writable?)
.map { |s| s.header.p_vaddr.to_i + s.header.p_memsz.to_i }.max
end
return nil unless end_of_data
first = (end_of_data + 0xf) & ~0xf # keep every slot pointer-aligned
last = ((end_of_data + PAGE_SIZE - 1) / PAGE_SIZE) * PAGE_SIZE
first < last ? (first...last) : nil
rescue StandardError
nil
end
# @param [Array<Integer>, nil] offsets restrict to these gadget offsets
# @param [Integer] level one_gadget output level; 0 keeps only the
# highest-scoring gadgets, 1 enumerates every gadget found
# @return [Array<Hash>] one result record per gadget
def run(offsets: nil, level: 0, &block)
gadgets = OneGadget.gadgets(file: @target, force_file: true, details: true, level: level)
gadgets = gadgets.select { |g| offsets.include?(g.offset) } if offsets
gadgets.map do |g|
result = verify(g)
block&.call(result)
result
end
end
private
def verify(gadget)
verify!(gadget)
rescue StandardError => e
{ offset: format('%#x', gadget.offset), effect: gadget.effect,
result: 'SKIP', reason: "harness error: #{e.class}: #{e.message}" }
end
def verify!(gadget)
plan = @satisfier.satisfy(gadget)
record = {
offset: format('%#x', gadget.offset),
effect: gadget.effect,
constraints: gadget.constraints,
chosen_branches: plan.branches,
plan_regs: plan.regs.transform_values { |v| v.is_a?(Integer) ? format('%#x', v) : v }
}
return record.merge(result: 'SKIP', reason: plan.reason) if plan.status == 'skip'
res = @oracle.run(plan)
record = record.merge(
result: res.result, reason: res.reason, base: res.base, l0: res.l0,
seen_root_entries: res.seen, expected_root_entries: res.expected
)
# An EXEC gadget reached a shell but the harness couldn't drive it. Retry with
# uncontrolled registers nulled: if the code writes such a register as argv[1],
# nulling it terminates argv and the shell becomes interactive (drivable). A
# promoted gadget is genuinely usable given that (attacker-controlled) input.
record[:promotable] = promotable?(plan) if res.result == 'EXEC'
record
end
def promotable?(plan)
null_plan = plan.dup
null_plan.benign_default = false
null_plan.null_default = true
@oracle.run(null_plan).result == 'PASS'
end
end
end
File diff suppressed because it is too large Load Diff
+262
View File
@@ -0,0 +1,262 @@
# frozen_string_literal: true
require 'json'
require 'socket'
module Aletheia
# How the target process is launched and driven: natively (host arch) or under
# qemu-user (foreign arch) via a gdbstub. Both expose the same contract to the
# oracle -- launch the stub + gdb driver with the guest's tty on +slave+ -- and
# return the pids to reap. The self-describing park_stub means neither transport
# needs inferior function calls or /proc access from gdb.
module Transport
ROOT = File.expand_path('../..', __dir__) # aletheia/
# Pick the transport from the *host* arch, not a per-arch flag, so the same
# backend runs natively on its own host and under qemu-user anywhere else. Set
# +ALETHEIA_FORCE_QEMU+ to drive a native arch through qemu too (e.g. to
# exercise the aarch64 qemu path on an aarch64 host).
# @return [Transport::Native, Transport::Qemu, Transport::SelfInject]
def self.for(arch, target)
if arch.native_on?(host_machine) && !ENV['ALETHEIA_FORCE_QEMU']
Native.new(arch, target)
elsif arch.respond_to?(:self_inject?) && arch.self_inject?
SelfInject.new(arch, target)
else
Qemu.new(arch, target)
end
end
# +uname -m+ of the host running the harness.
def self.host_machine
@host_machine ||= `uname -m`.strip
end
# What both transports have in common: where the stub and the target live,
# and how a plan is rendered for them.
class Base
def initialize(arch, target)
@arch = arch
@target = target
end
def driver = File.join(ROOT, 'driver.py')
# A per-version sysroot for this fixture (under +sysroots/<arch>-<major.minor>/+),
# or nil. Used for a libc too far from the runtime's own version to dlopen
# directly -- it carries the matching ld.so and a park_stub linked against
# that libc. Built on demand (and cached) when missing, so the git-ignored
# +sysroots/+ can be deleted anytime to reclaim disk.
#
# Needed under a *native* transport too, not just qemu: dlopen-ing a full
# libc.so.6 as a secondary shared object binds glibc-private, ld.so-internal
# symbols (e.g. +_dl_exception_create+, +__tunable_get_val+) that aren't
# ABI-stable across versions -- found via a native aarch64 host (glibc 2.43)
# SIGILLing inside its own ld.so while calling a libc-2.27 fixture's init,
# a version gap plenty of *qemu* runs already carry safely. A version match
# is the only thing that's actually safe to assume needs nothing extra.
def sysroot
return @sysroot if defined?(@sysroot)
ver = File.basename(@target)[/(\d+\.\d+)/, 1]
need = ver && @arch.version_strict? && ver != default_libc_version
dir = need && File.join(ROOT, 'sysroots', "#{@arch.name}-#{ver}")
@sysroot = dir && (stub_built?(dir) || build_sysroot(dir)) ? dir : nil
end
# Whether this run drives the target through qemu (a foreign arch, or a native
# one forced under qemu) rather than natively.
def qemu_transport?
!@arch.native_on?(Transport.host_machine) || ENV.fetch('ALETHEIA_FORCE_QEMU', nil)
end
# QEMU_LD_PREFIX base: the host root for a native arch (forced under qemu),
# else the arch's cross sysroot.
def runtime_prefix
@arch.native_on?(Transport.host_machine) ? '/' : @arch.qemu['ld_prefix']
end
# glibc major.minor of the libc the runtime prefix resolves to (the host libc
# for a native arch, the cross sysroot's otherwise).
def default_libc_version
libc = Dir[File.join(runtime_prefix, 'lib', '**', 'libc.so.6')].first ||
Dir[File.join(runtime_prefix, 'lib', '*', 'libc.so.6')].first
libc && File.binread(libc)[/GLIBC (\d+\.\d+)/, 1]
end
# Built, and not stale: a per-version stub is a cross-compile of park_stub.c
# baked with the memory-layout constants (SCRATCH_SIZE etc.) current when it
# was built. If park_stub.c has since changed, a cached stub silently drifts
# out of sync with the driver/satisfier's current layout -- e.g. a stub built
# before a SCRATCH_SIZE bump still only mmaps the old (smaller) size, so a
# plan computed against the new size writes past its actual mapping and
# faults. Rebuild whenever the source is newer than the cached binary.
def stub_built?(dir)
src_mtime = File.mtime(File.join(ROOT, 'park_stub.c'))
%w[park_stub park_stub_native].all? do |name|
stub = File.join(dir, name)
File.file?(stub) && File.mtime(stub) >= src_mtime
end
end
# A few fixtures are plain (non-Ubuntu) glibc builds and carry no "Ubuntu
# GLIBC" banner to parse an exact package version from -- e.g.
# libc-2.26-2104f3d4...'s banner reads "GNU C Library (GNU libc) stable
# release version 2.26", with no Ubuntu package suffix. Recorded by hand
# from a same-major.minor sibling fixture that does carry the banner
# (same glibc release, so ABI-equivalent for sysroot purposes).
NON_UBUNTU_FIXTURE_VERSIONS = {
'libc-2.26-2104f3d4ad5cf68603afbe7ba1a17f5ac99c5988' => '2.26-0ubuntu2.1'
}.freeze
# Build the per-version sysroot from the fixture's own Ubuntu package version
# (Ubuntu-sourced fixtures only). Returns whether its park_stub now exists.
def build_sysroot(dir)
uver = File.binread(@target)[/Ubuntu E?GLIBC (\d[^)]*)/, 1] ||
NON_UBUNTU_FIXTURE_VERSIONS[File.basename(@target, '.so')] or return false
warn "aletheia: building #{File.basename(dir)} sysroot (libc #{uver})..."
system(File.join(ROOT, 'build_sysroot.sh'), @arch.name, uver, %i[out err] => File::NULL)
stub_built?(dir)
end
# The park_stub to run: an explicit override, else the per-version sysroot's
# stub, else the arch default.
def stub
ENV['ALETHEIA_STUB'] || (sysroot && File.join(sysroot, 'park_stub')) ||
File.join(ROOT, @arch.stub_binary)
end
end
# Native: one gdb process runs the stub directly; L2 tty via inferior-tty.
class Native < Base
def launch(plan_path:, stub_out:, slave:, log:)
env = { 'ALETHEIA_PLAN' => plan_path, 'ALETHEIA_STUB_OUT' => stub_out, 'ALETHEIA_CONNECT' => 'run' }
cmd = ['gdb', '-nx', '-q', '-batch', '-ex', "set inferior-tty #{slave.path}",
'-x', driver, '--args', stub, @target]
[spawn(env, *cmd, out: log, err: log, pgroup: true)]
end
private
# A version-matched sysroot's normal park_stub keeps a generic interpreter
# path (qemu's QEMU_LD_PREFIX redirects it into the sysroot) -- a real
# execve has no such redirection, so it would still load through the
# HOST's system ld.so, the exact mismatch {#sysroot} exists to avoid.
# +park_stub_native+ (build_sysroot.sh) has the sysroot's own ld.so baked
# into its interpreter via +--dynamic-linker+, so the kernel loads the
# right one directly, and GDB still sees a normal, immediately-symboled
# primary executable (no pending-breakpoint dance for a stub loaded only
# via a hand-invoked interpreter).
def stub
return super unless sysroot && !ENV['ALETHEIA_STUB']
File.join(sysroot, 'park_stub_native')
end
end
# Qemu-user: the emulator runs the stub with the guest's stdio on the tty and
# exposes a gdbstub; gdb-multiarch attaches over TCP and runs the driver.
class Qemu < Base
def launch(plan_path:, stub_out:, slave:, log:)
q = @arch.qemu
port = free_port
# An explicit override, else the per-version sysroot (matching ld.so for an
# older libc), else the runtime prefix (host root for a native arch forced
# under qemu, the cross sysroot for a foreign one).
ld_prefix = ENV['ALETHEIA_LD_PREFIX'] || sysroot || runtime_prefix
qenv = { 'QEMU_LD_PREFIX' => ld_prefix, 'ALETHEIA_STUB_OUT' => stub_out }
qpid = spawn(qenv, q['bin'], '-g', port.to_s, stub, @target,
in: slave, out: slave, err: log, pgroup: true)
sleep 0.8 # let the gdbstub come up (don't pre-connect: it accepts one client)
genv = { 'ALETHEIA_PLAN' => plan_path, 'ALETHEIA_STUB_OUT' => stub_out,
'ALETHEIA_CONNECT' => "localhost:#{port}", 'ALETHEIA_SYSROOT' => ld_prefix }
gpid = spawn(genv, 'gdb-multiarch', '-nx', '-q', '-batch', '-x', driver, stub,
out: log, err: log, pgroup: true)
[gpid, qpid]
end
def free_port
s = TCPServer.new('127.0.0.1', 0)
port = s.addr[1]
s.close
port
end
end
# Self-injecting: plain qemu-user with no gdbstub. The stub applies the plan
# (passed as text in $ALETHEIA_SELFINJECT) and jumps to the gadget itself, so
# the whole run stays under plain qemu-user. Without gdb there is no L0 signal,
# so a gadget is judged purely on L2 (PASS) or its absence.
#
# Runs qemu with +-strace+ so its syscall log lands in +log+ (the tty stays
# clean): it lets the oracle see when qemu can't emulate a syscall the gadget
# needs and report SKIP instead of FAIL.
#
# @example A limitation and its workaround
# glibc >= 2.34 posix_spawn forks via clone3, which qemu-arm doesn't
# implement ("Unknown syscall 435"). +ALETHEIA_CLONE3_HACK+ redirects the
# libc's __clone3 to legacy clone (see park_stub.c patch_clone3), so these
# spawn and L2-verify; without it they SKIP on syscall 435.
class SelfInject < Base
def launch(plan_path:, stub_out:, slave:, log:)
q = @arch.qemu
ld_prefix = ENV['ALETHEIA_LD_PREFIX'] || sysroot || q['ld_prefix']
env = { 'QEMU_LD_PREFIX' => ld_prefix, 'ALETHEIA_STUB_OUT' => stub_out,
'ALETHEIA_SELFINJECT' => plan_text(JSON.parse(File.read(plan_path))),
# TEMPORARY: redirect glibc's clone3 to legacy clone so posix_spawn
# can fork under qemu-arm (which lacks clone3). No-op if the stub's
# signature check doesn't match. See park_stub.c patch_clone3.
'ALETHEIA_CLONE3_HACK' => '1' }
[spawn(env, q['bin'], '-strace', stub, @target, in: slave, out: slave, err: log, pgroup: true)]
end
# Render the JSON plan as the stub's line grammar (see park_stub.c). Offsets
# are emitted as 32-bit two's-complement so a negative scratch_off survives.
def plan_text(plan)
lines = ["default #{default_fill(plan)}"]
(plan['regs'] || {}).each do |name, val|
# The stub addresses registers by number, so a role name has to be
# resolved to one first (arm's +fp+ is +r11+). Dropping a register the
# plan asked for would run the gadget without a value it requires and
# report the resulting miss as the gadget's fault, so this raises.
num = @arch.normalize_reg(name)[/\d+/]
raise ArgumentError, "plan sets #{name}, which the stub cannot address" if num.nil?
lines << reg_line(num, val)
end
(plan['mem'] || {}).each { |off, val| lines << mem_line('mem', off, val) }
(plan['base_mem'] || {}).each { |off, val| lines << mem_line('bmem', off, val) }
lines << "sp #{hex(plan['sp_offset'] || 0x2000)}"
lines << "pc #{hex(Integer(plan['offset']))}"
lines << 'thumb 1' if plan.dig('arch', 'thumb')
"#{lines.join("\n")}\n"
end
def default_fill(plan)
return 'poison' if plan['poison_default']
return 'null' if plan['null_default']
'benign'
end
def reg_line(num, val)
return "reg #{num} l #{hex(val)}" unless val.is_a?(Hash)
return "reg #{num} s #{hex(val['scratch_off'])}" if val.key?('scratch_off')
return "reg #{num} n #{hex(val['neg_base_off'])}" if val.key?('neg_base_off')
"reg #{num} b #{hex(val['base_off'])}"
end
def hex(val) = format('0x%x', val & 0xffffffff)
# A memory write the satisfier needs applied before the jump, into scratch
# (+mem+) or a libc global (+bmem+): either a scratch pointer, so a chained
# dereference finds a real pointer (see Satisfier#apply_deep_null), or the
# literal a value comparison comes down to.
def mem_line(directive, off, val)
kind = val.is_a?(Hash) ? "s #{hex(val['scratch_off'])}" : "l #{hex(val)}"
"#{directive} #{hex(Integer(off))} #{kind}"
end
end
end
end
+341
View File
@@ -0,0 +1,341 @@
/*
* park_stub — load a target libc and park, so a debugger can hijack a fully
* initialized thread to test a one_gadget candidate. Works both natively and
* under qemu-user (cross-arch), because it is self-describing: it pre-allocates
* scratch and reports its own libc base, so the driver needs no inferior
* function calls and no /proc access from the (possibly remote) debugger.
*
* Usage: ALETHEIA_STUB_OUT=<file> park_stub <path-to-target-libc.so>
* - mmaps a zeroed scratch region (no driver-side inferior mmap needed),
* - dlopen()s the target and finds its load base from the *guest*
* /proc/self/maps (correct under qemu-user),
* - writes "ALETHEIA_BASE=..\nALETHEIA_SCRATCH=.." to $ALETHEIA_STUB_OUT,
* - parks in aletheia_park() (break there to inject state).
*
* Self-injection mode ($ALETHEIA_SELFINJECT set): instead of parking for a
* debugger, the stub applies the plan itself (set registers/sp, seed the L2
* command) and jumps to the gadget. This runs the whole test under plain
* qemu-user with no gdbstub -- needed where qemu's gdbstub mishandles the
* fork'd child of a posix_spawn gadget (arm), killing the L2 shell. The plan
* text is passed in the env var; see self_inject() for its grammar.
*
* Build (per arch, ahead of time):
* cc -O0 -g -o park_stub_aarch64 park_stub.c -ldl
* x86_64-linux-gnu-gcc -O0 -g -o park_stub_x86_64 park_stub.c -ldl
*/
#define _GNU_SOURCE
#include <dlfcn.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
#include <sys/mman.h>
#define SCRATCH_SIZE 0x20000 /* keep in sync with Satisfier::SCRATCH_SIZE */
#define STRING_POOL 0x100 /* benign default: a readable, zero-filled scratch slot */
#define COMMAND_POOL 0x200 /* where the L2 "ls /" command is seeded (cf. satisfier) */
/* Break here to inject: libc is fully loaded and scratch is mapped. */
void aletheia_park(void) {
for (;;) {
pause();
}
}
#ifdef __arm__
/* --- TEMPORARY HACK: clone3 -> clone for qemu-arm -----------------------------
* qemu-arm doesn't implement clone3 (EABI 435), which glibc 2.43's posix_spawn
* forks with, so posix_spawn gadgets can't spawn a shell under emulation. This
* redirects the target libc's __clone3 wrapper -- which the loader calls as
* __clone3(struct clone_args *a, size_t size, int (*fn)(void*), void *arg)
* -- to a shim that translates to the legacy clone (syscall 120, which qemu-arm
* does implement) via glibc's own __clone. Gated on $ALETHEIA_CLONE3_HACK and a
* byte-signature match, so it only fires where expected. Remove once qemu-arm
* gains 32-bit clone3. */
struct clone_args_min { /* prefix of the kernel struct clone_args (all u64) */
unsigned long long flags, pidfd, child_tid, parent_tid, exit_signal,
stack, stack_size, tls;
};
extern int __clone(int (*fn)(void *), void *stack, int flags, void *arg,
void *ptid, void *tls, void *ctid);
__attribute__((used)) static int
shim_clone3(struct clone_args_min *a, unsigned long size,
int (*fn)(void *), void *arg) {
(void)size;
int flags = (int)(a->flags | a->exit_signal);
void *stack_top = (void *)(unsigned long)(a->stack + a->stack_size);
return __clone(fn, stack_top, flags, arg,
(void *)(unsigned long)a->parent_tid,
(void *)(unsigned long)a->tls,
(void *)(unsigned long)a->child_tid);
}
/* Encode `movw Rd,#lo16 ; movt Rd,#hi16` (Thumb-2 T3/T1) into 8 bytes, loading
* the full 32-bit +val+ into register +rd+. */
static void emit_movw_movt(unsigned char *p, int rd, unsigned long val) {
for (int hi = 0; hi < 2; hi++) {
unsigned int imm16 = (val >> (hi * 16)) & 0xffff;
unsigned int i = (imm16 >> 11) & 1, imm4 = (imm16 >> 12) & 0xf;
unsigned int imm3 = (imm16 >> 8) & 0x7, imm8 = imm16 & 0xff;
unsigned int hw1 = 0xf240 | (hi ? 0x80 : 0) | (i << 10) | imm4;
unsigned int hw2 = (imm3 << 12) | (rd << 8) | imm8;
p[hi * 4 + 0] = hw1 & 0xff; p[hi * 4 + 1] = (hw1 >> 8) & 0xff;
p[hi * 4 + 2] = hw2 & 0xff; p[hi * 4 + 3] = (hw2 >> 8) & 0xff;
}
}
/* End address of the mapping that starts at +base+ in /proc/self/maps, or 0.
* The target libc's first LOAD (the R E text) starts at +base+, so this bounds
* the region to scan for a code signature. */
static unsigned long region_end(unsigned long base) {
FILE *f = fopen("/proc/self/maps", "r");
char line[1024];
unsigned long end = 0;
while (f && fgets(line, sizeof line, f)) {
unsigned long s, e;
if (sscanf(line, "%lx-%lx", &s, &e) == 2 && s == base) { end = e; break; }
}
if (f) fclose(f);
return end;
}
/* Locate the +__clone3+ syscall site by scanning the *loaded* target libc (from
* +base+, the mapping posix_spawn actually calls into -- correct whether the
* fixture is the primary libc or a dlopen'd secondary) for its unique byte
* signature. @return the base-relative offset of the site, or -1. */
static long find_clone3_site(unsigned long base, const unsigned char *sig, size_t siglen) {
unsigned long end = region_end(base);
if (!end) return -1;
for (unsigned long p = base; p + siglen <= end; p++) {
if (memcmp((const void *)p, sig, siglen) == 0) return (long)(p - base);
}
return -1;
}
/* Redirect the libc's __clone3 to shim_clone3 (an absolute Thumb branch via
* movw/movt/bx). Returns 1 if the patch was applied. */
static int patch_clone3(unsigned long base) {
/* push {r7}; movw r7,#435; svc 0 -- the wrapper's syscall site, little-endian */
static const unsigned char sig[] = {0x80, 0xb4, 0x40, 0xf2, 0xb3, 0x17, 0x00, 0xdf};
long off = find_clone3_site(base, sig, sizeof sig);
if (off < 0) {
fprintf(stderr, "aletheia: clone3 hack signature not found; not applied\n");
return 0;
}
unsigned char *site = (unsigned char *)(base + off);
unsigned long page = (unsigned long)site & ~0xfffUL;
if (mprotect((void *)page, 0x2000, PROT_READ | PROT_WRITE | PROT_EXEC) != 0) {
fprintf(stderr, "aletheia: clone3 hack mprotect failed\n");
return 0;
}
unsigned long tgt = (unsigned long)&shim_clone3; /* Thumb bit already set */
unsigned char patch[10];
emit_movw_movt(patch, 12, tgt); /* movw ip; movt ip */
patch[8] = 0x60; patch[9] = 0x47; /* bx ip */
memcpy(site, patch, sizeof patch);
__builtin___clear_cache((char *)site, (char *)site + sizeof patch);
fprintf(stderr, "aletheia: clone3->clone hack applied at %p\n", (void *)site);
return 1;
}
/* Register file to load before jumping to the gadget (r0..r12, sp, pc). */
struct inj { unsigned int r[13]; unsigned int sp; unsigned int pc; };
/* Load the register file and branch to g->pc; bit0 of pc selects Thumb/ARM.
* g is read through an absolute pointer, so moving sp first is safe. */
__attribute__((noreturn)) static void jump_inj(struct inj *g) {
__asm__ volatile(
"mov r3, %0\n"
"ldr r0, [r3, #52]\n" /* r0 = g->sp */
"mov sp, r0\n"
"ldr lr, [r3, #56]\n" /* lr = g->pc (target, Thumb bit set by caller) */
"ldr r0, [r3, #0]\n"
"ldr r1, [r3, #4]\n"
"ldr r2, [r3, #8]\n"
"ldr r4, [r3, #16]\n"
"ldr r5, [r3, #20]\n"
"ldr r6, [r3, #24]\n"
"ldr r7, [r3, #28]\n"
"ldr r8, [r3, #32]\n"
"ldr r9, [r3, #36]\n"
"ldr r10,[r3, #40]\n"
"ldr r11,[r3, #44]\n"
"ldr r12,[r3, #48]\n"
"ldr r3, [r3, #12]\n" /* r3 last: it held the pointer */
"bx lr\n"
:: "r"(g) : "memory");
__builtin_unreachable();
}
/* Apply the plan and jump. Plan grammar (one directive per line):
* default benign|poison|null fill for registers the plan doesn't set
* reg <n> s|l|b|n <hex> r<n> = scratch+hex (s) | literal (l) | base+hex (b)
* | -(base+hex) (n), the value that makes the gadget's
* own `add r<n>, pc` come out zero
* mem <hex-off> s|l <hex> *(scratch+off) = scratch+val (s) | literal (l)
* bmem <hex-off> s|l <hex> *(base+off) = scratch+val (s) | literal (l),
* for a constraint on a libc global
* sp <hex> sp = scratch + hex
* pc <hex> pc = base + hex
* thumb 1 enter the gadget in Thumb state
* Offsets are 32-bit two's-complement (a scratch_off may be negative). */
__attribute__((noreturn))
static void self_inject(unsigned long base, unsigned char *scratch, const char *plan) {
struct inj g;
unsigned int rv[13];
char rset[13] = {0};
unsigned long fill = (unsigned long)scratch + STRING_POOL;
unsigned int sp = 0, pc = 0;
unsigned long off;
int thumb = 0, i;
memcpy(scratch + COMMAND_POOL, "ls /", 5); /* the L2 command the gadget runs */
if (getenv("ALETHEIA_CLONE3_HACK")) patch_clone3(base);
char *buf = strdup(plan);
for (char *line = strtok(buf, "\n"); line; line = strtok(NULL, "\n")) {
unsigned int n;
char kind;
unsigned long v;
if (sscanf(line, "reg %u %c %lx", &n, &kind, &v) == 3 && n < 13) {
rv[n] = (unsigned int)(kind == 's' ? (unsigned long)scratch + v
: kind == 'b' ? base + v
: kind == 'n' ? -(base + v)
: v);
rset[n] = 1;
} else if (sscanf(line, "mem %lx %c %lx", &off, &kind, &v) == 3) {
/* A chained dereference (e.g. [[sp]]==NULL) needs a real pointer at
* scratch+off, not just the zero-fill a single dereference relies on;
* a value comparison instead needs the literal it is compared against. */
*(unsigned int *)(scratch + off) =
(unsigned int)(kind == 's' ? (unsigned long)scratch + v : v);
} else if (sscanf(line, "bmem %lx %c %lx", &off, &kind, &v) == 3) {
*(unsigned int *)(base + off) =
(unsigned int)(kind == 's' ? (unsigned long)scratch + v : v);
} else if (sscanf(line, "sp %lx", &v) == 1) {
sp = (unsigned int)((unsigned long)scratch + v);
} else if (sscanf(line, "pc %lx", &v) == 1) {
pc = (unsigned int)(base + v);
} else if (strncmp(line, "default poison", 14) == 0) {
fill = 0xDEAD0000;
} else if (strncmp(line, "default null", 12) == 0) {
fill = 0;
} else if (strncmp(line, "thumb 1", 7) == 0) {
thumb = 1;
}
}
free(buf);
for (i = 0; i < 13; i++) g.r[i] = rset[i] ? rv[i] : (unsigned int)fill;
g.sp = sp;
g.pc = thumb ? (pc | 1) : pc;
jump_inj(&g);
}
#endif /* __arm__ */
/* Load base of the first mapping whose file basename starts with +name+, or 0.
* When +path_out+ is non-NULL it receives that mapping's full file path. */
static unsigned long map_base_path(const char *name, char *path_out, size_t path_sz) {
FILE *f = fopen("/proc/self/maps", "r");
char line[1024];
unsigned long base = 0;
while (f && fgets(line, sizeof line, f)) {
char *slash = strrchr(line, '/');
if (slash && strncmp(slash + 1, name, strlen(name)) == 0) {
base = strtoul(line, NULL, 16);
if (path_out) {
char *p = strchr(line, '/');
size_t n = strcspn(p, "\n");
if (n < path_sz) { memcpy(path_out, p, n); path_out[n] = 0; }
else if (path_sz) path_out[0] = 0;
}
break;
}
}
if (f) fclose(f);
return base;
}
static unsigned long map_base(const char *name) {
return map_base_path(name, NULL, 0);
}
/* Whether two files have identical contents (used to confirm the target IS the
* already-loaded libc). */
static int files_identical(const char *a, const char *b) {
FILE *fa = fopen(a, "rb"), *fb = fopen(b, "rb");
int same = fa && fb;
char ba[65536], bb[65536];
size_t na, nb;
while (same) {
na = fread(ba, 1, sizeof ba, fa);
nb = fread(bb, 1, sizeof bb, fb);
if (na != nb || memcmp(ba, bb, na) != 0) { same = 0; break; }
if (na == 0) break;
}
if (fa) fclose(fa);
if (fb) fclose(fb);
return same;
}
int main(int argc, char **argv) {
if (argc < 2) {
fprintf(stderr, "usage: %s <target-libc.so>\n", argv[0]);
return 2;
}
void *scratch = mmap(NULL, SCRATCH_SIZE, PROT_READ | PROT_WRITE,
MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
if (scratch == MAP_FAILED) {
fprintf(stderr, "mmap failed\n");
return 1;
}
/* dlopen the target to map it at a known base. This can fail when the target
* is a full libc.so.6 that imports an ld.so-private symbol coupled only to
* the PRIMARY libc (e.g. glibc >= 2.35's __nptl_change_stack_perm) -- such a
* symbol can't be resolved for a dlopen'd SECONDARY libc. But a version-matched
* sysroot links this stub against a libc byte-identical to the target, so the
* target is ALREADY mapped as our primary libc; when its file matches the
* loaded libc.so.6, fall back to that mapping instead of erroring. */
char loaded[1024] = "";
unsigned long libc_base = map_base_path("libc.so.6", loaded, sizeof loaded);
void *h = dlopen(argv[1], RTLD_NOW | RTLD_LOCAL);
if (!h && !(loaded[0] && files_identical(argv[1], loaded))) {
fprintf(stderr, "dlopen failed: %s\n", dlerror());
return 1;
}
/* The target's own mapping, or the loaded libc when the target == it (dlopen
* deduped, or we fell back above). */
const char *bn = strrchr(argv[1], '/');
bn = bn ? bn + 1 : argv[1];
unsigned long base = map_base(bn);
if (!base) base = libc_base ? libc_base : map_base("libc.so.6");
const char *outpath = getenv("ALETHEIA_STUB_OUT");
if (outpath) {
FILE *out = fopen(outpath, "w");
if (out) {
fprintf(out, "ALETHEIA_BASE=0x%lx\nALETHEIA_SCRATCH=%p\n", base, scratch);
fclose(out);
}
}
const char *plan = getenv("ALETHEIA_SELFINJECT");
if (plan && *plan) {
#ifdef __arm__
self_inject(base, (unsigned char *)scratch, plan); /* noreturn */
#else
fprintf(stderr, "self-inject not supported on this arch\n");
return 2;
#endif
}
aletheia_park();
return 0;
}
+480
View File
@@ -0,0 +1,480 @@
# frozen_string_literal: true
$LOAD_PATH.unshift(File.expand_path('../lib', __dir__))
require 'aletheia/arch/aarch64'
require 'aletheia/satisfier'
# gdb-free unit tests for the constraint satisfier: they assert the plan it emits
# (register/memory assignments and chosen disjunction branch) for representative
# constraints of each category.
# The three things the satisfier reads off a gadget. A struct rather than the real
# one: these constraint lists are what is under test, and building them through
# one_gadget would let its own pruning rewrite them first.
StubGadget = Struct.new(:offset, :effect, :constraints, keyword_init: true)
RSpec.describe Aletheia::Satisfier do
subject(:satisfier) { described_class.new(Aletheia::Arch::AArch64) }
def gadget(constraints, offset: 0x1000, effect: 'execve("/bin/sh", x0, environ)')
StubGadget.new(offset: offset, effect: effect, constraints: constraints)
end
it 'sets a bare register to zero for "reg == NULL"' do
plan = satisfier.satisfy(gadget(['x1 == NULL']))
expect(plan.status).to eq('ok')
expect(plan.regs['x1']).to eq(0)
expect(plan.branches['c0']).to eq('x1 == NULL')
end
it 'satisfies a stack-relative dereference-NULL for free (no register set)' do
plan = satisfier.satisfy(gadget(['[sp+0x50] == NULL']))
expect(plan.status).to eq('ok')
expect(plan.regs).to be_empty
end
it 'rejects the unsatisfiable "sp+imm == NULL" branch and takes the deref branch' do
plan = satisfier.satisfy(gadget(['sp+0x218 == NULL || (u16)[sp+0x218] == NULL']))
expect(plan.status).to eq('ok')
expect(plan.branches['c0']).to eq('(u16)[sp+0x218] == NULL')
end
it 'points a register into scratch to satisfy "writable: reg+imm"' do
plan = satisfier.satisfy(gadget(['writable: x19+0x258']))
expect(plan.status).to eq('ok')
off = plan.regs['x19']['scratch_off']
expect(off + 0x258).to eq(Aletheia::Satisfier::WRITABLE_BASE)
end
it 'gives distinct scratch write-areas to multiple writable constraints' do
plan = satisfier.satisfy(gadget(['writable: x19+0x258', 'writable: x20+0x4']))
a = plan.regs['x19']['scratch_off'] + 0x258
b = plan.regs['x20']['scratch_off'] + 0x4
expect(a).not_to eq(b)
end
it 'prefers the cheap NULL branch over building a valid argv' do
plan = satisfier.satisfy(gadget(['x4 == NULL || {x4, x3, x23, NULL} is a valid argv']))
expect(plan.regs['x4']).to eq(0)
expect(plan.branches['c0']).to eq('x4 == NULL')
end
it 'ends the array after argv[0], the shape a shell can be driven from' do
# Giving x3 a string too would make the shell read it as a script name and
# exit; {<str>, NULL} leaves it reading stdin. Verified against a real
# /bin/sh -- see the shape table on #apply_argv_list.
plan = satisfier.satisfy(gadget(['{x4, x3, x23, NULL} is a valid argv']))
expect(plan.regs['x4']).to eq('scratch_off' => Aletheia::Satisfier::STRING_POOL)
expect(plan.regs['x3']).to eq(0)
expect(plan.regs).not_to have_key('x23')
end
it 'gives the command slot of a "-c" array the command, not a terminator' do
plan = satisfier.satisfy(gadget(['{"sh", "-c", x23, NULL} is a valid argv']))
expect(plan.regs['x23']).to eq('scratch_off' => Aletheia::Satisfier::COMMAND_POOL)
end
it 'terminates after a fixed argv[0] the gadget supplies' do
plan = satisfier.satisfy(gadget(['{"/bin/sh", x0, NULL} is a valid argv']))
expect(plan.regs['x0']).to eq(0)
end
it 'sets a register to the immediate for a "reg == imm" branch condition' do
plan = satisfier.satisfy(gadget(['x2 == 0x1']))
expect(plan.status).to eq('ok')
expect(plan.regs['x2']).to eq(1)
end
it 'normalises a 32-bit view (w21) to its 64-bit register' do
plan = satisfier.satisfy(gadget(['w21 == 0x1']))
expect(plan.regs['x21']).to eq(1)
end
it 'treats a scratch pointer as already satisfying "!= 0"' do
plan = satisfier.satisfy(gadget(['writable: x0', 'x0 != 0']))
expect(plan.status).to eq('ok')
expect(plan.regs['x0']).to be_a(Hash) # points into scratch, hence nonzero
end
it 'builds a valid argv by pointing register elements at scratch, -c at the command pool' do
plan = satisfier.satisfy(gadget(['{"sh", "-c", x23, NULL} is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.regs['x23']).to eq('scratch_off' => Aletheia::Satisfier::COMMAND_POOL)
end
it 'points the first register operand after -c at the command pool, past a "--" separator' do
# `$base+0x100` here stands in for the libc "--" constant; the real command is
# the next operand register (x21), which `sh -c -- <x21>` runs.
plan = satisfier.satisfy(gadget(['{"sh", "-c", $base+0x100, x21, NULL} is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.regs['x21']).to eq('scratch_off' => Aletheia::Satisfier::COMMAND_POOL)
end
describe 'masks one_gadget could not fold' do
it 'gives a register a value whose masked bits meet the target' do
plan = satisfier.satisfy(gadget(['(x1 & 0xf000) == 0x2000']))
expect(plan.status).to eq('ok')
expect(plan.regs['x1']).to eq(0x2000)
end
it 'refuses a target the mask can never produce' do
# 0x1 lies outside the mask, so no value of x1 makes the masked read 0x1.
plan = satisfier.satisfy(gadget(['(x1 & 0xf000) == 0x1']))
expect(plan.status).to eq('skip')
end
it 'flips the masked bits for an inequality' do
plan = satisfier.satisfy(gadget(['(x2 & 0x10) != 0x0']))
expect(plan.status).to eq('ok')
expect(plan.regs['x2']).to eq(0x10)
end
it 'writes the value where the mask reads through a pointer' do
plan = satisfier.satisfy(gadget(['([sp+0x40] & 0x10) != 0x0']))
expect(plan.status).to eq('ok')
expect(plan.mem[Aletheia::Satisfier::SP_OFFSET + 0x40]).to eq(0x10)
end
it 'points a register rounded down for alignment at a scratch slot' do
# the gadget writes through (x3 & ~0xf); a scratch slot is 16-aligned, so
# the rounding leaves it untouched and the slot is the address written.
plan = satisfier.satisfy(gadget(['writable: (x3 & 0xfffffffffffffff0)']))
expect(plan.status).to eq('ok')
expect(plan.regs['x3']['scratch_off'] % 0x10).to eq(0)
end
it 'reads a 32-bit alignment mask as an alignment, not a field' do
# i386 renders the same rounding as 0xfffffff0; complementing that over 64
# bits would make it look like a field selector and skip the gadget.
plan = satisfier.satisfy(gadget(['writable: (x3 & 0xfffffff0)']))
expect(plan.status).to eq('ok')
expect(plan.regs['x3']['scratch_off'] % 0x10).to eq(0)
end
it 'reads a rounded pointer inside a larger expression as that pointer' do
# the whole disjunction is about the address x3 rounds to, so every mention
# of it resolves to x3 -- and the scratch it is pointed at is zeroed, which
# already satisfies the cheapest branch.
plan = satisfier.satisfy(gadget(['writable: (x3 & 0xfffffffffffffff0)',
'[(x3 & 0xfffffffffffffff0)] == NULL || ' \
'(x3 & 0xfffffffffffffff0) is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.regs['x3']).to be_a(Hash)
end
it 'refuses an alignment coarser than a scratch slot guarantees' do
# page alignment: WRITABLE_STRIDE is 0x800, so slots are not all 0x1000-aligned.
plan = satisfier.satisfy(gadget(['writable: (x3 & 0xfffffffffffff000)']))
expect(plan.status).to eq('skip')
end
end
it 'lets a register another constraint pins to NULL terminate the argv' do
# x3 is __sigaction's oldact -- it has to be NULL, and NULL is exactly what
# ends an argv, so the array is `sh -c <x6>` rather than unsatisfiable.
plan = satisfier.satisfy(gadget(['x3 == NULL', '{"sh", "-c", x6, x3, NULL} is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.regs['x3']).to eq(0)
expect(plan.regs['x6']).to eq('scratch_off' => Aletheia::Satisfier::COMMAND_POOL)
end
it 'builds no element past the argv terminator' do
plan = satisfier.satisfy(gadget(['{"sh", "-c", x6, NULL, x21} is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.regs['x6']).to eq('scratch_off' => Aletheia::Satisfier::COMMAND_POOL)
expect(plan.regs).not_to have_key('x21')
end
it 'zeroes memory for a single-deref "[reg] == NULL" by pointing the register at scratch' do
plan = satisfier.satisfy(gadget(['[x0] == NULL']))
expect(plan.status).to eq('ok')
expect(plan.regs['x0']).to eq('scratch_off' => Aletheia::Satisfier::STRING_POOL)
end
it 'restores and retries when the cheapest branch genuinely conflicts' do
# writable: x0 pins x0 to a (nonzero) scratch address; "x0 == NULL" would need
# x0 = 0 -- a conflict -- so the satisfier restores and takes "x0 is a valid argv".
plan = satisfier.satisfy(gadget(['writable: x0', 'x0 == NULL || x0 is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.branches['c1']).to eq('x0 is a valid argv')
end
it 'lets a writable slot also satisfy a "[reg] == NULL" on that same slot' do
# writable: x0 points x0 at zeroed scratch, so the deref [x0] already reads
# NULL -- the cheapest argv branch holds without re-assigning (and conflicting on) x0.
plan = satisfier.satisfy(gadget(['writable: x0', '[x0] == NULL || x0 == NULL || x0 is a valid argv']))
expect(plan.status).to eq('ok')
expect(plan.branches['c1']).to eq('[x0] == NULL')
expect(plan.regs['x0']).to be_a(Hash) # still the single writable scratch pointer
end
it 'SKIPs (does not crash) on an unparseable operand' do
# Deeper than the one modelled level of nesting (see Operand#inner_imm).
plan = satisfier.satisfy(gadget(['(s32)[[[sp+0x30]+0x4]+0x8] <= 0']))
expect(plan.status).to eq('skip')
end
it 'points a pointer read from memory at scratch, for a field read off it' do
plan = satisfier.satisfy(gadget(['(s32)[[sp+0x30]+0x4] <= 0']))
expect(plan.status).to eq('ok')
# [sp+0x30] holds a scratch pointer, so the field at +0x4 reads the zero fill.
expect(plan.mem[Aletheia::Satisfier::SP_OFFSET + 0x30]).to have_key('scratch_off')
end
it 'defaults to benign fill, and to poison fill in strict mode' do
expect(satisfier.satisfy(gadget(['x1 == NULL'])).benign_default).to be(true)
strict = described_class.new(Aletheia::Arch::AArch64, strict: true)
plan = strict.satisfy(gadget(['x1 == NULL']))
expect(plan.poison_default).to be(true)
expect(plan.benign_default).to be(false)
end
# A nested readable (aarch64-2.27 0xa3228) states the readability of its own
# base: reading the pointer AT x19+0xed8 requires that address readable. One
# gadget lists no shallower constraint saying so, so the satisfier has to give
# x19 somewhere to point before it can place the pointer.
it 'establishes its own base for "readable: [reg+imm]"' do
plan = satisfier.satisfy(gadget(['readable: [x19+0xed8]']))
expect(plan.status).to eq('ok')
pool = Aletheia::Satisfier::STRING_POOL
expect(plan.regs['x19']).to eq('scratch_off' => pool)
expect(plan.mem[pool + 0xed8]).to eq('scratch_off' => pool)
end
context 'amd64 backend' do
require 'aletheia/arch/amd64'
subject(:satisfier) { described_class.new(Aletheia::Arch::Amd64) }
def gadget(constraints, offset: 0x1000, effect: 'execve("/bin/sh", rsi, environ)')
StubGadget.new(offset: offset, effect: effect, constraints: constraints)
end
it 'satisfies a bare stack-alignment "rsp & 0xf == 0" by construction (no register set)' do
plan = satisfier.satisfy(gadget(['rsp & 0xf == 0']))
expect(plan.status).to eq('ok')
expect(plan.regs).to be_empty
expect(plan.branches['c0']).to eq('rsp & 0xf == 0')
end
it 'aligns a GPR by pointing it at an aligned scratch slot for "reg & 0xf == 0"' do
plan = satisfier.satisfy(gadget(['rbx & 0xf == 0']))
expect(plan.status).to eq('ok')
expect(plan.regs['rbx']).to eq('scratch_off' => Aletheia::Satisfier::STRING_POOL)
end
# A branch condition on a libc global, e.g. libc-2.19 0xe654d's
# `(s64)[$base+0x3c3e88] <= 0`: the driver writes 0 to base+off rather than the
# satisfier pinning a register (a $base address isn't settable).
it 'zeroes a libc global for "(s64)[$base+off] <= 0"' do
plan = satisfier.satisfy(gadget(['(s64)[$base+0x3c3e88] <= 0x0']))
expect(plan.status).to eq('ok')
expect(plan.base_mem[0x3c3e88]).to eq(0)
expect(plan.regs).to be_empty # $base is not pinned as a register
end
it 'normalises a 32-bit view (eax) to its 64-bit register (rax)' do
plan = satisfier.satisfy(gadget(['eax == 0']))
expect(plan.regs['rax']).to eq(0)
end
it 'points a register at zeroed scratch for a dereferenced "[reg] == 0"' do
plan = satisfier.satisfy(gadget(['[rbx] == 0']))
expect(plan.status).to eq('ok')
expect(plan.regs['rbx']).to eq('scratch_off' => Aletheia::Satisfier::STRING_POOL)
end
# "readable: reg" (a libc call dereferences reg, e.g. libc-2.31 0x51df8's
# posix_spawnattr_setsigmask/setsigdefault reading r12/r13): point the register
# at readable scratch, like the bare-pointer argv/envp form.
it 'points a register at readable scratch for "readable: reg"' do
plan = satisfier.satisfy(gadget(['readable: r12']))
expect(plan.status).to eq('ok')
expect(plan.regs['r12']).to eq('scratch_off' => Aletheia::Satisfier::STRING_POOL)
end
# A "writable: reg" and a "reg != 0" on the SAME register must not conflict
# (libc-2.19 0xc1ca7 builds argv in place at rax and also branches on rax != 0):
# the writable pins rax to a scratch pointer, which -- applied first -- already
# satisfies the != 0. Applying the relation first would pin rax to a bare 1 and
# leave the writable unsatisfiable.
it 'satisfies "writable: reg" and "reg != 0" together by pinning the pointer' do
plan = satisfier.satisfy(gadget(['rax != 0x0', 'writable: rax+0x8']))
expect(plan.status).to eq('ok')
expect(plan.regs['rax']).to be_a(Hash) # a scratch pointer, not the literal 1
end
# libc-2.23's 0xcc610 reads a mode flag off the stack (`mov esi,[rbp-0x50]`,
# never overwritten within the window) that a later branch requires to be
# exactly 1 -- unlike a zero target, there's no pre-zeroed region to point
# at, so this needs rbp pinned to a *fresh* scratch slot (rbp is otherwise
# unconstrained by this gadget) with the literal actually written there.
it 'pins an unconstrained register and writes a nonzero literal for "[reg+imm] == <imm>"' do
plan = satisfier.satisfy(gadget(['[rbp-0x50] == 0x1']))
expect(plan.status).to eq('ok')
rbp_off = plan.regs['rbp']['scratch_off']
expect(plan.mem[rbp_off - 0x50]).to eq(1)
end
# A "writable: [base]+imm" compound base (base is dereferenced, not a bare
# register -- a store through a pointer read off the stack, e.g. libc-2.27's
# 0xe5887) can't be resolved until `base`'s own argv/envp constraint has run,
# and that constraint must not pick base == NULL: with base == NULL,
# "[base]+imm" is a fixed low address (a real unmapped-page write), not
# merely untracked. The deferred pass (order_compound_writable_last) plus the
# NULL-branch block (@null_unsafe_bases) together force "[rbp-0x78] is a
# valid argv" instead of the cheaper "[rbp-0x78] == NULL".
it 'defers a compound "writable: [base]+imm" until base resolves to a real pointer' do
plan = satisfier.satisfy(gadget([
'writable: [rbp-0x78]+0x10',
'writable: rbp-0x80',
'[[rbp-0x78]] == NULL || [rbp-0x78] == NULL || [rbp-0x78] is a valid argv',
'[[rbp-0x70]] == NULL || [rbp-0x70] == NULL || [rbp-0x70] is a valid envp'
], effect: 'execve("/bin/sh", [rbp-0x78], [rbp-0x70])'))
expect(plan.status).to eq('ok')
expect(plan.branches.values).to include('[rbp-0x78] is a valid argv')
expect(plan.branches.values).not_to include('[rbp-0x78] == NULL')
rbp_off = plan.regs['rbp']['scratch_off']
expect(plan.mem[rbp_off - 0x78]).to eq('scratch_off' => Aletheia::Satisfier::STRING_POOL)
end
end
# arm-2.27's 0x2d358 window runs `add r1, pc` and then stores through the sum,
# so one_gadget names the store target `(r1 + $base+0x2d364)`: a fixed libc
# address whose landing place only r1 decides. There is no pointer to hand out
# -- r1 has to carry the literal that puts the sum in libc's own spare
# writable data.
context 'a store through a register added to a fixed libc address' do
require 'aletheia/arch/arm'
subject(:satisfier) { described_class.new(Aletheia::Arch::Arm, spare_writable: spare) }
let(:spare) { 0xf7590...0xf8000 }
def gadget(constraints, offset: 0x2d358, effect: 'execve("/bin/sh", sp+0x20, environ)')
StubGadget.new(offset: offset, effect: effect, constraints: constraints)
end
it 'pins the register so the sum lands in the spare writable data' do
plan = satisfier.satisfy(gadget(['writable: (r1 + $base+0x2d364)']))
expect(plan.status).to eq('ok')
expect(spare).to cover(plan.regs['r1'] + 0x2d364)
end
# The register carries the whole displacement, so a trailing one only shifts
# where inside its area the sum lands -- it stays in the spare region.
it 'folds a trailing displacement into the literal' do
plan = satisfier.satisfy(gadget(['writable: (r1 + $base+0x2d364)+0x8']))
expect(spare).to cover(plan.regs['r1'] + 0x2d364 + 0x8)
end
it 'gives distinct areas to two such stores' do
plan = satisfier.satisfy(gadget(['writable: (r1 + $base+0x100)', 'writable: (r2 + $base+0x200)']))
expect(plan.status).to eq('ok')
expect(plan.regs['r1'] + 0x100).not_to eq(plan.regs['r2'] + 0x200)
end
# Once the register is pinned the sum is a fixed libc address, so a read
# through it is an ordinary libc-global read -- and lands on the zero fill.
it 'reads zero through a dereference of the sum' do
plan = satisfier.satisfy(gadget(['[(r1 + $base+0x50558)+0x8] == 0x0', 'writable: (r1 + $base+0x50558)']))
expect(plan.status).to eq('ok')
slot = plan.regs['r1'] + 0x50558
expect(spare).to cover(slot)
expect(plan.base_mem[slot + 0x8]).to eq(0) # written where the read lands
end
# A chained read needs a real pointer at the first level, which the driver
# writes into the libc global the sum resolved to.
it 'stages a pointer in libc for a chained dereference of the sum' do
plan = satisfier.satisfy(gadget(['[[(r2 + $base+0x50492)+0xc]+0xa4] == 0x0',
'r6 == [[(r2 + $base+0x50492)+0xc]+0x38]',
'readable: (r2 + $base+0x50492)+0xc']))
expect(plan.status).to eq('ok')
slot = plan.regs['r2'] + 0x50492 + 0xc
expect(plan.base_mem[slot]).to have_key('scratch_off')
expect(plan.regs['r6']).to eq(0)
end
# Pinning a register a rejected branch asked for would hand a poisoned
# register a valid value, so an address-shaped sum inside a disjunction is
# refused rather than steered (see Satisfier#steer_base_sums).
it 'refuses to steer a sum that only one branch of a disjunction needs' do
plan = satisfier.satisfy(gadget(['r4 == NULL || writable: (r1 + $base+0x100)']))
expect(plan.status).to eq('skip')
end
it 'SKIPs when the libc has no spare writable room to steer the store into' do
plan = described_class.new(Aletheia::Arch::Arm).satisfy(gadget(['writable: (r1 + $base+0x2d364)']))
expect(plan.status).to eq('skip')
end
it 'SKIPs when the register is not one the plan can set' do
plan = satisfier.satisfy(gadget(['writable: (lr + $base+0x2c5ee)']))
expect(plan.status).to eq('skip')
end
# A sum required to be NULL cannot be steered anywhere -- only the negation
# of the libc address makes it vanish, and only the driver knows that value.
it 'names the value that cancels the libc address for a NULL requirement' do
plan = satisfier.satisfy(gadget(['(r2 + $base+0x47a68) == NULL']))
expect(plan.status).to eq('ok')
expect(plan.regs['r2']).to eq('neg_base_off' => 0x47a68)
end
# The same steering serves an argv element: the sum lands on the zero fill,
# which reads as the valid empty string argv[0] only has to be. arm-2.27's
# 0x2d35e shape, where the gadget supplies the "-c" and the command follows.
it 'places an argv[0] built the same way, and still seeds the command' do
plan = satisfier.satisfy(gadget(['{(ip + $base+0x2d36a), "-c", fp, r3, ...} is a valid argv']))
expect(plan.status).to eq('ok')
# Both are named by their AAPCS role in the constraint and assigned under
# the register that role denotes.
expect(spare).to cover(plan.regs['r12'] + 0x2d36a)
expect(plan.regs['r11']).to eq('scratch_off' => Aletheia::Satisfier::COMMAND_POOL)
end
# An element that has to end the array is NULL, so it takes the cancelling
# value too, where argv[0] before it is merely steered at a readable string.
it 'cancels the address for such an element where the array has to end' do
plan = satisfier.satisfy(gadget(['{(ip + $base+0x100), (r7 + $base+0x200), fp, r3, ...} is a valid argv']))
expect(plan.status).to eq('ok')
expect(spare).to cover(plan.regs['r12'] + 0x100)
expect(plan.regs['r7']).to eq('neg_base_off' => 0x200)
end
# Emptying the array and building it are different shapes, and which one
# yields an observable shell varies per gadget -- so where both are open the
# builder still wins, exactly as before the cancelling value existed.
it 'still builds the array when a NULL branch is also open' do
plan = satisfier.satisfy(gadget(['(ip + $base+0x2d36a) == NULL || ' \
'{(ip + $base+0x2d36a), "-c", fp, r3, ...} is a valid argv']))
expect(plan.branches['c0']).to start_with('{')
expect(spare).to cover(plan.regs['r12'] + 0x2d36a)
end
it 'refuses such an element on a register the plan cannot set' do
plan = satisfier.satisfy(gadget(['{(lr + $base+0x2c5fe), "-c", r6, r3, ...} is a valid argv']))
expect(plan.status).to eq('skip')
end
end
context 'i386 backend' do
require 'aletheia/arch/i386'
subject(:satisfier) { described_class.new(Aletheia::Arch::I386, got_offset: 0x1d5000) }
def gadget(constraints, offset: 0x1000, effect: 'execve("/bin/sh", esp+0x34, environ)')
StubGadget.new(offset: offset, effect: effect, constraints: constraints)
end
it 'sets the base register to the libc GOT (base + PLTGOT offset)' do
plan = satisfier.satisfy(gadget(['esi is the GOT address of libc']))
expect(plan.status).to eq('ok')
expect(plan.regs['esi']).to eq('base_off' => 0x1d5000)
end
it 'SKIPs the GOT constraint when the PLTGOT offset is unknown' do
plan = described_class.new(Aletheia::Arch::I386).satisfy(gadget(['esi is the GOT address of libc']))
expect(plan.status).to eq('skip')
end
end
end
+3
View File
@@ -9,6 +9,9 @@ SimpleCov.start do
SimpleCov::Formatter::HTMLFormatter
])
skip '/spec/'
# The harness runs under gdb/qemu against real libcs, which CI has none of;
# its unit specs run here, but its coverage is not what this bar is about.
skip '/aletheia/'
skip '/lib/one_gadget/builds/'
# The suite covers every line, so anything less is a real gap rather than a
# number to interpret -- and a new line arrives covered or the build says so.
+66
View File
@@ -0,0 +1,66 @@
# frozen_string_literal: true
ARCHES = %w[aarch64 amd64 arm i386].freeze
FIXTURES = 'spec/data/*.so'
namespace :aletheia do
desc 'Run every gadget one_gadget reports for a libc and check a real shell comes back'
# Verification is always strict: whatever a gadget's constraints do not name is
# poisoned, so an incomplete constraint list fails here instead of passing by
# luck. Needs the harness's prerequisites -- see aletheia/README.md.
#
# bundle exec rake aletheia:verify # every fixture, level 0
# bundle exec rake "aletheia:verify[1]" # deeper output level
# bundle exec rake "aletheia:verify[0, arm]" # one architecture
# bundle exec rake "aletheia:verify[2, spec/data/arm-libc-2.39.so]"
task :verify, :level, :target do |_t, args|
require 'json'
bin = File.expand_path('../aletheia/bin/aletheia', __dir__)
raise "#{bin} is missing; the harness lives on the aletheia branch" unless File.executable?(bin)
level = (args.level || 0).to_i
targets = aletheia_targets(args.target)
raise "no libc matches #{args.target.inspect}" if targets.empty?
totals = Hash.new(0)
targets.each do |file|
results = aletheia_verify(bin, file, level)
results.each { |r| totals[r['result']] += 1 }
report(file, results)
end
puts "level #{level}: #{totals.sort.map { |result, n| "#{n} #{result}" }.join(', ')}"
unverified = totals.sum { |result, n| result == 'PASS' ? 0 : n }
raise "#{unverified} gadgets did not verify" unless unverified.zero?
end
# A libc to verify: everything shipped for the specs by default, an
# architecture's share of them, or whatever a path or glob names.
# @param [String, nil] target
# @return [Array<String>]
def aletheia_targets(target)
return Dir.glob(FIXTURES) if target.nil? || target.empty?
target = target.strip
if ARCHES.include?(target)
require 'one_gadget'
return Dir.glob(FIXTURES).select { |f| OneGadget::Helper.architecture(f).to_s == target }
end
Dir.glob(target).select { |f| File.file?(f) }
end
# @return [Array<Hash>] one entry per gadget, as the harness reports it.
def aletheia_verify(bin, file, level)
out = IO.popen([bin, 'verify', file, '--level', level.to_s, '--strict', '--json'], &:read)
out.lines.filter_map { |l| JSON.parse(l) rescue nil } # rubocop:disable Style/RescueModifier
end
def report(file, results)
counts = results.group_by { |r| r['result'] }.transform_values(&:size)
puts format('%-56s %s', File.basename(file), counts.sort.map { |k, v| "#{v} #{k}" }.join(', '))
results.reject { |r| r['result'] == 'PASS' }.each do |r|
puts format(' %-10s %s %s', r['result'], r['offset'], r['reason'])
end
end
end