Machinevertaling, niet beoordeeld door een moedertaalspreker. Engels is de referentie.

Pagina's per scenariotypeBewerken op GitHubBron: docs/kinds/by-kind/spoof.md

spoof (scenariosoort)

Scenariosoort van de engine v0.40.0, familie Jamming, spoofing en het spectrum. Adviserend: uitvoer van een analyse door een onderzoeks- en engineeringhulpmiddel, geen typegoedgekeurde navigatieapparatuur en geen safety-of-life-dienst. Elk label hier is van de engine of van de verificatiematrix; een soort is MODELLED tenzij de matrix anders vermeldt (hoe een label wordt verdiend: de sectie Evidence van de README).

Wat het doet#

Stochastische detector voor tijdspoofing (Neyman–Pearson / χ²₁) met Monte-Carlo P_fa/P_md.

Eén run van scenarios/spoof-attack.toml vat samen als: scenario 2b6bd22c3b80 | spoof LinearRamp { rate_ns_per_s: 0,1 } tegenover 20,000 ns spec (P_fa 0,010) | quantum-beveiliging 1,000 (P_md 0,000, MC 0,000) gedetecteerd 70s | klassieke beveiliging 0,558 (P_md 0,442, MC 0,444) gedetecteerd 430s

Invoer#

Uit het schema (kshana kinds --json):

  • Verplichte velden: threshold_ns, time, attack, clock_quantum, clock_classical
  • Optionele velden: geen

Het voorbeeld scenarios/spoof-attack.toml stelt onder meer in:

Veld Waarde Eenheid
attack.rate_ns_per_s 0.1 s
attack.start_s 60 s
clock_classical.id csac-sa45s tekst
clock_classical.provenance Microchip SA65 / SA.45s CSAC-datasheet sigma_y(1s)=3e-10; q_ tekst
clock_classical.q_rw 0 niet vermeld
clock_classical.q_wf 9.0000e-20 niet vermeld
clock_classical.y0 5.0000e-10 niet vermeld
clock_quantum.id optical-sr-lattice tekst
clock_quantum.provenance Optische strontiumroosterklok, op de ruimte gericht doel sigma_y tekst
clock_quantum.q_rw 0 niet vermeld
clock_quantum.q_wf 1.0000e-30 niet vermeld
clock_quantum.y0 5.0000e-17 niet vermeld

Uitvoeren#

kshana scenarios/spoof-attack.toml

2 meegeleverde scenario's gebruiken dit kind; de overige staan in scenarios/.

Wat het oplevert#

De scalaire resultaten van die run, met de eenheden die de engine noemt:

Resultaat Waarde Eenheid
classical.breaches_spec_undetected true vlag
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 aantal
classical.detection.monitor_sigma_ns 7.348481 ns
classical.detection.target_pfa 0.01 1
De grafiek die de engine schrijft voor scenarios/spoof-attack.toml, soort spoof

Bewijs#

MODELLED: de rijen van de verificatiematrix die dit type noemen.

  • MODELLED Klokondersteunde χ², RAIM, AGC, SQM, gefuseerd tot een beveiligingskwaliteitsmaat per epoch Tests: spoof_texbat_validation.rs.
  • MODELLED De sectie [spoofer] van de soort leo-pass: een spoofer vervalst, zelfconsistent in afstand en afstandssnelheid, de signalen die worden gezien op een geclaimde positie die springt en/of na een aanvang van de ware positie wordt weggeduwd (per LEO-band en voor de MEO Tests: leo_resilience_verticals.rs.
  • MODELLED Voor elke LEO-satelliet en elk paar afstandsmetingsbanden vormt de sectie [spoofer] de geometrievrije pseudoafstandscombinatie, verwijdert het ionosfeermodel van de ontvanger en toetst de stap van epoch tot epoch ervan tegen de coderuis van de twee banden en een st Tests: leo_resilience_verticals.rs.

De rijen die de run zelf heeft beproefd, met de onafhankelijke referentie die de matrix aan elk geeft (de openbare bronnen worden daar genoemd):

  • MODELLED Klokondersteunde χ², RAIM, AGC, SQM, per tijdstip gefuseerde veiligheidskwaliteitsmaat. Onafhankelijke referentie (ExternalDataset): TEXBAT-scenarioparameters (Humphreys 2012) — karakterisering, geen vastgezette vectoren. 0,30 externe vergelijking, een bevinding (blijft MODELLED): op JammerTest 2024 (Bleik; GPL-3.0-data) gaven de monitors op waarnemingsniveau (klokondersteunde chikwadraat, RAIM, oplossingsfout) geen alarm binnen 10 s van een van de 8 evalueerbare gepubliceerde spoofingbegintijden (waar het venster vóór het begin schoon was, kwam het eerste alarm 10,2 tot 39 s na de pu
  • MODELLED Deterministisch, scenario-gehasht, SBOM + gouden poorten voor meerdere platforms. Onafhankelijke referentie (ExternalDataset): formaatcontrole van de SBOM tegen het officiële CycloneDX 1,5 JSON Schema (+ geldige SPDX-identificatoren) — een externe gepubliceerde standaard, nul validatiefouten over de volledige afhankelijkheidsgraaf; het onderdeel determinisme van de FoM en byte-reproduceerbaarheid blijft een vastgepinde zelfconsistentiecontrole, dus de rij blijft MODELLED

Beperkingen#

Wat het eigen rapport van de run zegt dat niet is gemodelleerd of niet extern getoetst is:

  • Spoofingdetectie is MODELLED, niet extern getoetst: een deelclaim wordt extern gecontroleerd, maar de hele mogelijkheid is samengesteld uit gemodelleerde onderdelen, dus de mogelijkheid blijft gemodelleerd. (verificatiematrix (docs/MODELLED-RATIONALE.md))
  • Reproduceerbaarheid en softwarewaarborging is MODELLED, niet extern getoetst: een deelclaim wordt extern gecontroleerd, maar de hele mogelijkheid is samengesteld uit gemodelleerde onderdelen, dus de mogelijkheid blijft gemodelleerd. (verificatiematrix (docs/MODELLED-RATIONALE.md))

Zie ook#