Tradução automática, não revista por um falante nativo. O inglês é a referência.

Páginas de tipos de cenárioEditar no GitHubFonte: docs/kinds/by-kind/spoof.md

spoof (tipo de cenário)

Tipo de cenário do motor v0.40.0, família Jamming, spoofing e o espectro. Consultivo: saída de análise de uma ferramenta de pesquisa e engenharia, não um equipamento de navegação homologado e não um serviço de segurança da vida humana. Todo rótulo aqui é do motor ou da matriz de verificação; um tipo de cenário é MODELLED, a menos que a matriz diga outra coisa (como um rótulo é conquistado: a seção Evidence do README).

O que faz#

Detector estocástico de spoofing de tempo (Neyman–Pearson / χ²₁) com P_fa/P_md de Monte Carlo.

Uma execução de scenarios/spoof-attack.toml resume-se assim: cenário 2b6bd22c3b80 | spoof LinearRamp { rate_ns_per_s: 0,1 } contra especificação de 20,000 ns (P_fa 0,010) | segurança quântica 1,000 (P_md 0,000, MC 0,000) detectado em 70s | segurança clássica 0,558 (P_md 0,442, MC 0,444) detectado em 430s

Entradas#

A partir do esquema (kshana kinds --json):

  • Campos obrigatórios: threshold_ns, time, attack, clock_quantum, clock_classical
  • Campos opcionais: nenhum

O exemplo scenarios/spoof-attack.toml define, entre outros:

Campo Valor Unidade
attack.rate_ns_per_s 0.1 s
attack.start_s 60 s
clock_classical.id csac-sa45s texto
clock_classical.provenance Folha de dados do CSAC Microchip SA65 / SA.45s sigma_y(1s)=3e-10; q_ texto
clock_classical.q_rw 0 não indicado
clock_classical.q_wf 9.0000e-20 não indicado
clock_classical.y0 5.0000e-10 não indicado
clock_quantum.id optical-sr-lattice texto
clock_quantum.provenance Relógio óptico de rede de estrôncio, meta para uso espacial sigma_y texto
clock_quantum.q_rw 0 não indicado
clock_quantum.q_wf 1.0000e-30 não indicado
clock_quantum.y0 5.0000e-17 não indicado

Execute#

kshana scenarios/spoof-attack.toml

2 cenários incluídos usam este tipo de cenário; os demais estão em scenarios/.

O que ele fornece#

Os resultados escalares dessa execução, com as unidades que o motor declara:

Resultado Valor Unidade
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 contagem
classical.detection.monitor_sigma_ns 7.348481 ns
classical.detection.target_pfa 0.01 1
O gráfico que o mecanismo gera para scenarios/spoof-attack.toml, tipo spoof

Evidências#

MODELLED: as linhas da matriz de verificação que nomeiam este tipo de cenário.

  • MODELLED χ² auxiliado pelo relógio, RAIM, AGC, SQM fundidos em uma FoM de segurança por época Testes: spoof_texbat_validation.rs.
  • MODELLED A seção [spoofer] do tipo leo-pass: um spoofer falsifica, de forma autoconsistente em distância e taxa de distância, os sinais vistos em uma posição declarada que salta e/ou é deslocada da verdadeira após um instante inicial (por banda LEO e para o MEO Testes: leo_resilience_verticals.rs.
  • MODELLED Para cada satélite LEO e par de bandas de medição de distância, a seção [spoofer] forma a combinação de pseudodistância livre de geometria, remove o modelo ionosférico do receptor e testa seu salto de época a época contra o ruído de código das duas bandas e um Testes: leo_resilience_verticals.rs.

As linhas que a própria execução exercitou, com a referência independente que a matriz dá a cada uma (as fontes públicas são nomeadas ali):

  • MODELLED χ² auxiliado pelo relógio, RAIM, AGC e SQM fundidos em uma figura de mérito de segurança por época. Referência independente (ExternalDataset): parâmetros de cenário do TEXBAT (Humphreys 2012) — caracterização, não vetores fixados. Comparação externa 0,30, um achado (permanece MODELLED): no JammerTest 2024 (Bleik; dados GPL-3.0) os monitores em nível de observável (qui-quadrado auxiliado pelo relógio, RAIM, falha de solução) não levantaram alarme em até 10 s de nenhum dos 8 inícios de spoofing publicados avaliáveis (onde a janela anterior ao início estava limpa, o primeiro alarme veio de 10,2 a 39 s após o pu
  • MODELLED Portões determinísticos, com hash de cenário, de SBOM e de golden entre plataformas. Referência independente (ExternalDataset): aderência à norma do SBOM ao JSON Schema oficial do CycloneDX 1,5 (+ identificadores SPDX válidos) — um padrão externo publicado, zero erros de validação em todo o grafo de dependências; a parte de determinismo das FoMs / reprodutibilidade byte a byte continua sendo uma verificação de autoconsistência fixada, de modo que a linha permanece MODELLED

Limitações#

O que o próprio relatório da execução diz que não é modelado ou não é validado:

  • A detecção de spoofing é MODELLED, não validada: uma subafirmação é conferida externamente, mas a capacidade inteira compõe peças modeladas, de modo que a capacidade permanece modelada. (matriz de verificação (docs/MODELLED-RATIONALE.md))
  • Reprodutibilidade e garantia de software é MODELLED, não validada: uma subafirmação é verificada externamente, mas a capacidade inteira compõe peças modeladas, de modo que a capacidade permanece modelada. (matriz de verificação (docs/MODELLED-RATIONALE.md))

Veja também#