Strojový překlad, nekontrolovaný rodilým mluvčím. Referenční je anglická verze.

Stránky druhů scénářůUpravit na GitHubuZdroj: docs/kinds/by-kind/spoof.md

spoof (druh scénáře)

Druh scénáře enginu v0.40.0, rodina Rušení, spoofing a spektrum. Pouze poradní charakter: výstup analýzy z výzkumného a inženýrského nástroje; nejde o typově schválené navigační zařízení ani o službu z oblasti bezpečnosti života. Každý štítek zde pochází z enginu nebo z verifikační matice; druh je MODELLED, pokud matice neuvádí jinak (jak se štítek získává: oddíl Evidence v README).

Co dělá#

Stochastický detektor časového spoofingu (Neyman–Pearson / χ²₁) s P_fa/P_md metodou Monte Carlo.

Jeden běh scenarios/spoof-attack.toml se shrnuje takto: scénář 2b6bd22c3b80 | spoof LinearRamp { rate_ns_per_s: 0,1 } oproti specifikaci 20,000 ns (P_fa 0,010) | kvantové zabezpečení 1,000 (P_md 0,000, MC 0,000) detekováno za 70s | klasické zabezpečení 0,558 (P_md 0,442, MC 0,444) detekováno za 430s

Vstupy#

Ze schématu (kshana kinds --json):

  • Povinná pole: threshold_ns, time, attack, clock_quantum, clock_classical
  • Volitelná pole: žádná

Příklad scenarios/spoof-attack.toml mimo jiné nastavuje:

Pole Hodnota Jednotka
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, datový list sigma_y(1s)=3e-10; q_ text
clock_classical.q_rw 0 neuvedeno
clock_classical.q_wf 9.0000e-20 neuvedeno
clock_classical.y0 5.0000e-10 neuvedeno
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 neuvedeno
clock_quantum.q_wf 1.0000e-30 neuvedeno
clock_quantum.y0 5.0000e-17 neuvedeno

Spusťte jej#

kshana scenarios/spoof-attack.toml

Tento druh používají 2 přibalené scénáře; ostatní jsou v scenarios/.

Co poskytuje#

Skalární výsledky tohoto běhu s jednotkami, které engine uvádí:

Výsledek Hodnota Jednotka
classical.breaches_spec_undetected true příznak
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 počet
classical.detection.monitor_sigma_ns 7.348481 ns
classical.detection.target_pfa 0.01 1
Graf, který engine zapisuje pro scenarios/spoof-attack.toml, druh spoof

Důkazy#

MODELLED: řádky verifikační matice, které tento druh jmenují.

  • MODELLED Sloučený bezpečnostní ukazatel kvality po epochách z χ² podporovaného hodinami, RAIM, AGC a SQM Testy: spoof_texbat_validation.rs.
  • MODELLED Sekce [spoofer] druhu leo-pass: spoofer padělá, vnitřně konzistentně v dosahu a rychlosti změny dosahu, signály viděné v deklarované poloze, která po nástupu skočí a/nebo je odtlačena od skutečné (pro každé pásmo LEO a pro MEO Testy: leo_resilience_verticals.rs.
  • MODELLED Pro každou družici LEO a dvojici měřicích pásem sekce [spoofer] vytvoří geometricky nezávislou kombinaci pseudovzdáleností, odstraní model ionosféry přijímače a testuje její krok mezi epochami proti kódovému šumu obou pásem a st Testy: leo_resilience_verticals.rs.

Řádky, které běh sám procvičil, s orákulem, které matice každému dává (veřejné zdroje jsou tam uvedeny):

  • MODELLED Hodinami podpořené χ², RAIM, AGC, SQM slučované do bezpečnostního FoM pro každou epochu. Oracle (ExternalDataset): parametry scénářů TEXBAT (Humphreys 2012) -- charakterizace, nikoli připnuté vektory. 0,30 vnější srovnání, zjištění (zůstává MODELLED): na JammerTest 2024 (Bleik; data GPL-3.0) monitory na úrovni pozorování (chí-kvadrát podpořený hodinami, RAIM, selhání řešení) nevyvolaly žádný alarm do 10 s od žádného z 8 vyhodnotitelných zveřejněných nástupů spoofingu (kde bylo okno před nástupem čisté, první alarm přišel 10,2 až 39 s po pu
  • MODELLED Deterministické, hashované po scénářích, brány SBOM a zlatých výsledků mezi platformami. Orákulum (ExternalDataset): shoda SBOM s oficiálním schématem JSON CycloneDX 1,5 (+ platné identifikátory SPDX) — externí publikovaný standard, nula chyb validace přes celý graf závislostí; část o determinismu FoM / bajtové reprodukovatelnosti zůstává zafixovanou kontrolou vlastní konzistence, takže řádek zůstává MODELLED

Omezení#

Co zpráva samotného běhu uvádí jako nemodelované nebo neověřené:

  • Detekce spoofingu je MODELLED, nikoli ověřena proti nezávislé vnější referenci: dílčí tvrzení je zkontrolováno externě, ale celá schopnost skládá dohromady části vypočtené z modelu, takže schopnost zůstává vypočtena z modelu. (verifikační matice (docs/MODELLED-RATIONALE.md))
  • Reprodukovatelnost a zajištění softwaru je MODELLED, nikoli ověřeno nezávislou referencí: dílčí tvrzení je externě zkontrolováno, ale celá schopnost skládá modelované části, takže schopnost zůstává vypočtená z modelu. (verifikační matice (docs/MODELLED-RATIONALE.md))

Viz také#