Skip to content

SPIDER_LINEAGE.md

Latest commit

 

History

History
209 lines (162 loc) · 9.16 KB

SPIDER_LINEAGE.md

File metadata and controls

209 lines (162 loc) · 9.16 KB
Raw

SPIDER lineage

TianoShield began as a workspace around the original SPIDER research implementation and is now a separate Python design. This document records where TianoShield came from, how the two tools differ, which SPIDER capabilities were and were not reimplemented, and where the original code is preserved.

Reference

Aravind Machiry, Nilo Redini, Eric Camellini, Christopher Kruegel, and Giovanni Vigna. "SPIDER: Enabling Fast Patch Propagation in Related Software Repositories." 2020 IEEE Symposium on Security and Privacy (SP), 2020. Paper · IEEE Xplore

Dr. Aravind Machiry, SPIDER's lead author, is a member of the TianoShield project. TianoShield extends his SPIDER work within that project.

Where the original code lives

The Java/Joern implementation, its build files, batch and statistics scripts, Android Security Bulletin example pairs, the QAS Docker path, and the earlier docs/SPIDER_PARITY.md inventory are preserved at the Git tag spider-reference (commit dad547c) of the private working repository. They are not part of the current product, runtime, or package.

The legacy tool requires Linux because Joern bundles Linux-only Z3 JNI libraries. From a checkout of the tag, the existing Docker path builds and exercises it:

git switch --detach spider-reference
scripts/qas-container-smoke.sh

Different questions

SPIDER and TianoShield answer different questions about the same kind of upstream fix.

  • SPIDER asks whether an upstream patch is a safe patch: one that does not disrupt intended functionality on valid inputs and can therefore be propagated to related repositories without testing. It never examines a downstream fork.
  • TianoShield asks whether one pinned downstream function still contains the upstream pre-patch state, already contains the post-patch state, is absent, or cannot be decided. It can then produce and check an inert candidate patch for human review.

SPIDER

  • Input: pre-patch and post-patch versions of one C file.
  • Output: a per-function safepatch Boolean with condition, insertion, and move counts, plus a patch size.
  • Parsing and diffing: the Joern parser, GumTree AST mapping, and unifdef preprocessing.
  • Program analysis: a program dependence graph, error-handling basic blocks, and symbolic path constraints.
  • Solver: Z3 through Java JNI.
  • Runtime: Java, Ant, Python 2, and Linux-only native libraries.

TianoShield

  • Input: upstream pre-patch and post-patch files plus a downstream repository, commit, path, and function, sealed into a prepared manifest.
  • Output: VULNERABLE, ALREADY_PATCHED, NOT_APPLICABLE, or UNCERTAIN; JSON and Markdown evidence; and an optional inert candidate with isolated validation evidence.
  • Parsing and diffing: the Tree-sitter C grammar and deterministic patch-local differencing, with preprocessor constructs retained as diagnostics.
  • Program analysis: an intraprocedural CFG, read/write sets, and reaching definitions.
  • Solver: Z3 through Python, with fixed-width C integer models and bounded queries.
  • Runtime: CPython 3.11 to 3.13 and uv.

Reported results

The paper evaluates SPIDER on 341,767 commits from 32 repositories, finding 67,408 (19.72%) safe patches, and on 809 CVE-patching commits, of which 448 (55.37%) are safe.

The safe-patch definition

The paper defines a safe patch by two conditions on a function f and its patched version fp:

  • C1, non-increasing input space. Every input that executes successfully through fp also executes successfully through f. SPIDER checks this by building path constraints to the valid exit points of each function and proving an implication with Z3.
  • C2, output equivalence. For every such valid input, fp produces the same externally visible output as f: writes to global and pointer variables, function-call arguments and order, and return values. SPIDER checks this with symbolic output-constraint pairs over data-dependence paths in the program dependence graph.

It applies three further restrictions:

  • Every directly affected statement must be locally analyzable: no new function calls and no pointer manipulation.
  • Changes inside error-handling basic blocks are discarded before checking.
  • A patch that directly modifies a statement inside a loop is not safe.

