montana/Формальная Документация/09 Внешний Аудит/Internal-Audit-2026-05-04.md

16 KiB
Raw Permalink Blame History

Внутренний аудит безопасности Монтаны

Дата: 2026-05-04 Версия аудируемой спецификации: Montana Protocol v35.25.0 Версия аудируемого кода: M8 cross-machine deploy (commit на genesis-узлах 2026-05-02) Аудитор: Claude Opus 4.7 (1M context) — внутренний security review. Статус: Не заменяет независимый внешний аудит. Является baseline-разбором перед привлечением внешней компании (см. Статус аудита).

Объём аудита

Слой Покрыт Глубина
Криптографические примитивы Параметры, FIPS-соответствие
Консенсус (Proof of Time) Safety/Liveness, лотерея, fork choice
Сетевой слой TLS-A, gossip, anti-Sybil
Управление ключами Хранение, восстановление, rotation
Account Chain Двойная трата, replay, баланс
Прикладной слой 🟡 Anchor — поверхностно
iOS/macOS клиенты 🔴 Не проверены глубоко (требует отдельного аудита)

Методология

Аудит проводился по шаблону Trail of Bits / NCC Group:

  1. Чтение спецификации v35.25.0 (4412 строк) и whitepaper'ов RU/EN/ZH.
  2. Просмотр genesis-manifest и runtime поведения 3 узлов.
  3. Тематический разбор атак: 51%, long-range, eclipse, nothing-at-stake, time manipulation, network partition, quantum, bribery, replay, MEV.
  4. Проверка соответствия NIST стандартам для PQ-крипто.
  5. Кросс-проверка против Threat Model (07) и Game Theory (08).

Severity-классификация

Уровень Определение
Critical Прямая угроза средствам пользователей или целостности консенсуса. Mainnet недопустим без устранения.
High Серьёзный риск, требует устранения до публичного M9.
Medium Риск ограниченного scope, может быть mitigated на уровне клиента.
Low Косметика, ergonomics, рекомендация.
Informational Замечание, не уязвимость.

Findings

F-01 [High] Single-implementation risk

Описание: Все 3 узла (мос/фра/зел) работают на одной реализации montana-node в Rust. Любая бага в этом единственном бинарнике автоматически распространяется на 100% сети.

Риск: Критический недостаток первой строки реализации может остановить или forkнуть всю сеть.

Сравнение: Bitcoin имеет три независимые реализации (Bitcoin Core, btcd, libbitcoin) специально как защиту от monoculture. Ethereum имеет geth + erigon + nethermind + besu.

Рекомендация:

  1. Документация спецификации должна быть достаточно полной чтобы написать независимую реализацию.
  2. До mainnet — минимум одна независимая реализация (на Go, TypeScript или Python) хотя бы в read-only режиме (verifier-only).
  3. Cross-implementation conformance тесты на каждый релиз.

Статус: Не закрыт. Mitigation плана не существует.


F-02 [High] Internal review только, нет независимого внешнего аудита

Описание: Все ИИ-критики в Внешний аудит/ выполнены Claude Opus 4.7 — это полезные итеративные разборы, но не настоящий внешний аудит.

Рекомендация: До mainnet провести аудит у Trail of Bits / Cure53 / NCC Group / Sigma Prime / Halborn (см. Статус аудита §3).

Статус: Phase 1 (pre-audit hardening) готова частично — спецификация стабильна, формальная верификация начата (см. F-03).


F-03 [Medium] TLA+ модель не закрывает всё пространство

Описание: Базовая TLA+ модель PoT существует (10 Формальная верификация), но:

  • Model check проводится при N=4 операторов, 3 аккаунта, 10 окон — мало для реальной уверенности.
  • TLAPS proof obligations не написаны.
  • Сетевой partition + GST поведение не моделируется.

Рекомендация: Расширить модель до N=7+ с symmetry reduction; написать TLAPS proofs для 4 теорем; добавить partition модель.

Статус: Roadmap составлен. Конкретные сроки не определены.


F-04 [Medium] Калибровка D₀ публично не обоснована

Описание: В спеке зафиксировано D₀ = 325 000 000 как «≈ 60 секунд на обычном x86_64». Численного публичного бенчмарка на N разных CPU нет.

Риск: Гетерогенная сеть может видеть значимый разброс времени окна на ранних окнах до первой адаптации τ₂ (через 14 дней).

Реальное наблюдение на текущей сети (window 8086, чуть менее 6 суток после genesis):

  • Drift между 3 узлами: 13 окна, что соответствует ~60-180 секундам разницы.
  • Это в пределах нормального допуска и не указывает на проблему.

Рекомендация: Опубликовать таблицу benchmark D=325M на: x86_64 SHA-NI (Intel 11+, AMD Ryzen 5+), x86_64 без SHA-NI (старые Intel/AMD), Apple Silicon M1/M2/M3, ARM Cortex-A78+ (cloud ARM).

Статус: Не сделано.


F-05 [Low] BFT-запас при n=3 равен нулю

Описание: При n=3 формула f<n/3 даёт f<1, то есть ни одного византийского узла нельзя терпеть. Один отказ или компрометация = провал безопасности по теореме.

Реальный риск: Низкий, потому что все 3 узла — одного автора, и риск компрометации концентрирован в одной точке отказа (что отдельно flagged в F-01).

Рекомендация: Расширить сеть до n≥9 с f<n/3=3, что даёт реальный BFT-запас. См. Mainnet Readiness §G3.

