Scenario kind pagesEdit on GitHubSource: docs/kinds/by-kind/spoof.md

spoof (scenario kind)

Scenario kind of the engine v0.38.0, family Jamming, spoofing and the spectrum. Advisory: analysis output from a research and engineering tool, not type-approved navigation equipment and not a safety-of-life service. Every label here is the engine's or the verification matrix's; a kind is MODELLED unless the matrix says otherwise (how a label is earned: the README's Evidence section).

What it does#

Stochastic time-spoof detector (Neyman–Pearson / χ²₁) with Monte-Carlo P_fa/P_md.

One run of scenarios/spoof-attack.toml summarises as: scenario 2b6bd22c3b80 | spoof LinearRamp { rate_ns_per_s: 0.1 } vs 20.000 ns spec (P_fa 0.010) | quantum security 1.000 (P_md 0.000, MC 0.000) detected 70s | classical security 0.558 (P_md 0.442, MC 0.444) detected 430s

Inputs#

From the schema (kshana kinds --json):

  • Required fields: threshold_ns, time, attack, clock_quantum, clock_classical
  • Optional fields: none

The example scenarios/spoof-attack.toml sets, among others:

Field Value Unit
attack.rate_ns_per_s 0.1 s
attack.start_s 60 s
clock_classical.id csac-sa45s text
clock_classical.provenance Microchip SA65 / SA.45s CSAC datasheet sigma_y(1s)=3e-10; q_ text
clock_classical.q_rw 0 not stated
clock_classical.q_wf 9.0000e-20 not stated
clock_classical.y0 5.0000e-10 not stated
clock_quantum.id optical-sr-lattice text
clock_quantum.provenance Strontium optical lattice clock, space-oriented goal sigma_y text
clock_quantum.q_rw 0 not stated
clock_quantum.q_wf 1.0000e-30 not stated
clock_quantum.y0 5.0000e-17 not stated

Run it#

kshana scenarios/spoof-attack.toml

2 bundled scenarios use this kind; the others are in scenarios/.

What it gives#

The scalar results of that run, with the units the engine states:

Result Value Unit
classical.breaches_spec_undetected true flag
classical.detect_time_s 430 s
classical.detection.analytic_pmd 0.442031 1
classical.detection.boundary_ns 18.928432 ns
classical.detection.eval_offset_ns 20 ns
classical.detection.mc_pfa 0.0088 1
classical.detection.mc_pmd 0.4439 1
classical.detection.mc_runs 10000 count
classical.detection.monitor_sigma_ns 7.348481 ns
classical.detection.target_pfa 0.01 1
The chart the engine writes for scenarios/spoof-attack.toml, kind spoof

Evidence#

MODELLED: the verification matrix rows that name this kind.

  • MODELLED Clock-aided χ², RAIM, AGC, SQM fused per-epoch security FoM Tests: spoof_texbat_validation.rs.
  • MODELLED The leo-pass kind's [spoofer] section: a spoofer counterfeits, self-consistently in range and range rate, the signals seen at a claimed position that jumps and/or is pushed from the true one after an onset (per LEO band and for the MEO Tests: leo_resilience_verticals.rs.
  • MODELLED For every LEO satellite and pair of ranging bands the [spoofer] section forms the geometry-free pseudorange combination, removes the receiver's ionospheric model and tests its epoch-to-epoch step against the two bands' code noise and a st Tests: leo_resilience_verticals.rs.

The rows the run itself exercised, with the oracle the matrix gives each (the public sources are named there):

  • MODELLED Clock-aided χ², RAIM, AGC, SQM fused per-epoch security FoM. Oracle (ExternalDataset): TEXBAT scenario parameters (Humphreys 2012) — characterisation, not pinned vectors. 0.30 external comparison, a finding (stays MODELLED): on JammerTest 2024 (Bleik; GPL-3.0 data) the observable-level monitors (clock-aided chi-square, RAIM, solve failure) raised no alarm within 10 s of any of the 8 evaluable published spoofing onsets (where the pre-onset window was clean, the first alarm came 10.2 to 39 s after the pu
  • MODELLED Deterministic, scenario-hashed, SBOM + cross-platform golden gates. Oracle (ExternalDataset): SBOM conformance to the official CycloneDX 1.5 JSON Schema (+ valid SPDX identifiers) — an external published standard, zero validation errors over the full dependency graph; the FoM-determinism / byte-reproducibility part remains a pinned self-consistency check, so the row stays MODELLED

Limitations#

What the run's own report says is not modelled or not validated:

  • Spoofing detection is MODELLED, not validated: a sub-claim is externally checked, but the whole capability composes modelled pieces, so the capability stays Modelled. (verification matrix (docs/MODELLED-RATIONALE.md))
  • Reproducibility & software assurance is MODELLED, not validated: a sub-claim is externally checked, but the whole capability composes modelled pieces, so the capability stays Modelled. (verification matrix (docs/MODELLED-RATIONALE.md))

See also#