The paper also describes a Security Patch (SeP) mode that restricts safe patches to control-flow-only changes to identify likely security fixes without a CVE.

Legacy entry points

The legacy tree contains several Java drivers:

  • build.xml packages executable.jar with tools.safepatch.SafepatchMain. That driver combines the heuristics in HeuristicsDispatcher.java with a Boolean OR and reports a security Boolean. It characterizes likely security patches; it does not evaluate C1 and C2.
  • flowres/ (for example, FlowRestrictiveMain.java) and iocorrespondence/ (IOCorrespondenceChecker.java and StatementLoopChecker.java) correspond to flow restriction (C1), output correspondence (C2), and the loop restriction. The first two write the documented safepatch JSON field; StatementLoopChecker writes spider and per-function hasinLoop fields.
  • The authors' batch script, joern/testscripts/testcves.py, invokes statementloopchecker.jar, not executable.jar.

This suggests that the flowres/ and iocorrespondence/ drivers, not SafepatchMain, implement the configuration used for the paper's results. Confirming this with the author is an open item.

The earlier docs/SPIDER_PARITY.md inventory treated SafepatchMain as the active legacy behavior and classified the flowres/ and iocorrespondence/ drivers as experimental. Its parity conclusions therefore describe the heuristic security-patch path rather than the paper's safe-patch analysis.

Capability comparison

Reimplemented

  • Parsing, function matching, and affected statements: reimplemented with Tree-sitter. Absence and ambiguity are explicit outcomes instead of crashes.
  • AST differencing: reimplemented as deterministic patch-local differencing. GumTree is not used.
  • Z3 condition reasoning: reimplemented for aligned conditions, with fixed-width C types, casts, timeouts, and explicit unknown results.

Partially reimplemented

  • Control-flow and data-dependence analysis: an intraprocedural CFG, read/write sets, and reaching definitions, but no full program dependence graph.
  • Error-handling basic-block detection: only narrow cases, such as negative-literal returns and caller-declared noreturn calls.

Not implemented

  • The locally analyzable filter.
  • C1, non-increasing input space.
  • C2, output equivalence.
  • The loop restriction.
  • SeP mode. TianoShield starts from known upstream fixes.
  • The heuristic security Boolean from SafepatchMain. It was intentionally not ported because it answers a different question.
  • The batch processing and statistics scripts.

TianoShield additions

Downstream target discovery, immutable preparation, the patch-state verdict, candidate generation, and isolated validation have no SPIDER equivalent.

TianoShield therefore reuses SPIDER's analysis concepts but does not yet compute SPIDER's safe-patch verdict.

Relevance to TianoShield

TianoShield's isolated validation checks only exact replay and parsing. Firmware build and hardware testing are expensive and platform-specific. A safe-patch result is evidence that a candidate may not need that testing, which makes C1 and C2 the most relevant unported SPIDER capability.

For the current generator, which requires the downstream function to equal the upstream pre-patch function byte for byte, a safe-patch result for the upstream pair applies unchanged to the downstream candidate. For divergent downstream functions, C1 and C2 can be evaluated directly on the downstream function and its candidate.

The locally analyzable restriction may exclude many EDK II fixes, because SPIDER treats macros as function calls and EDK II code relies heavily on macros, protocol calls, and pointers. Before porting C1 and C2, the planned next step is to run the original flowres/ and iocorrespondence/ drivers on the existing EDK II cases and measure the safe-patch rate. Any port would be an evidence-only analyzer under the authority boundaries in ARCHITECTURE.md.

Provenance and license

The Python implementation is a clean design based on SPIDER's published concepts and observed legacy behavior. It does not translate the Java sources line by line, reuse Java or JNI binaries, or package the legacy tree.

Use of the original SPIDER sources within TianoShield was approved by Dr. Machiry at the start of the project.

The legacy tree includes Joern under the GNU GPL v3 (joern/LICENSE at the tag). The SafePatch sources carry @author notices for Aravind Machiry and Eric Camellini but no license notice. This repository does not yet declare a license. Choosing one, and meeting any obligations for redistributing the legacy tree or derived work, is a project decision to make before public release. This is not legal advice.