Статус: Запланировано в M9.


F-06 [Low] Все 3 узла — RU/EU юрисдикция

Описание: мос (RU), фра (DE), зел (FI) — все в зоне европейской/российской регуляции. Один государственный actor может теоретически давить на хостинг-провайдеров в этих регионах одновременно.

Рекомендация: При расширении до n≥9 добавить узлы в Asia (Japan, Singapore), Americas (US, Brazil), Africa (если применимо).

Статус: Запланировано.


F-07 [Low] Нет публичной dispute resolution процедуры

Описание: Если 2 узла не согласны о канонической истории (например, после network partition), нет публично документированной процедуры разбирательства.

Текущее поведение: Fork choice rule = самая длинная VDF-цепь. Это работает, но нет явной документации шагов которые оператор должен предпринять при наблюдении расхождения.

Рекомендация: Документировать процедуру в 11 Тестовая сеть или отдельным документом «Operator runbook».

Статус: Открыто.


F-08 [Informational] Mnemonic — 24 слова

Описание: Montana wordlist.txt и спека упоминают мнемонику.

Проверка: Длина 24 слова → 256 бит энтропии при стандартном BIP-39 wordlist (2048 слов). Соответствует требованию категории безопасности 3 (NIST L3).

Замечание: Если используется собственный wordlist, нужен документ с обоснованием выбора слов и проверкой на лингвистическую устойчивость (отсутствие омофонов в RU).

Статус: Замечание, не уязвимость.


F-09 [Medium] Network listener на 0.0.0.0:8444 — exposure

Описание: Узлы слушают на /ip4/0.0.0.0/tcp/8444 (всех интерфейсах). При отсутствии правильно настроенного firewall — exposure для глобального интернета.

Текущая защита:

  • ufw на Moscow открыт для 22/80/443/8443 — порт 8444 НЕ в списке (нужно проверить).
  • TLS-A pinning защищает от MITM, но не от DDoS/scan.

Рекомендация: Проверить ufw на всех 3 узлах — порт 8444 должен быть открыт только для p2p-connections, идеально с rate-limiting.

Статус: Требует операционной проверки.


F-10 [Informational] Genesis-manifest с фиксированными peer_id

Описание: В genesis-manifest.json зафиксированы 3 peer_id:

  • мос: 12D3KooWE6kn…
  • фра: 12D3KooWMzPB…
  • зел: 12D3KooWEzWH…

Замечание: Это правильный паттерн для bootstrap-узлов. Документ не указывает явно как добавлять новые non-bootstrap узлы — нужно для M9.

Статус: Не уязвимость, но gap в документации M9.


F-11 [Medium] Account chain и replay protection

Описание: Защита от replay основана на seq + τ-привязке (см. спека §«Замена двойной траты»).

Проверка модели:

  • Каждая операция имеет seq, привязанный к AccountChain.
  • Окно τ создаёт временную координату.
  • Replay невозможен потому что увеличение seq делает старую операцию недействительной.

Замечание: TLA+ модель явно не верифицирует replay protection. Нужно добавить инвариант:

ReplaySafety == \A op1, op2 \in committed[w] :
  (op1[1] = op2[1] /\ op1.seq = op2.seq) => op1 = op2

Статус: В спеке корректно, в TLA+ — TODO.


F-12 [Informational] Lottery determinism

Описание: Лотерея победителя окна детерминирована из VDF-выхода + AccountChain состояний участников.

Проверка: В TLA+ модели лотерея абстрактно моделируется как LotterySelect. Полная детерминированность зависит от:

  1. VDF-выход стабилен у всех узлов ( по построению).
  2. AccountChain state стабилен у всех ( по построению канона).
  3. Хеш-функция выбора одинакова у всех ( SHA-256 каноничен).

Статус: Корректно. Замечание для записи.

Сводная таблица findings

ID Severity Тема Статус
F-01 High Single-implementation risk 🔴 Не закрыт
F-02 High Нет внешнего аудита 🔴 Phase 1
F-03 Medium TLA+ модель ограничена 🟡 Roadmap
F-04 Medium D₀ калибровка не обоснована 🔴
F-05 Low BFT-запас 0 при n=3 🟡 M9
F-06 Low RU/EU монокультура юрисдикций 🟡 M9
F-07 Low Нет dispute runbook 🔴
F-08 Info Mnemonic 24 слов — OK
F-09 Medium 0.0.0.0:8444 exposure 🟡 Проверить ufw
F-10 Info Genesis-manifest без extension 🟡 M9
F-11 Medium Replay protection в TLA+ 🟡 TODO
F-12 Info Lottery determinism

Всего: 0 Critical, 2 High, 4 Medium, 3 Low, 3 Informational.

Pre-mainnet checklist

Для перехода в launched mainnet необходимо:

  • F-01: написать минимум одну независимую реализацию (хотя бы verifier-only).
  • F-02: завершённый внешний аудит у независимой компании.
  • F-03: расширенная TLA+ модель + TLAPS proofs.
  • F-04: публичный benchmark D на 5+ платформах.
  • F-05: расширение сети до n≥9 операторов (см. M9).
  • F-09: операционная проверка ufw на всех узлах.
  • F-11: replay safety в TLA+.

Связанные документы

Disclaimer

Этот документ — внутренний security review, выполненный ИИ-аудитором (Claude Opus 4.7). Не заменяет независимый аудит у профессиональной компании. Цель — baseline-разбор для подготовки к настоящему внешнему аудиту.