Предвычисленные матрицы допуска, решатель Z3 и иммунная петля возврата retry_of
Главная инженерная трудность при защите автономных агентов состоит в противоречии между математической строгостью и задержкой отклика. Если компилировать текстовые правила политики безопасности на каждом вызове заново или обращаться к внешней языковой модели, время ожидания возрастает до секунд, а формальная гарантия теряется.
В комплексе MITR это противоречие разрешено разделением времени компиляции и времени исполнения. Декларативные политики отрасли заранее переводятся в предвычисленные матрицы предикатов бескванторной линейной целочисленной арифметики с неинтерпретируемыми функциями (логика QF_UFLIA). Во время работы агента решатель Z3 проверяет уже собранную матрицу за считанные миллисекунды, а повторяющиеся безопасные вызовы обслуживаются по отпечатку параметров в линейном журнале.
1. Конвейер прохождения вызова по шкале обратимости R0–R5
Каждый вызов внешнего инструмента перехватывается адаптером до попадания в сетевой сокет или файловую систему. В зависимости от ступени обратимости шлюз применяет ровно тот уровень проверки, который необходим для исключения необратимого вреда.
Последовательность прохождения команды через шлюз: разбор аргументов, быстрая проверка в памяти пакетом mcp-sentinel 1.1.2, классификация по шести ступеням обратимости, решение формулы в Z3 и запись сцепленной квитанции в gate_actions.jsonl.
| Ступень | Доля потока | Примеры операций в правовой и финансовой практике | Режим проверки и удержания границы |
|---|---|---|---|
R0 | 48% | Чтение карточки судебного дела, проверка статуса контрагента, запрос баланса счёта | Мгновенная сверка области видимости в памяти (~0,016 мс), состояние среды не меняется |
R1 | 14% | Сохранение черновика заметки во внутренней рабочей папке, создание временной закладки | Полностью обратимо внутри рабочей сессии, запись в локальный журнал |
R2 | 11% | Простановка внутренних меток классификации, предварительный расчёт государственной пошлины или комиссии | Контроль целостности типов и диапазонов значений без внешних вызовов |
R3 | 16% | Формирование проекта процессуального ходатайства или постановка платёжного поручения в отзывную очередь | Сверка полномочий и лимитов, возможность отзыва до подписания руководителем |
R4 | 7% | Отправка официального уведомления во внешний канал, запись в рабочую таблицу хранилища | Принудительная фильтрация личных реквизитов (ADR-0073) и проверка на косвенные инъекции |
R5 | 4% | Необратимое списание денежных средств, подача отказа от иска в суд, безвозвратное удаление дела | Отказ по умолчанию (fail-closed), полное доказательство в решателе Z3 (p99 = 4,5 мс) |
2. Иммунная петля самоисправления агента (Unsat Core Injection / retry_of)
Обычный межсетевой экран при срабатывании правила возвращает слепую ошибку отказа в доступе, после чего автономный агент либо зацикливается, либо падает с аварийным исключением. Шлюз MITR использует математическое свойство решателя Z3: при нарушении политики формула проверки на поиск контрпримера оказывается выполнимой (SAT), а при проверке совместности инвариантов выделяется минимальное невыполнимое ядро (Unsat Core).
Имена нарушенных предикатов и точные пороговые условия упаковываются в поле retry_of и возвращаются агенту прямо в ответном сообщении протокола вызова инструментов. Агент видит конкретную причину отказа (например, превышение лимита одиночной подписи в пятьсот тысяч рублей или отсутствие идентификатора резервной копии) и за один-три раунда (порог MITR_GATE_ROUNDS_MAX = 3) самостоятельно переводит операцию в безопасный режим постановки в очередь R3.
3. Независимая перепроверка хэш-цепочки без доверия к серверу
Каждое решение шлюза (как допуск UNSAT, так и блокировка SAT) записывается в линейный журнал gate_actions.jsonl. Каждая строка связывается с предыдущей отпечатками SHA-256 и ГОСТ Р 34.11-2012 («Стрибог-256»), а суточные корни дерева хэшей фиксируются в блокчейне Bitcoin через открытый стандарт OpenTimestamps.
python verify_chain_standalone.py --replay --ledger gate_actions.jsonl
python iss_verifier.py --ledger audit.jsonlОднофайловый скрипт проверки работает исключительно на стандартной библиотеке Python и не требует сетевого подключения к серверам разработчика. Любая попытка изменить, удалить или вставить запись задним числом немедленно обнаруживается при пересчёте цепочки.