Проблема: почему анализ систем — это боль

Представьте, что у вас есть система, которая может находиться в разных состояниях.

Вот примеры из реальной жизни:

  • Банк — состояние: обычный пользователь, оператор, администратор

  • Автопилот БПЛА — состояние: взлёт, набор высоты, патрулирование, возврат, авария

  • Сетевое соединение — состояние: установка связи, передача данных, ошибка, закрытие

  • Смарт-контракт — состояние: ожидание, выполнение, заблокирован

  • Лифт в небоскрёбе — состояние: этаж, открыты/закрыты двери, есть ли вызовы

Главный вопрос, который постоянно нужно задавать:

«Если система сейчас в состоянии X, может ли она когда-нибудь попасть в состояние Y?»

Зачем это нужно знать:

  • Банку — может ли пользователь получить права администратора? (взлом безопасности)

  • Атомной станции — может ли реактор попасть в опасный режим? (предотвращение катастрофы)

  • БПЛА — может ли миссия войти в аварийный цикл? (спасение дрона)

  • Смарт-контракту — можно ли навсегда заблокировать средства? (аудит безопасности)

В чём проблема:

Состояний может быть миллионы, миллиарды. Каждый раз запускать поиск в ширину (BFS) или глубину (DFS) — слишком долго. А если нужно задать миллион таких вопросов? А если система меняется в реальном времени?

Как решают сегодня (классический подход):

// Классика: BFS из начального состояния
bool CanReachBad(int start, bool[] bad, int[][] graph)
{
    var queue = new Queue<int>();
    var visited = new bool[n];
    queue.Enqueue(start);
    visited[start] = true;
    
    while (queue.Count > 0)
    {
        int u = queue.Dequeue();
        if (bad[u]) return true;
        foreach (int v in graph[u])
            if (!visited[v])
            {
                visited[v] = true;
                queue.Enqueue(v);
            }
    }
    return false;
}
// Для каждого запроса — новый BFS (очень медленно!)
foreach (var start in thousandQueries)
{
    bool answer = CanReachBad(start, badStates, graph);
}

Сложность: O(Q × (V+E)). Для миллиона запросов на графе из миллиона вершин — это миллиарды операций.

Идея: а что если один раз всё предвычислить?

Мы рассуждали так:

Если система детерминированная (из каждого состояния ровно один переход), то можно предвычислить таблицы прыжков — как в быстром возведении в степень, но для переходов между состояниями.

Тогда вопрос «где будет система через N шагов?» решается за O(log N) вместо O(N). Ускорение — тысячи раз.

Если система недетерминированная (из состояния несколько выходов), то можно один раз построить обратный индекс достижимости — как поисковый индекс Google, только для графов состояний.

Тогда миллионы запросов «достижимо ли B из A?» отвечаются за O(1) — просто проверкой массива.

Аналогия из жизни:

Без предвычисления — как искать книгу в библиотеке, каждый раз проходя между рядами и просматривая каждую полку.

С предвычислением — как Google: один раз проиндексировали все книги, а потом поиск занимает доли секунды.

Что получилось: платформа SymFSM

Мы построили платформу, которая умеет:

  1. Принимать на вход любую дискретную систему — протокол, программу, робота, БПЛА, цифровой двойник

  2. Строить индекс — один раз, тяжело (секунды для миллионов состояний)

  3. Отвечать на вопросы — миллионы раз, легко (наносекунды)

Типы вопросов:

Тип

Что спрашиваем

Сложность

Reach(A,B)

Можно ли попасть из A в B?

O(1)

Distance(A,B)

За сколько шагов?

O(log N)

Attractor(A)

В какой цикл попадёт система?

O(1)

Future(A,N)

Где будет система через N шагов?

O(log N)

Как это выглядит в коде:

