Manta: Hybrid-Sensitive Type Inference Toward Type-Assisted Bug Detection for Stripped Binaries

When source code is compiled into a stripped binary, the variable types vanish, and without them a security tool analyzing that binary — say, firmware with no source — cannot tell which function an indirect call could really reach or which data actually depends on which, so it drowns in false possibilities; this paper (HKUST) recovers those types by combining several data-flow analyses of different precision that cover each other's weaknesses — a cheap coarse pass to guess a type for nearly every variable, then sharper passes to tighten the over-broad guesses — inferring types at high precision and recall, and using them to prune infeasible call targets and dependencies well enough to have surfaced 86 confirmed firmware vulnerabilities, 64 with assigned identifiers.

Why this problem is worth solving

The entire precision of a binary analysis rides on a kind of information the binary no longer contains.

The reason existing recovery falls short is a fundamental tension in how static analyses trade breadth for sharpness.

What people did before, and where it broke

• Analyze binaries without types at all. Run indirect-call and data-dependency analysis on the stripped binary directly, conservatively assuming anything is possible. Where it broke. Without types the analysis cannot prune infeasible targets or flows, so it drowns in false possibilities and its bug reports are imprecise — the core problem.
• Low-precision type inference (flow/context-insensitive). Collect every type hint for a variable and unify them, cheaply assigning a type to nearly every variable. Where it broke. Because hints from many unrelated variables are merged, each variable gets a bloated, over-approximated type; high recall but low precision, and coarse types prune little.
• High-precision type inference (flow/context-sensitive). Propagate type hints carefully along control flow with strong updates and along valid calling contexts to avoid blurring. Where it broke. The carefulness gathers fewer hints, leaving many variables’ types unknown; high precision but low recall, and unknown types prune nothing.
• Pick one sensitivity and accept its weakness. Commit to either the coarse-but-complete or the precise-but-partial approach as a fixed design point. Where it broke. Either choice leaves inferred types that cannot effectively assist the downstream analysis — too coarse to filter, or too sparse to matter — so type-assisted binary bug detection never materialized.
• The gap. No approach combined sensitivities so that the coarse analysis’s recall and the precise analyses’ precision covered each other, yielding types that are both broadly assigned and sharp enough to prune real infeasible facts in bug detection. That combination is what Manta introduces.

How Manta works

The idea

Let analyses of different precision cover each other’s blind spots. The stuck point in binary type inference is that each sensitivity fails in the opposite way: the coarse analysis over-approximates, the precise analysis leaves variables unknown. Manta’s central observation is that these failures are complementary. A precise analysis can pin down exactly the types that a coarse analysis left as bloated unions, because it does not blur unrelated hints together; and a coarse analysis can supply types for exactly the variables a precise analysis abandoned as unknown, because it gathers hints broadly. So rather than picking one sensitivity and living with its weakness, Manta runs several and lets each repair the other’s output, achieving both high precision and high recall. Combining static analyses tuned to different sensitivities so that their strengths compensate for their individual imprecision is the same complementary-precision strategy the path-sensitive, alias-aware analysis work covered elsewhere on this site is built on, dialing analysis sensitivity to where it pays and leaning on cheaper reasoning elsewhere so the whole is more precise than any single setting.

Start coarse for recall, then refine only what is over-approximated. The way Manta orchestrates the combination is a staged refinement that spends effort where it is needed. It begins with the cheapest, most complete analysis — a global flow- and context-insensitive pass that assigns a type to nearly every variable, guaranteeing high recall even though many of those types are coarse. Then it applies the expensive high-precision analyses selectively, only to the variables whose types came out over-approximated, sharpening those coarse unions rather than re-analyzing everything. This staging is what makes precision affordable: the costly context- and flow-sensitive reasoning is aimed exactly at the over-approximations it can fix, not spent uniformly. Reconstructing high-level structure from a stripped binary by first recovering a broad, approximate picture and then progressively refining it is the same reverse-engineering discipline the accurate-disassembly work covered elsewhere on this site relies on, rebuilding what compilation discarded through layered inference rather than one monolithic pass.

Turn recovered types into a filter that prunes the impossible. Types are only worth recovering if they make the downstream analysis better, and Manta’s payoff is precisely that. It feeds the refined types into bug detection as a pruning filter: at an indirect call, only functions whose type matches the function pointer’s recovered type are kept as possible targets, discarding the rest; in data-dependency tracking, a putative dependency between two locations of incompatible types is dropped as infeasible. Removing these impossibilities shrinks the search space the bug detector must consider, which both speeds it up and cuts false positives, and it is accurate enough that program slicing on the binary comes close to slicing on the original source. Using a recovered, precise notion of what a pointer can legitimately be to prune the infeasible targets of an indirect call is the same type-driven filtering the precise pointer-analysis work covered elsewhere on this site performs, tightening the set of legal call targets so a downstream security analysis reasons about only what can really happen.

