From a sink
to a solver question.
A visual reading of the v0.4r architecture: represent the context of a vulnerable operation, retrieve related families, and test whether the patch’s safety conditions hold in a candidate.
01 / A concrete starting point
Enough data to overflow. Enough context to explain why.
The operation is only the starting point
A sink is the operation whose safety is being examined—here, a memory copy. Copying is ordinary and useful. The relevant question is whether the amount being copied fits the destination, and which path establishes that condition.
The patch supplies a question
A bound added by a patch can be expressed as a predicate: copy_length ≤ capacity. SCJ’s patch-intent extraction identifies the added conditions, then asks whether related implementations enforce them too. The drawing is a teaching example, not a disclosed vulnerability.
02 / The geometric representation
A fingerprint of operations and relationships.
| Channel | Representation | Role |
|---|---|---|
| Instruction structure | 256-dimensional IR2Vec-style representation of P-code n-grams | Describe operations in an intermediate representation. |
| Graph neighborhood | 128-dimensional GraphSAGE representation over two-hop neighborhoods | Retain relationships around the function. |
| Engineered features | 64-dimensional feature vector | Include selected structural and safety-relevant properties. |
| Compressed embedding | 448 concatenated dimensions → 128 by PCA | Support approximate-neighbor retrieval. |
| Cross-module family | Sink identity + callsite signature | Group candidates using caller/callee context, argument shape and local control-flow shape. |
Similarity scoring combines vector proximity with sink overlap, semantic parity and binary-diff evidence. The geometry helps prioritize where to look. A similar embedding does not itself determine whether a candidate is vulnerable.
03 / The semantic question
Can these conditions hold while the protection fails?
SPES builds bounded slices of the relevant paths and compares candidate predicates with the conditions introduced by the patch. In the small model below, the question is whether candidate conditions ∧ ¬patch condition is satisfiable. Z3 computes the three results retained with this page.
Read the result precisely
SAT supplies a violating assignment within the encoded model. UNSAT means none exists within that model. Neither conclusion extends automatically to unmodeled program behavior.
The specification also allows partial and inconclusive outcomes. A timeout or ambiguous mapping does not establish either protection or vulnerability.
What is bounded?
This example uses integer lengths from 0 to 64. It is a direct constraint exercise, not the full SPES implementation. The specification’s program slices have a default depth of three, conditional extension to four, and explicit solver budgets.
The fingerprint drawing and this integer model explain two connected representations. The embedding vector is not simply passed to Z3 as a safety proof.
04 / Keep the records connected
The architecture and the contributions.
This study draws on Shadow Clone Jutsu v0.4r, especially pages 2–4, 14 and 15. It illustrates that specification rather than claiming every specified subsystem was used in the later F Prime investigations. The June source-code report and the later anomaly-scan contribution have their own methods and evidence.