{"id":"ad6d6492-e1ec-4ade-aa91-2de7bdd71c0e","arxiv_id":"2411.11624","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Teapot statically rewrites COTS binaries into separate normal and speculation-simulation code paths and fuzzes them to discover Spectre-V1 gadgets without source code.","lead":"Teapot is a new tool that scans compiled binary programs, without source code, for Spectre-V1 gadgets by rewriting the binary so it can simulate mispredicted branches and then fuzz the program. It is claimed to be the first such static binary rewriter, running over 20 times faster and finding more gadgets than the previous binary-based approach SpecTaint.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Shadow Copy relocation of PC-relative data references is unspecified and can silently break speculation simulation.","rationale":"The paper's central claim depends on the Shadow Copy being a faithful stand-in for the transient execution path. The single most load-bearing assumption is therefore that the copy preserves the semantics of the original function. The reader's weakest assumption focuses on Datalog Disassembly/GTIRB correctly recovering the instruction stream and control-flow graph. My concern is related but distinct: even after a perfectly correct disassembly, the described 'byte-to-byte copy' does not, on its face, account for x86-64 PC-relative data references and jump-table bases, which are abundant in real COTS binaries. Section 5.2 explicitly mentions updating direct branches and calls but is silent on data relocations. If GTIRB's re-assembly does recompute these displacements symbolically, the concern is resolved and the design is sound; the artifact makes this checkable. The paper itself is otherwise transparent about limitations (Section 8), ships a reproducible artifact for Figure 7 and Table 4, and its performance and detection evidence is substantial but conditional. Because my concern is a specific rewriting-correctness failure mode rather than a disassembler-accuracy caveat, I only partially agree with the reader's weakest assumption. The right verdict stays CONDITIONAL: the central claim is plausible, but the semantic integrity of the Shadow Copy must be demonstrated before the detection-completeness and performance claims are fully established.","tokens_in":22370,"tokens_out":14788,"duration_ms":150836,"concrete_test":"Disassemble the `$spec` functions Teapot generates for a small PIE binary whose shadow-copied function contains a PC-relative global access followed by an injected Spectre gadget, and verify that every RIP-relative displacement in the Shadow Copy resolves to the same data target as in the Real Copy; then fuzz the binary and check that the injected gadget is reported. If any displacement is unadjusted by the copy delta or the gadget is missed, the Shadow Copy is semantically unsound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 5.2 says Teapot makes a 'complete, byte-to-byte copy' of each function and updates only direct branches and calls to point into the Shadow Copy. In x86-64, PC-relative data operands are pervasive: `mov`, `lea`, `cmp`, and similar instructions read `[rip+disp32]` globals, and jump-table idioms (including the clang switch code shown in Section 3.2) compute a base with `lea rcx, [rip+.LJT]`. A byte-identical copy placed at a different virtual address changes the effective address of every unrelocated `[rip+disp32]` operand by the difference between the Real and Shadow addresses. The paper never states how these displacements are adjusted, nor does it mention relocating jump-table bases. The failure would not be a visible crash: exceptions trigger the conservative rollback handler, and Section 5.3's indirect-branch guards force a rollback when a target is unrecognized. Thus a mis-relocated access silently cuts off the simulated transient path, suppressing any gadget whose secret load or transmitter depends on the wrong address. This is not covered by Section 8's disassembler caveat: even with perfect disassembly, the described copy procedure is incomplete unless PC-relative data references are re-emitted symbolically and recomputed. The evaluation does not rule this out because instrumented binaries can still find many gadgets before reaching a broken reference.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"Teapot proposes Speculation Shadows, a static-binary-rewriting design that splits each function into a Real Copy for normal execution and a Shadow Copy for speculation simulation, removing most per-instrumentation guard branches. The instrumented binary is fuzzed with honggfuzz, and gadget detection follows the Kasper policy implemented with binary-level ASan and DIFT. The paper reports runtime results on five real-world binaries, artificial-gadget ground-truth experiments, and detection results on unmodified binaries, claiming that Teapot is the first static-rewriting-based Spectre-V1 detector for COTS binaries, is within 0.5x--2.0x of SpecFuzz's runtime, and is more than 20x faster than SpecTaint and finds more gadgets.","tokens_in":22606,"tokens_out":4525,"duration_ms":46862,"significance":"If the central claims hold, Teapot is a practically important contribution: it is the first Spectre-V1 gadget scanner based on static binary rewriting, it ships an open-source artifact with scripts for reproduction, it evaluates against external baselines (SpecFuzz and SpecTaint), and it uses a ground-truth artificial-gadget experiment. Speculation Shadows is a clean design insight that could benefit other binary instrumentation tools. However, the correctness of the Shadow Copy depends on an unspecified handling of PC-relative data references, and the headline performance advantage over SpecTaint is measured on only two of the five programs. These issues must be resolved before the paper's central claims can be accepted.","major_comments":[{"comment":"The description of the Shadow Copy is incomplete for x86-64 code. Section 5.2 says Teapot makes a 'complete, byte-to-byte copy' of each function and updates only direct branches and calls. In x86-64, PC-relative data operands are pervasive: memory operands such as [rip+disp32] and LEA instructions compute addresses relative to the instruction pointer. A byte-identical copy placed at a different virtual address will silently compute different effective addresses for every unrelocated RIP-relative operand, including jump-table bases of the kind shown in Figure 2 (lea rcx, [rip+.LJT]). The paper never states how these displacements are adjusted or how jump-table bases are relocated. The failure would not be visible as a crash: the exception handler and the indirect-branch guards in Section 5.3 conservatively roll back, so a mis-relocated access would simply cut off the simulated transient path and suppress any gadget whose secret load or transmitter depends on the wrong address. This is not covered by the Section 8 disassembler caveat because even with perfect disassembly the described copy procedure is incomplete. The authors must either describe the relocation procedure or demonstrate, with concrete examples or artifact inspection, that all RIP-relative data references in Shadow Copies are re-emitted with corrected displacements.","section":"§5.2, Figure 4"},{"comment":"The abstract's general claim that Teapot is 'more than 20x performant' than SpecTaint is supported by only two of the five benchmark programs. For libhtp, brotli, and openssl, SpecTaint crashes the emulator and no SpecTaint times are reported. This makes the headline comparison partial, and the conclusion that Teapot outperforms 'the previously proposed binary-based approach' is broader than the evidence. The authors should qualify the claim to the two programs where SpecTaint runs, or provide SpecTaint measurements on the remaining programs, or present the comparison as a best-effort case study rather than a general performance result.","section":"§7.1, Figure 7"},{"comment":"The artificial-gadget comparison against SpecTaint relies on numbers reported in the SpecTaint paper rather than on a reproduced run, while the reproduced SpecFuzz results differ substantially from the reported ones (e.g., libyaml recall rises from 40% to 80% and brotli recall from 54% to 100%). This asymmetry weakens the claim that Teapot's detection ability is superior to SpecTaint. The authors do acknowledge the difficulty of reproducing SpecTaint, but the evaluation section should state explicitly which SpecTaint rows are not independently verified and treat the comparison as indicative rather than definitive.","section":"§7.2, Table 3"}],"minor_comments":[{"comment":"The phrase 'more than 20x performant than a previously proposed binary-based approach' is grammatically awkward; replacing it with 'more than 20x faster' would improve readability.","section":"Abstract"},{"comment":"There is a typo in the first paragraph: 'detect Specter gadgets' should be 'detect Spectre gadgets'.","section":"§5.1"},{"comment":"The y-axis of Figure 7 is difficult to read: the tick labels appear to be duplicated and the scale is not clearly described. A logarithmic axis or a table of the underlying normalized times would make the comparison easier to verify.","section":"Figure 7"},{"comment":"The rationale for the nested-speculation heuristic (sixth-order depth for the first five runs of a branch, then SpecFuzz heuristics) is stated but not justified with sensitivity experiments; a brief discussion of why these constants were chosen, or a sensitivity comparison, would strengthen the evaluation.","section":"§6.1"},{"comment":"The artifact appendix does not reproduce the artificial-gadget experiment (Table 3), which is the only ground-truth evaluation of detection ability. Since the artifact is a stated contribution, adding a scripted or documented procedure for that experiment would improve reproducibility.","section":"§B.8.2"}],"recommendation":"major_revision","confidential_remarks":"The PC-relative relocation issue is the central technical concern. If the authors can show in the artifact or by a precise description that RIP-relative operands are relocated when Shadow Copies are created, the main objection would be resolved. The partial SpecTaint comparison is more a matter of wording and scope than a fundamental flaw. The paper is otherwise a solid systems contribution for CGO."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Teapot is the first static-binary-rewriting Spectre-V1 gadget scanner for COTS binaries, and the Speculation Shadows design is a genuine contribution: separating Real and Shadow copies to eliminate guard branches is simple and effective. The engineering is solid—~3k lines of Python/C/asm, an artifact with Docker images and scripts, and careful comparison against SpecFuzz and SpecTaint on five standard programs. The performance numbers are believable: 0.5x-2.0x of SpecFuzz and 22-28x faster than SpecTaint on the two SpecTaint programs that ran. The artificial-gadget ground truth, where Teapot misses only two unreachable gadgets in libyaml, is the strongest detection evidence in the paper.\n\nThe main soft spot is one the paper doesn't discuss: the Shadow Copy is a byte-to-byte copy placed at a different virtual address, but the paper never explains how PC-relative data references ([rip+disp32]) are relocated. In x86-64 these are pervasive—global variable loads, jump table bases, and constant pool references. If they aren't re-emitted symbolically, the Shadow Copy reads the wrong addresses; the result isn't a crash (the exception handler rolls back), so Teapot silently drops gadgets whose secret load or transmitter depends on a mis-relocated reference. This isn't covered by the disassembler caveat in Section 8; it would matter even with perfect disassembly. The evaluation doesn't rule it out because Teapot still finds many gadgets elsewhere. This is not necessarily fatal—the implementation may well handle relocations through GTIRB, but the paper should say how.\n\nTwo other issues: the SpecTaint baseline is only reproducible on two of five programs, so the '20x+ faster' claim is narrower than the abstract suggests, and the Table 3 experiment is explicitly omitted from the artifact, which weakens the detection-ability headline. Both are acknowledged in Section 7 and Appendix B, which is honest, but they should be fixed for the claims to be fully established.\n\nBottom line: this deserves a serious referee. I'd send it out, and ask for a concrete relocation story for RIP-relative data, plus packaging for Table 3 and a clearer scoping of the SpecTaint speedup.","headline":"Teapot has a genuinely new design and solid engineering, but the paper leaves a load-bearing question about PC-relative data relocation in Shadow Copies open.","tokens_in":23184,"tokens_out":2825,"would_cite":false,"duration_ms":26264,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Teapot claims that Spectre-V1 gadgets can be found directly in closed-source x86-64 binaries, with no source code, at speeds comparable to compiler-based scanners, by rewriting each binary into a normal-execution copy and a…","keywords":["Spectre gadgets","static binary rewriting","speculative execution","dynamic taint analysis","fuzzing","COTS binaries","side channels","binary instrumentation"],"falsifier":"A concrete test: build a small stripped x86-64 binary whose only reachable Spectre-V1 gadget sits behind an indirect jump that the rewriting pass cannot resolve. If Teapot, fuzzed with inputs that trigger the misprediction, reports no gadget while a manual trace confirms the transient access, then its detection is limited by disassembly completeness rather than by speculation simulation.","tokens_in":22090,"feed_emoji":"🫖","tokens_out":9517,"duration_ms":88310,"temperature":0.7,"pith_summary":"The paper sets out to show that Spectre-V1 gadgets — code that leaks data through mispredicted bounds checks — can be uncovered in commercial off-the-shelf binaries without access to source code, at run-time costs close to those of compiler-based detectors. To achieve this, Teapot statically rewrites each function into two copies: a Real Copy that runs normal execution and a Shadow Copy that simulates transient execution, so each copy carries only the instrumentation it needs and the guard branches around every check disappear. On top of this skeleton Teapot adds binary-level out-of-bounds checks and data-flow taint tracking, then fuzzes the instrumented binary to trigger and report gadgets through cache, microarchitectural data sampling, and port-contention channels. The paper reports that this design outperforms the previous binary-only approach by more than 20x in runtime and finds all reachable artificially injected gadgets with no false positives on the tested programs.","feed_headline":"Teapot finds Spectre gadgets in binaries 20x faster","feed_subtitle":"Static binary rewriting brings Spectre-V1 scanning to closed-source x86-64 programs with no source code needed.","key_machinery":"Speculation Shadows is the named mechanism: a design that duplicates every function in the binary into a normal-execution copy and a speculation-simulation copy. Direct branches and calls are rewired to the matching copy, trampolines flip the branch condition to enter the wrong path and start transient simulation, and end_simulation restore points trigger rollback after a preset instruction window of 250 instructions, matching the reorder-buffer idea. To keep control flow inside the Shadow Copy, indirect returns, calls, and jumps get runtime checks plus special nop markers at Real-Copy targets. Teapot's detection layer reimplements AddressSanitizer-style shadow-memory bounds checks and DataFlowSanitizer-style byte-granular tag propagation directly on the binary, using the Kasper taint policy to classify attacker-controlled and secret data. The machinery's work is to make speculation simulation cheap enough that deep nested mispredictions can be fuzzed, which is what lets Teapot find gadgets previous binary scanners missed.","core_discovery":"The central claim is that Spectre gadget detection no longer requires source code or full-system emulation: a static binary rewriter can instrument a deployed x86-64 Linux binary to simulate branch misprediction and detect gadgets at run time with practical efficiency. The load-bearing discovery is Speculation Shadows: instead of mixing normal execution, speculation simulation, ASan checks, and memory logging in one code stream guarded by in_simulation conditionals, every function is duplicated byte-for-byte. Normal execution stays in the Real Copy and speculation simulation runs in the Shadow Copy; trampolines on conditional branches send the program down the deliberately wrong path, and checkpoint/rollback plus indirect-branch integrity checks keep the simulation contained. Each copy is then instrumented with only what it needs — the Shadow Copy gets bounds checks, memory logging, and taint propagation, while the Real Copy gets lightweight asynchronous tag updates — which removes almost all guard branches. Evaluations on five real-world binaries show Teapot is 22–28x faster than the previous binary-based detector on the programs where that detector runs, performs within 0.5–2.0x of a compiler-based tool, and detects every reachable gadget in the artificial-injection benchmark with zero false positives.","pith_inferences":["Speculation Shadows is a general binary-rewriting pattern: any analysis that needs different instrumentation during a special mode could duplicate functions and drop guard checks, so the speedup is not limited to Spectre scanning.","The paper's switch-statement example (GCC generates branches while Clang generates a jump table) implies Teapot can serve as a deployment-time check: even source-owning teams could run it on release binaries to catch toolchain-induced gadgets that compiler-based scans miss.","Detection is bounded by fuzzing coverage and the fixed speculation window of 250 instructions and six branch levels; a CPU with a larger reorder buffer or a different fuzzer could reveal additional gadgets without changing Teapot's instrumentation.","Porting the design to AArch64 or Windows, which the paper lists as future work, would face its main challenge in disassembly accuracy rather than in the Shadow Copy mechanism itself."],"forward_implications":["Closed-source x86-64 Linux binaries can be scanned for Spectre-V1 gadgets without source code, at run-time overhead within about 0.5x–2.0x of compiler-based instrumentation.","Deeper speculation heuristics become affordable: Teapot simulates nested mispredictions beyond the five-simulation limit of the previous binary tool and reports more gadgets on unmodified binaries as a result.","The design removes most mode-check guard branches, giving a performance edge of 22x–28x over full-system emulation on the two programs where the emulator-based baseline completed.","Taint tracking plus binary bounds checks lets Teapot distinguish attacker-controlled out-of-bounds reads from benign ones, yielding no false positives on the injected-gadget benchmark where a compiler-based tool without taint produced many false positives.","Because the detector is decoupled from the fuzzer through a standard coverage interface, the same instrumented binaries can be reused with different coverage-guided fuzzers."],"supporting_citations":[{"why":"The compiler-based detector that defines the checkpoint/rollback speculation-simulation architecture and serves as Teapot's performance and detection baseline.","marker":"[30]"},{"why":"The only previous binary-level detector, used as the direct baseline for the claimed 20x+ speedup and detection comparison.","marker":"[36]"},{"why":"The Kasper policy Teapot ports to binaries, defining User and Massage taint classes and the MDS, cache, and port-contention reporting scheme.","marker":"[21]"},{"why":"The Datalog Disassembly platform that recovers functions and rewrites binaries, making static rewriting possible.","marker":"[12]"},{"why":"GTIRB, the binary intermediate representation used to represent and reassemble the instrumented program.","marker":"[39]"},{"why":"AddressSanitizer, whose shadow-memory scheme Teapot reimplements in binary form for out-of-bounds detection.","marker":"[40]"},{"why":"DataFlowSanitizer, whose tag-shadow design Teapot adapts for binary dynamic taint tracking.","marker":"[25]"},{"why":"The original Spectre paper, which defines the V1 bounds-check-bypass gadget that Teapot targets.","marker":"[23]"}],"fun_headline_variants":["Teapot: Spectre scanning for closed-source binaries","Static rewriting exposes Spectre gadgets in binaries","Teapot detects Spectre gadgets 20x faster, no source needed","Speculation Shadows speed up Spectre gadget detection","Teapot finds Spectre holes in binaries without source"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Teapot assumes the static disassembler correctly recovers every instruction, every function boundary, and every indirect branch target, because code it cannot see is never duplicated into the Shadow Copy and can never be checked.","fun_headline_variants_meta":{"raw":{"variants":["Teapot: Spectre scanning for closed-source binaries","Static rewriting exposes Spectre gadgets in binaries","Teapot detects Spectre gadgets 20x faster, no source needed","Speculation Shadows speed up Spectre gadget detection","Teapot finds Spectre holes in binaries without source"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000213,"raw_usage":{"total_tokens":1447,"prompt_tokens":997,"completion_tokens":450,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":613,"completion_tokens_details":{"reasoning_tokens":370}},"tokens_in":613,"tokens_out":450,"duration_ms":3896,"temperature":1.0,"reasoning_tokens":370,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:18:21.833086+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete test: build a small stripped x86-64 binary whose only reachable Spectre-V1 gadget sits behind an indirect jump that the rewriting pass cannot resolve. If Teapot, fuzzed with inputs that trigger the misprediction, reports no gadget while a manual trace confirms the transient access, then its detection is limited by disassembly completeness rather than by speculation simulation.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The compiler-based detector that defines the checkpoint/rollback speculation-simulation architecture and serves as Teapot's performance and detection baseline."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The only previous binary-level detector, used as the direct baseline for the claimed 20x+ speedup and detection comparison."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The Kasper policy Teapot ports to binaries, defining User and Massage taint classes and the MDS, cache, and port-contention reporting scheme."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The Datalog Disassembly platform that recovers functions and rewrites binaries, making static rewriting possible."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"AddressSanitizer, whose shadow-memory scheme Teapot reimplements in binary form for out-of-bounds detection."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"DataFlowSanitizer, whose tag-shadow design Teapot adapts for binary dynamic taint tracking."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The original Spectre paper, which defines the V1 bounds-check-bypass gadget that Teapot targets."}],"review_version":1}