Following a variable through Manta

The lifting and points-to map give a uniform data-flow view on which the inference operates.

Why it works

• Complementary sensitivities beat any single one. Each sensitivity fails oppositely — coarse over-approximates, precise leaves unknowns → but a precise pass fixes the coarse over-approximations while the coarse pass fills the precise pass’s unknowns → so Manta reaches both high precision (78.7 percent) and high recall (97.2 percent) that neither achieves alone.
• Starting coarse guarantees recall. A precise-only analysis abandons many variables as unknown → but a cheap flow- and context-insensitive first pass assigns a type to nearly every variable → so almost nothing is left untyped before refinement even begins, anchoring the high recall.
• Refining only over-approximations makes precision affordable. Running expensive context- and flow-sensitive analysis on everything would not scale → but applying it only to the variables the coarse pass over-approximated targets the effort where it fixes something → so precision rises without re-analyzing the whole binary.
• Precise types prune what the untyped analysis could not. Without types, an indirect call seems to reach almost any function and data seems to flow almost anywhere → but matching a call’s recovered function-pointer type against candidate functions discards the mismatched ones → so Manta prunes 63.9 percent more infeasible indirect-call targets than existing type analysis.
• Accurate types bring binary analysis near source level. A binary analysis normally lags source analysis precisely because it lacks types → but recovering them precisely restores the filter source analyses enjoy → so program slicing on the binary reaches 61.1 percent similarity to slicing on the original source, and the sharpened detection found real vulnerabilities.

What it costs (trade-offs and scope)

• Precision is high but not perfect. At 78.7 percent precision the inferred types are far better than prior work but still sometimes wrong, so some pruning decisions rest on imperfect types; a mis-inferred type could over-prune (risking missed behavior) or under-prune, and the downstream analysis inherits that residual error.
• The staged refinement adds machinery and cost. Running a coarse global pass followed by selective context- and flow-sensitive refinements is more complex and more expensive than a single-sensitivity analysis; the design keeps it affordable by refining only over-approximations, but it is heavier than the simplest approaches and its cost scales with how many variables need refinement.
• It depends on lifting and pointer analysis being sound enough. Manta operates on an LLVM intermediate representation lifted from the binary and on a pointer analysis; errors or imprecision in lifting stripped machine code or in the points-to map propagate into the type inference, and binary lifting is itself a hard, imperfect step.
• Recovered types are structural, not semantic ground truth. Type inference reconstructs types from usage, so it recovers what the code’s behavior implies rather than the programmer’s original declarations; unusual coding patterns, heavy pointer casting, or optimized code can yield types that differ from the source intent even when they are consistent with the binary.
• Evaluation centers on indirect calls, dependencies, and firmware bug-finding. The reported gains — the precision and recall, the 63.9 percent extra target pruning, the 61.1 percent slicing similarity, and the 86 confirmed vulnerabilities — are for these specific tasks and targets; the approach’s value on other analyses, architectures, or heavily obfuscated binaries is beyond what the paper measures.

The evaluation

Check yourself

Sources

The paper is “Manta: Hybrid-Sensitive Type Inference Toward Type-Assisted Bug Detection for Stripped Binaries” by Chengfeng Ye, Yuandao Cai, Anshunkang Zhou, Heqing Huang, Hao Ling, and Charles Zhang (The Hong Kong University of Science and Technology, with Heqing Huang at City University of Hong Kong), published at ASPLOS 2024 (Volume 4), DOI 10.1145/3622781.3674177.

This explainer is written from the full text of the authors’ copy of the paper. Everything above comes from the paper’s own sections: the introduction motivating type-assisted static binary bug detection for source-less software such as firmware and industrial control systems, and identifying the loss of type information during compilation as the main reason binary analysis is imprecise, since types are used to prune infeasible indirect-call targets and data dependencies; the problem statement that existing binary type inference either over-approximates (flow- and context-insensitive analysis unifying all type hints indiscriminately, giving high recall but low precision) or leaves many types unknown (flow- and context-sensitive analysis propagating hints carefully, giving high precision but low recall); the observation that a hybrid combination of sensitivities can complement each other (a precise analysis refining over-approximated types, a coarse analysis capturing hints the precise one ignores); the Manta pipeline (lifting the binary to LLVM IR, pointer analysis producing a points-to map, a global flow- and context-insensitive pass producing an over-approximated initial type map, then context-sensitive and flow-sensitive refinement of the over-approximated types, followed by type-assisted analysis that prunes infeasible indirect-call targets and data dependencies); and the evaluation reporting 78.7 percent precision and 97.2 percent recall (about 32.7 percent better than prior inference on average), 63.9 percent more infeasible indirect-call targets pruned than existing type analysis, program slicing on binaries with 61.1 percent similarity to source-level slicing, and 86 new developer-confirmed vulnerabilities in popular IoT firmware with 64 assigned CVE or PSV identifiers.