// Клиент загружает автомат
var e = new SymFsmEngine(stateCount, symbolCount);
e.SetTransitionTable(symbol, transitions);
e.BuildJumpTables(24);  // один раз построили индекс
// Анализ достижимости (недетерминированный случай)
var ra = new ReachabilityAnalyzer(succ);
bool[] canReachBad = ra.ReverseReachable(badStates);
// Миллионы запросов — мгновенно
foreach (var start in queries)
{
    bool dangerous = canReachBad[start];  // O(1) — наносекунды!
    int distance = dist[start];
}

Как мы тестировали: не синтетика, а реальные системы

Мы не использовали случайные графы — они могут давать завышенные результаты. Вместо этого мы взяли реальные системы из промышленности:

  • Протоколы: TLS 1.3, QUIC (HTTP/3), HTTP/2, OPC-UA (промстандарт), MQTT (IoT)

  • Алгоритмы синхронизации: Peterson, Bakery, Обедающие философы (классика OS)

  • Кибербезопасность: Snort (100 000 сигнатур), Suricata, CFG вредоносного ПО

  • Компиляторы: DFA регулярных выражений, LR/LALR парсеры, лексеры

  • Робототехника: мобильные роботы, манипуляторы, складские рои

  • БПЛА: миссии дронов, рои из 10 000 дронов, перехват целей

  • Оборона: многоэшелонированная ПВО, радиолокация, РЭБ

  • Цифровые двойники: энергосети, ж/д сети, заводы

Всего — 47 бенчмарков, от 5 состояний (MQTT) до 4.8 миллионов состояний (14 философов).

Результаты тестирования

Первые тесты (без RaaS)

Мы начали с простых вещей — проверили ускорение на классических задачах: DFA, Aho-Corasick, сетевые протоколы, Game of Life.

Вот что получилось:

Направление

Что делали

Ускорение

DFA / Regex (F^16M)

16 млн шагов вперёд

x616 028

Game of Life 4×4 (F^16M)

16 млн поколений

x444 558

Сетевые протоколы (F^1M)

миллион тактов симуляции

x67 442

Aho-Corasick (100k сигн.)

поиск по автомату

x3 987

Model Checking

анализ всех циклов

x249

Reachability (BFS vs reverse)

проверка достижимости

x23 556

Ключевые выводы первых тестов:

  • Детерминированные системы (DFA, Life, протоколы) ускоряются в сотни тысяч раз за счёт jump-таблиц

  • Недетерминированные системы (reachability) ускоряются в десятки тысяч раз за счёт амортизации

  • Даже на малых размерах (Aho-Corasick, парсеры) ускорение стабильно держится на уровне тысяч раз

Оборонные и аэрокосмические системы

Мы подумали: а что если проверить на том, где каждая миллисекунда на счету? Взяли автопилот БПЛА, системы ПВО, рои дронов.

Результаты:

Направление

Что проверяли

Ускорение

Вердикт

Автопилот БПЛА (F^16M)

посадка через 16 млн шагов

x1 385 382

посадка достижима ✅

Анализ миссий UAV

262 тыс. конфигураций

x174

132 зацикленных миссии ⚠️

Рой роботов

131 тыс. конфигураций

x74

1 deadlock, 69 livelock ⚠️

Радиоканал (потеря связи)

50 тыс. состояний

x26 160

потеря связи из 100% 🔴

Промышленный PLC

40 тыс. состояний

x125 391

авария из 100% 🔴

Космический аппарат

128 состояний

x10

SAFE MODE из 100% ✅

Радарное сопровождение

65 тыс. конфигураций

x125

44 цикла потери трека ⚠️

Что это значит для оборонки:

SymFSM позволяет за миллисекунды доказывать безопасность систем, где раньше требовались часы и дни верификации. Автопилот БПЛА — безопасен (посадка достижима). Радиоканал — опасен (потеря связи из любого состояния). Промышленный контроллер — опасен (авария из любого состояния).

Код проверки автопилота:

// Построение модели автопилота (64 состояния)
var flightController = BuildFlightControllerModel();
var fsm = new SymFsmEngine(64, 1);
fsm.SetTransitionTable(0, flightController);
fsm.BuildJumpTables(24);
// Проверка: достижима ли посадка через 16 млн шагов?
int state = 0;  // INIT
int finalState = fsm.Jump(0, 16_777_216, 0);
bool landingReachable = (finalState & 7) == 7;  // DONE = 7

Сенсорные и трекинговые системы

Потом проверили системы, которые следят за целями — радары, сенсорная интеграция, обнаружение роев.

Результаты:

Направление

Что делали

Ускорение

Вердикт

Multi-Sensor Track (F^16M)

16 млн шагов трека

x469 726

51.6% треков теряются

Радарное управление треком

анализ всех состояний

x99

5 циклических режимов

Сенсорная интеграция (R/EO/IR/RF)

проверка ложных треков

x58

ложный трек из 9%

Обнаружение роя (10 млн дронов)

предсказание распределения

x106 587

рой распределяется по 8 фазам

Классификация траекторий

262 тыс. траекторий

x417

10 устойчивых, 158 неустойчивых

Раннее предупреждение

анализ ложных тревог

x24 062

ложная тревога из 100% 🔴

Распределённая сеть

131 тыс. конфигураций

x348

10 отказовых, 151 восстановление

Код предсказания роя дронов:

// Построение модели роя (1 млн дронов)
var swarmModel = BuildSwarmModel(1_000_000);
var fsm = BuildFN(swarmModel, 20);
// Распределение после миллиона тактов
var distribution = new int[8];
for (int i = 0; i < 100000; i++)
{
    int startState = random.Next(1_000_000);
    int finalState = fsm.Jump(startState, 1_000_000, 0);
    distribution[finalState & 7]++;  // 3 бита фазы
}
// Результат: ph0:18%, ph1:16%, ph2:11%, ph3:8%, ph4:6%, ph5:10%, ph6:14%, ph7:16%

Reachability-as-a-Service (RaaS) — главный результат

И вот тут началось самое интересное. Мы поняли, что платформа может больше, чем просто ускорять отдельные задачи. Она может стать сервисом, который отвечает на любые вопросы о будущем системы.

Что такое RaaS:

Облачная платформа, которая принимает на вход граф состояний (FSM, протокол, программу, робота, БПЛА), один раз строит индекс, а затем отвечает на миллиарды запросов о достижимости, расстоянии, аттракторах и будущем состоянии.

Четыре типа запросов, которые поддерживает RaaS:

Запрос

Что спрашиваем

Пример

Reach(A,B)

Можно ли попасть из A в B?

«Может ли пользователь стать админом?»

Distance(A,B)

За сколько шагов?

«Через сколько тактов робот столкнётся?»

Attractor(A)

В какой цикл попадёт система?

«Закрутится ли дрон?»

Future(A,N)

Где будет система через N шагов?

«Где будет БПЛА через час?»

Код RaaS для клиента:

// Клиент загружает автомат (1 млн состояний)
var e = new SymFsmEngine(stateCount, symbolCount);
e.SetTransitionTable(symbol, transitions);
e.BuildJumpTables(24);  // один раз построили индекс
// Анализ достижимости (недетерминированный случай)
var ra = new ReachabilityAnalyzer(succ);
bool[] canReachBad = ra.ReverseReachable(badStates);
int[] distanceToBad = ra.ReverseDistance(badStates);
// Миллионы запросов — наносекунды
foreach (var start in millionQueries)
{
    bool dangerous = canReachBad[start];
    int steps = distanceToBad[start];
    var attractor = e.GetAttractor(start, 0);
    int future = e.Jump(start, 1_000_000_000_000L, 0);
}

Результаты RaaS-тестирования (47 бенчмарков):

A. Ядро RaaS (масштабируемость)

Бенчмарк

