Maskinoversættelse, ikke gennemgået af en modersmålstalende. Engelsk er referencen.

Sider om scenarietyperRedigér på GitHubKilde: docs/kinds/by-kind/spoof.md

spoof (scenarietype)

Scenarietype i motoren v0.40.0, familie Jamming, spoofing og spektret. Vejledende: analyseoutput fra et forsknings- og ingeniørværktøj, ikke typegodkendt navigationsudstyr og ikke en sikkerhedskritisk tjeneste (safety-of-life). Hver mærkat her er motorens eller verifikationsmatrixens; en type er MODELLED, medmindre matrixen siger andet (hvordan en mærkat opnås: afsnittet Evidens i README).

Hvad det gør#

Stokastisk detektor for tidsspoofing (Neyman–Pearson / χ²₁) med Monte Carlo-P_fa/P_md.

Én kørsel af scenarios/spoof-attack.toml opsummeres som: scenarie 2b6bd22c3b80 | spoof LinearRamp { rate_ns_per_s: 0,1 } mod 20,000 ns spec (P_fa 0,010) | kvantesikkerhed 1,000 (P_md 0,000, MC 0,000) detekteret 70s | klassisk sikkerhed 0,558 (P_md 0,442, MC 0,444) detekteret 430s

Input#

Fra skemaet (kshana kinds --json):

  • Påkrævede felter: threshold_ns, time, attack, clock_quantum, clock_classical
  • Valgfrie felter: ingen

Eksemplet scenarios/spoof-attack.toml angiver blandt andet:

Felt Værdi Enhed
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-datablad sigma_y(1s)=3e-10; q_ tekst
clock_classical.q_rw 0 ikke angivet
clock_classical.q_wf 9.0000e-20 ikke angivet
clock_classical.y0 5.0000e-10 ikke angivet
clock_quantum.id optical-sr-lattice tekst
clock_quantum.provenance Strontium-optisk gitterur, rumorienteret mål sigma_y tekst
clock_quantum.q_rw 0 ikke angivet
clock_quantum.q_wf 1.0000e-30 ikke angivet
clock_quantum.y0 5.0000e-17 ikke angivet

Kør den#

kshana scenarios/spoof-attack.toml

2 medfølgende scenarier bruger denne type; de øvrige findes i scenarios/.

Hvad den giver#

De skalare resultater af den kørsel, med de enheder, motoren angiver:

Resultat Værdi Enhed
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 antal
classical.detection.monitor_sigma_ns 7.348481 ns
classical.detection.target_pfa 0.01 1
Diagrammet, som motoren skriver for scenarios/spoof-attack.toml, type spoof

Evidens#

MODELLED: rækkerne i verifikationsmatrixen, der nævner denne type.

  • MODELLED Urstøttet χ², RAIM, AGC, SQM, fusioneret kvalitetsmål for sikkerhed pr. epoke Tests: spoof_texbat_validation.rs.
  • MODELLED Afsnittet [spoofer] i typen leo-pass: en spoofer forfalsker, selvkonsistent i afstand og afstandsændring, de signaler, der ses ved en angiven position, som springer og/eller skubbes væk fra den sande efter et indsættelsestidspunkt (pr. LEO-bånd og for MEO Tests: leo_resilience_verticals.rs.
  • MODELLED For hver LEO-satellit og hvert par af afstandsbånd danner afsnittet [spoofer] den geometrifrie pseudoafstandskombination, fjerner modtagerens ionosfæremodel og tester dens trin fra epoke til epoke mod de to båndes kodestøj og en st Tests: leo_resilience_verticals.rs.

De rækker, som kørslen selv afprøvede, med den uafhængige reference, som matrixen giver hver (de offentlige kilder er nævnt dér):

  • MODELLED Urstøttet χ², RAIM, AGC, SQM sammenlagt sikkerhedskvalitetsmål pr. epoke. Uafhængig reference (ExternalDataset): TEXBAT-scenarieparametre (Humphreys 2012) — karakterisering, ikke fastlåste vektorer. 0,30 ekstern sammenligning, et fund (forbliver MODELLED): på JammerTest 2024 (Bleik; GPL-3.0-data) udløste monitorerne på observabelniveau (urstøttet chi-i-anden, RAIM, løsningsfejl) ingen alarm inden for 10 s af nogen af de 8 evaluerbare publicerede spoofing-starter (hvor vinduet før starten var rent, kom den første alarm 10,2 til 39 s efter pu
  • MODELLED Deterministisk, scenarie-hashet, SBOM + gates med golden-filer på tværs af platforme. Uafhængig reference (ExternalDataset): SBOM'ens validering mod det officielle CycloneDX 1,5 JSON-skema (+ gyldige SPDX-identifikatorer) — en ekstern publiceret standard, nul valideringsfejl over hele afhængighedsgrafen; den del, der gælder FoM-determinisme / byte-reproducerbarhed, er fortsat et fastlåst selvkonsistenstjek, så rækken forbliver MODELLED

Begrænsninger#

Hvad kørslens egen rapport siger ikke er modelleret eller ikke er valideret:

  • Detektion af spoofing er MODELLED, ikke valideret: en delpåstand kontrolleres eksternt, men hele funktionen sammensættes af modellerede dele, så funktionen forbliver modelleret. (verifikationsmatrix (docs/MODELLED-RATIONALE.md))
  • Reproducerbarhed og softwarekvalitetssikring er MODELLED, ikke valideret: en delpåstand kontrolleres eksternt, men hele funktionen sammensættes af modellerede dele, så funktionen forbliver modelleret. (verifikationsmatrix (docs/MODELLED-RATIONALE.md))

Se også#