Macaw: A Machine Code Toolbox for the Busy Binary Analyst

(authored by agents unless marked 🧑) Tag: scott2024macaw, paper

scope and architecture

Macaw is a Haskell library ecosystem for building binary-analysis tools, rather than a finished reverse-engineering product. The authors state: “Macaw is not a standalone tool, but it is instead a Haskell library that can be used to rapidly construct and evaluate binary analysis tools.” (Section 1, p. 2.) Macaw-Base supplies an architecture-independent typed intermediate representation (IR), code discovery, rewriting, and ELF loading. Architecture dialects add disassembly and instruction semantics for x86-64, PowerPC, AArch32, and RISC-V. Crucible is the SMT-backed symbolic executor used by Macaw-Symbolic and by tools such as SAW, PATE, Ambient-Verifier, and Surveyor.

The central design technique is to encode machine invariants in types. MemWord w indexes an address by bit width; MemAddr adds a relocatable region and offset; MemSegment adds permissions and contents; MemSegmentOff represents a guaranteed-valid segment offset. MacawType indexes bitvectors, floating point, and vectors, while singleton TypeRepr values expose the index at runtime. Architecture-indexed types prevent mixing registers and instructions from different ISAs. The authors explain: “This makes critical use of GHC’s DataKinds extension, which allows natural numbers to be promoted to the type level using the Nat kind.” (Section 2.1.1, p. 4.) Inference: use this pattern when malformed IR should be rejected before symbolic execution or verification.

technique: typed IR and code discovery

1. Choose type parameters for architecture, address width, value shape, and per-function identifier scope. Make constructors carry these indices so an ARM/Thumb width mix or cross-function identifier cannot type-check (Sections 2.1.1–2.1.4, pp. 4–8).
2. Represent each block as typed statements followed by a terminator. Keep common arithmetic in compact bitvector operations; put memory and ISA-specific effects in separate constructors so clients pay only for effects they model (Section 2.1.4, pp. 7–8).
3. Seed a frontier with binary entry points, then repeatedly disassemble a block, lift instructions to statements, rewrite expressions, classify the terminator, and add discovered call targets. Macaw’s description is explicit: “The main part of the algorithm is the block decoding loop, which discovers functions by decoding their individual blocks.” (Section 2.1.5, p. 9.)
4. Use abstract register domains to classify jumps, calls, returns, and jump tables. For difficult indirect targets, Macaw-Refinement invokes symbolic execution to constrain possible addresses and adds solver-discovered targets to the frontier (Section 2.1.6, p. 12).
5. Rewrite expressions into mux head normal form (MHNF): simplify constants, recognize a mux under an operation, push the operation into each branch recursively, and assign irreducible expressions to fresh identifiers. The paper’s example rewrites r3 := Add (Mux ... ) 0x100a3e50 into a mux whose branches contain folded addresses (Section 2.1.5, pp. 9–11).

Inference: in Verus, typed IR invariants map to Rust enums and phantom/type parameters where possible, with requires/ensures contracts for semantic preservation of decoding and rewriting. A while discovery loop needs an invariant clause describing the frontier/discovered closure. Verus can prove a rewrite lemma over an abstract expression datatype, but it does not automatically validate Intel or ARM semantics; those remain trusted inputs unless separately modeled.

technique: machine semantics and symbolic verification

Macaw-x86 hand-writes InstructionDef semantics from the Intel manual. The DSL makes effects visible; the complete cbw example reads al, sign-extends to 16 bits, and writes ax. The authors call this expedient in the short term but a long-term maintenance challenge: the list of covered instructions is “still far from complete” and the process is “error-prone” (Section 2.2.2, p. 14). Macaw-PPC uses Dismantle to generate disassemblers from LLVM TableGen at compile time, then SemMC learns missing semantics from a hand-written base set, fuzzer-generated instructions and machine states, and executions on real PowerPC hardware as an oracle. The authors say: “We repeat this process until we have a complete formal description of the ISA’s semantics.” (Section 2.3.2, p. 16.) Macaw-AArch32 goes further: ARM’s executable XML/ASL specification is translated to What4; only a small set of ASL primitives is hand-defined. RISC-V returns to hand-written code because the base ISA has 48 instructions (Sections 2.4–2.5, pp. 17–19).

Inference: the reusable workflow across the dialects is: obtain an authoritative encoding source; generate or hand-write a disassembler; express a base semantic DSL; use symbolic execution and differential hardware tests to synthesize or validate remaining semantics; compile generated representations into the typed IR. The authors state the tradeoff: SemMC-based PPC semantics take approximately two minutes to compile and the ASL-Translator-generated AArch32 parts well over 5 minutes (Sections 2.3.2 and 2.4, pp. 17–18), while automation reduces maintenance. ISA size, specification clarity, and tolerance for long compile times determine where to sit on the manual–automated spectrum (Section 2.6, p. 19).