Состояний

Ускорение

Пропускная способность

Динамическая смена цели

1 млн

x123 430

108 млн q/с

База данных достижимости

1 млн

x122 457

166 млн q/с

Динамический Unsafe Atlas

1 млн

x207 594

186 млн q/с

B. Model Checking (SPIN) — верификация алгоритмов

Алгоритм

Состояний

Ускорение

Вердикт

Peterson (8 проц.)

390 625

x301

нарушение из 100%

Dining Philosophers (12)

531 441

x270 796

deadlock из 100%

Dining Philosophers (13)

1.59 млн

x693 044

deadlock из 100%

Dining Philosophers (14)

4.78 млн

x1 377 723

deadlock из 100%

Producer-Consumer

100 003

x124 443

overflow из 100%

Elevator Controller

768

x2 612

безопасен ✅

C. Сетевые протоколы

Протокол

Состояний

Ускорение

Вердикт

TLS 1.3

13

x17

ERROR из 92%

QUIC

7

x32

LOST из 71%

HTTP/2

7

x15

deadlock из 86%

OPC-UA

12

x26

Faulted из 100%

MQTT

5

x24

session loss из 100%

D. Кибербезопасность

Система

Состояний

Ускорение

Вердикт

Snort IDS (100k сигн.)

303 088

x50 159

alert из 100%

Suricata (100k сигн.)

377 565

x107 353

alert из 100%

Malware CFG

500 000

x218 605

payload из 100%

Exploit RCE

500 000

x1 192 953

RCE из 100%

Binary Vuln Atlas

1 млн

x34 091

уязвимость из 100%

E. Компиляторы

Система

Размер

Ускорение

Вердикт

Regex DFA (F^16M)

1 млн

x910 462

91 нс вместо 90 мс

LR/LALR парсер

100 000

x146 175

ошибка из 100%

Lexer Reachability

50 000

x991 990

все токены достижимы ✅

F. Программный код (CFG, LLVM, Smart Contracts)

Система

Состояний

Ускорение

Вердикт

Linux kernel CFG

1 млн

x25 233

unsafe из 100%

LLVM IR UB

800 000

x57 376

UB из 100%

Smart Contract

100 000

x69 003

reentrancy из 100%

EVM loss of funds

200 000

x72 528

loss из 100%

G. Робототехника

Система

Состояний

Ускорение

Вердикт

Mobile Robot

262 144

x141 337

collision из 100%

Warehouse Fleet

1 млн

x412 468

collision из 100%

H. БПЛА и оборона

Система

Состояний

Ускорение

Вердикт

Swarm (10 000 дронов)

1 млн

x814 340

collapse из 100%

Multi-Layer Air Defense

500 000

x554 442

прорыв из 100%

Radar Track (F^16M)

65 536

x726 592

потеря сопровождения

I. Цифровые двойники

Система

Состояний

Ускорение

Вердикт

Smart Grid

500 000

x270 068

каскад из 100%

Railway Network

300 000

x202 652

deadlock из 100%

Factory Twin

400 000

x177 109

останов из 100%

Флагманские демонстрации RaaS

Демо 1: 1 миллиард запросов за 29 секунд

Построили индекс на 4 млн состояний (0.9 секунды). Затем выполнили 1 000 000 000 (миллиард) запросов четырёх типов (Reach, Distance, Attractor, Future).

Результат: 1 миллиард запросов за 28.93 секунды. Пропускная способность — 34.6 млн запросов в секунду. Средняя латенси — 28.9 наносекунды.

// 1 миллиард запросов за 29 секунд
for (long q = 0; q < 1_000_000_000; q++)
{
    int a = probe[q & mask];
    switch (q & 3)
    {
        case 0: answer = reach[a]; break;           // Reach
        case 1: answer = dist[a]; break;            // Distance
        case 2: answer = e.GetAttractor(a, 0); break; // Attractor
        case 3: answer = e.Jump(a, 1_000_000, 0); break; // Future
    }
}

