montana/Formal-Docs/09-External-Audit/Internal-Audit-2026-05-04.md

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

**Дата:** 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-разбором перед привлечением внешней компании (см. [Статус аудита](Статус-аудита.md)).

## Объём аудита

| Слой | Покрыт | Глубина |
|------|--------|---------|
| Криптографические примитивы | ✅ | Параметры, 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](../07-Threat-Model/)) и Game Theory ([08](../08-Incentives-Game-Theory/)).

## 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 только, нет независимого внешнего аудита

**Описание:** Все ИИ-критики в [External-Audit/](../../Montana-Protocol/External-Audit/) выполнены Claude Opus 4.7 — это полезные итеративные разборы, но не настоящий внешний аудит.

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

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

---

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

**Описание:** Базовая TLA+ модель PoT существует ([10 Формальная верификация](../10-Formal-Verification/PoT.tla)), но:
- 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 узлами: 1–3 окна, что соответствует ~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](../Mainnet-Readiness.md).

**Статус:** Запланировано в 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 Тестовая сеть](../11-Testnet/) или отдельным документом «Operator runbook».

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

---

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

**Описание:** [Montana wordlist.txt](../../Montana-Protocol/Montana%20wordlist.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+.

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

- [Статус аудита](Статус-аудита.md) — индустриальный план.
- [TLA+ модель](../10-Formal-Verification/) — формальная верификация.
- [Threat Model](../07-Threat-Model/) — кросс-проверка.
- [Mainnet Readiness](../Mainnet-Readiness.md) — гейты.
- [Critic Analysis 3 столпов](../../Montana-Protocol/External-Audit/critic-analysis-2026-05-04-3-pillars.md) — внешняя критика.

## Disclaimer

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