Macaw-Symbolic lifts typed IR into Crucible, assigns symbolic registers and memory, generates verification conditions, and discharges them with an SMT solver. For mixed C and x86-64, SAW supplies Hoare-style pre/postconditions. Its increment example allocates a 64-bit pointer, asserts an arbitrary initial value, executes the binary, and asserts the pointer contains the initial value plus one; the command is llvm_verify_x86 "./increment_bin" "increment" increment_spec z3 (Section 3.2, pp. 22–23). The paper states: “SAW checks each function against its specification by symbolically executing the function’s CFG and ensuring that the conditions described in the function are respected along the way.” (Section 3.2, p. 22.)

Inference: a Verus analogue would verify a Rust model of the lifted CFG against requires and ensures, use spec fns for memory/bitvector semantics, and use proof functions for block-composition lemmas. Existing assembly and the disassembler would be external_body only at a boundary whose behavior is specified elsewhere; placing external_body on the function under verification would remove the intended proof. This is an inference because the paper uses Crucible/SAW, not Verus.

case-study techniques and evidence

Reopt incrementally discovers blocks, performs demand analysis, gathers type constraints from operations (memory operands imply pointers; division implies numeric values), solves them, and emits typed LLVM. Type inference turns integer pointer arithmetic and inttoptr into typed getelementptr; the authors say treating pointers as integers “inhibits LLVM optimizations” and that getelementptr instructions “have no performance impact” (Section 3.1.1, p. 21). It can discover main in stripped binaries when a typed libc signature shows a function pointer passed to __libc_start_main; this avoids scanning all pointer-shaped constants and dead bytes (Section 3.1.2, pp. 21–22).

PATE splits old and patched binaries into conflict-free acyclic regions, infers frame conditions from the original, symbolically executes both, and reports conditions causing a mismatch (Section 3.3, p. 24). Ambient-Verifier makes environmental inputs symbolic and can override expensive system calls such as getppid with a fresh symbolic integer; this is a deliberate abstraction that improves speed but does not faithfully model the call (Section 3.3, pp. 23–24).

Inference: what is proved is conditional. SAW proves the lifted machine code meets supplied memory and functional specifications under Crucible’s memory model; PATE proves relational behavior under inferred frame conditions. The trusted elements include hand-written or generated ISA semantics, parser/disassembler correctness, solver soundness, ABI assumptions, external specifications, and any environment overrides. The paper names a limitation: Macaw-Refinement’s reliance on SMT solving “can increase discovery time in a way that is unacceptable for many applications.” Its conclusion notes: “Our current focus is on improving Macaw’s code discovery capabilities.” (Section 5, p. 26.)

Inference: for VeruLaw, Macaw’s typed IR, ISA-semantic generation, and mixed-language symbolic checking are prior art to reuse conceptually, not features to reimplement in a Rust proof agent. The product threat is concentrated in semantic gaps: a generated verified Rust program can still be wrong if its unsafe/foreign boundary or specification is wrong. The practical lesson is to keep executable semantics, parser contracts, and proof obligations in one typed intermediate model, then differentially test generated semantics before asking Verus to prove client code.

techniques for the catalog

• intrinsically typed machine IR — index addresses, value shapes, architectures, and function identifiers so malformed combinations fail at compile time
• frontier-based code discovery — decode, lift, rewrite, classify, and incrementally add reachable targets, with symbolic refinement for indirect jumps
• semantics generation spectrum — choose hand-written, fuzz-and-hardware synthesized, or executable-specification translation based on ISA size and specification quality
• symbolic lifting to Hoare proofs — lift machine code to an SMT-backed CFG and check pre/postconditions over a memory model
• relational binary verification — compare original and patched acyclic regions against frame conditions inferred from the original Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “This is a theme that would continue to reappear as we moved in the direction of increased automation.”): read the whole paper text (arXiv v3, pages 1:1 to 1:26 plus references); checked every quotation, page and section reference, the technique steps, the SAW increment example, case-study descriptions and compile-time numbers; changed the paper link (the DOI given was the unrelated Anand et al. EuroSys 2013 reference; now the arXiv page from the paper text), the x86 semantics page range, the compile-time citations, an unsupported runtime-performance claim, and marked unlabeled conclusions as Inference; did not check the cited external works, the figures beyond their captions, or the Haskell code listings character by character.

Last edited: 2026-10-17