Демо 2: «Поисковик по будущему» (10¹² шагов вперёд)

Отвечаем на вопрос «где будет система через 1 триллион (10¹²) шагов?» — 5.28 млн запросов в секунду. Классический подход физически невозможен: триллион итераций никто не будет ждать.

Демо 3: Универсальный API для всех систем

Один и тот же API запускается на 9 разнородных системах — от DFA до роя дронов. Везде работает одинаково.

Система

Состояний

QPS (Reach)

Вердикт

DFA

200 000

246 млн

0% дост.

TLS 1.3

13

219 млн

92% дост.

QUIC

7

251 млн

71% дост.

HTTP/2

7

189 млн

86% дост.

Dining Philosophers

59 049

228 млн

100% дост.

Aho-Corasick

20 502

256 млн

100% дост.

Robotics

50 000

254 млн

100% дост.

UAV

50 000

256 млн

100% дост.

Air Defense

50 000

255 млн

100% дост.

Итоговая сводка

Общая статистика

Показатель

Значение

Всего бенчмарков

47

NFA-REACH: среднее ускорение

x222 219

NFA-REACH: максимальное ускорение

x1 377 723

FUNC-JUMP: среднее ускорение

x818 527

Максимальная пропускная способность

1.06 млрд запросов/сек

Минимальная латенси

0.9 наносекунды

Самый большой граф

4.78 млн состояний

Рекорд ускорения (F^N)

x1 388 204 (автопилот БПЛА)

Что мы доказали

  1. Детерминированные системы (DFA, протоколы, трекинг) — jump-таблицы дают ускорение до 1.4 миллиона раз. Вопрос «где будет система через 16 млн шагов?» — ответ за 100 наносекунд.

  2. Недетерминированные системы (NFA, SPIN, CFG, оборона) — амортизация индекса даёт ускорение до 1.38 миллиона раз. Один предварительный обход (секунды), затем миллионы запросов за наносекунды.

  3. RaaS как сервис — миллиард запросов к базе достижимости за 29 секунд. Это первый в мире «поисковик по будущему» для дискретных систем.

  4. Универсальность — один API работает на всех типах систем: от протоколов до роёв дронов и ПВО.

Применение в реальном мире

Область

Что даёт RaaS

Банки и финансы

Проверка эскалации привилегий, миллионы запросов в секунду

Атомные станции

Доказательство безопасности реактора за миллисекунды

БПЛА и оборона

Предсказание прорыва ПВО, состояния роя дронов за наносекунды

Медицина

Анализ сердечного ритма, детекция аритмии

Смарт-контракты

Аудит уязвимостей, поиск reentrancy

Компиляторы

Доказательство достижимости всех токенов языка

Кибербезопасность

Анализ CFG вредоносного ПО, поиск RCE-гаджетов

Автопилоты

Предсказание аварийных сценариев

Что дальше? Открыты к сотрудничеству

На данный момент библиотека SymFSM не опубликована в открытых репозиториях (NuGet, GitHub). Это связано с тем, что мы продолжаем активные исследования и доработки платформы.

Мы открыты к сотрудничеству в интересных и значимых проектах, где требуется:

  • Верификация критических систем (атомная энергетика, авионика, медицинское ПО)

  • Анализ безопасности (банки, блокчейн, кибербезопасность)

  • Оптимизация высоконагруженных систем (сети, протоколы, компиляторы)

  • Цифровые двойники и промышленная автоматизация

  • Оборонные и аэрокосмические проекты

Если у вас есть задача, где:

  • Есть конечный автомат, протокол, программа или любая другая дискретная система

  • Нужно отвечать на миллионы вопросов о достижимости, расстоянии, циклах

  • Классические BFS/DFS/SAT/SMT работают слишком медленно

Будем рады новым гипотезам и экспериментам.