Машинный перевод, не проверенный носителем языка. Эталоном служит английская версия.

Страницы видов сценариевПравить на GitHubИсточник: docs/kinds/by-kind/spoof.md

spoof (вид сценария)

Вид сценария движка v0.40.0, семейство Подавление, спуфинг и спектр. Носит консультативный характер: результат анализа исследовательского и инженерного инструмента; это не навигационное оборудование с утверждённым типом и не служба обеспечения безопасности жизни. Все обозначения здесь принадлежат движку или матрице верификации; вид относится к уровню MODELLED, если матрица не указывает иное (как заслуживается обозначение: раздел Evidence в README).

Что делает#

Стохастический детектор спуфинга времени (Неймана–Пирсона / χ²₁) с P_fa/P_md по методу Монте-Карло.

Один прогон scenarios/spoof-attack.toml сводится к следующему: сценарий 2b6bd22c3b80 | спуфинг LinearRamp { rate_ns_per_s: 0,1 } против спецификации 20,000 ns (P_fa 0,010) | безопасность квантовой системы 1,000 (P_md 0,000, MC 0,000) обнаружено за 70s | безопасность классической системы 0,558 (P_md 0,442, MC 0,444) обнаружено за 430s

Входные параметры#

Из схемы (kshana kinds --json):

  • Обязательные поля: threshold_ns, time, attack, clock_quantum, clock_classical
  • Необязательные поля: нет

В примере scenarios/spoof-attack.toml среди прочего задано:

Поле Значение Единица
attack.rate_ns_per_s 0.1 s
attack.start_s 60 s
clock_classical.id csac-sa45s текст
clock_classical.provenance Microchip SA65 / SA.45s CSAC datasheet sigma_y(1s)=3e-10; q_ текст
clock_classical.q_rw 0 не указано
clock_classical.q_wf 9.0000e-20 не указано
clock_classical.y0 5.0000e-10 не указано
clock_quantum.id optical-sr-lattice текст
clock_quantum.provenance Strontium optical lattice clock, space-oriented goal sigma_y текст
clock_quantum.q_rw 0 не указано
clock_quantum.q_wf 1.0000e-30 не указано
clock_quantum.y0 5.0000e-17 не указано

Запустите#

kshana scenarios/spoof-attack.toml

Этот вид используют 2 поставляемых сценария; остальные находятся в scenarios/.

Что он даёт#

Скалярные результаты этого прогона с единицами, которые указывает движок:

Результат Значение Единица
classical.breaches_spec_undetected true флаг
classical.detect_time_s 430 s
classical.detection.analytic_pmd 0.442031 1
classical.detection.boundary_ns 18.928432 нс
classical.detection.eval_offset_ns 20 нс
classical.detection.mc_pfa 0.0088 1
classical.detection.mc_pmd 0.4439 1
classical.detection.mc_runs 10000 число
classical.detection.monitor_sigma_ns 7.348481 нс
classical.detection.target_pfa 0.01 1
График, который движок строит для scenarios/spoof-attack.toml, вид spoof

Доказательства#

MODELLED: строки матрицы верификации, называющие этот вид.

  • MODELLED χ² с использованием часов, RAIM, AGC, SQM — объединённый показатель качества безопасности по эпохам Тесты: spoof_texbat_validation.rs.
  • MODELLED Раздел [spoofer] вида leo-pass: спуфер подделывает, самосогласованно по дальности и скорости изменения дальности, сигналы, наблюдаемые в заявленном положении, которое скачком и/или сдвигом отклоняется от истинного после момента начала (для каждого диапазона LEO и для MEO Тесты: leo_resilience_verticals.rs.
  • MODELLED Для каждого спутника LEO и пары дальномерных диапазонов раздел [spoofer] образует безгеометрическую комбинацию псевдодальностей, удаляет ионосферную модель приёмника и проверяет её скачок от эпохи к эпохе относительно кодовых шумов двух диапазонов и st Тесты: leo_resilience_verticals.rs.

Строки, которые задействовал сам прогон, с оракулом, который указывает им матрица (публичные источники названы там):

  • MODELLED Объединённый посчётный показатель безопасности по эпохам: χ² с привлечением часов, RAIM, AGC, SQM. Oracle (ExternalDataset): параметры сценариев TEXBAT (Humphreys 2012) — характеристика, а не зафиксированные векторы. 0,30 внешнее сравнение, результат (остаётся MODELLED): на JammerTest 2024 (Bleik; данные под GPL-3.0) мониторы на уровне наблюдаемых (хи-квадрат с привлечением часов, RAIM, сбой решения) не подали тревоги в пределах 10 s ни при одном из 8 поддающихся оценке опубликованных начал спуфинга (где окно до начала было чистым, первая тревога приходила через 10,2–39 s после pu
  • MODELLED Детерминированные, хешируемые по сценарию, SBOM и кроссплатформенные эталонные проверки (golden). Оракул (ExternalDataset): соответствие SBOM официальной схеме JSON CycloneDX 1,5 (плюс допустимые идентификаторы SPDX) — внешний опубликованный стандарт, ноль ошибок валидации на всём графе зависимостей; часть о детерминизме FoM и побайтной воспроизводимости остаётся закреплённой проверкой внутренней согласованности, поэтому строка остаётся MODELLED

Ограничения#

Что отчёт самого прогона называет не смоделированным или не проверенным:

  • Обнаружение спуфинга — MODELLED, а не validated: одно из частных утверждений проверено внешне, но вся возможность составлена из смоделированных частей, поэтому остаётся Modelled. (матрица верификации (docs/MODELLED-RATIONALE.md))
  • Воспроизводимость и гарантии качества ПО — MODELLED, а не validated: одно из частных утверждений проверено извне, но вся возможность составлена из смоделированных частей, поэтому возможность остаётся Modelled. (матрица верификации (docs/MODELLED-RATIONALE.md))

См. также#