81 lines
4.6 KiB
Markdown
81 lines
4.6 KiB
Markdown
|
# Формальная верификация Монтаны
|
|||
|
|
|
|||
|
|
**Версия:** черновик 1.0
|
|||
|
|
**Текущий статус:** 🔴 Не начата.
|
|||
|
|
|
|||
|
|
## 1. Цель
|
|||
|
|
|
|||
|
|
Математическое доказательство ключевых свойств протокола в формальной системе (TLA+, Coq, Isabelle/HOL).
|
|||
|
|
|
|||
|
|
Это самый высокий уровень зрелости L1-блокчейна. Tendermint, Algorand, Cardano — у всех есть формальные модели хотя бы консенсуса.
|
|||
|
|
|
|||
|
|
## 2. Что должно быть верифицировано
|
|||
|
|
|
|||
|
|
### 2.1 Консенсус Proof of Time
|
|||
|
|
|
|||
|
|
- **Safety теорема S1** ([01 Консенсус §4.1](../01%20Консенсус/Proof-of-Time.md)): невозможность форков при f<n/3.
|
|||
|
|
- **Liveness теорема L1** ([01 Консенсус §4.2](../01%20Консенсус/Proof-of-Time.md)): включение операций после GST.
|
|||
|
|
- **Fork choice rule** — самая длинная цепь VDF, формализация и устойчивость.
|
|||
|
|
|
|||
|
|
### 2.2 Криптография
|
|||
|
|
|
|||
|
|
- KAT-таблицы для ML-DSA-65, ML-KEM-768, SHA-256 — соответствие FIPS-стандартам.
|
|||
|
|
- Канонический формат сериализации — биективность, отсутствие неоднозначности.
|
|||
|
|
|
|||
|
|
### 2.3 Account Chain
|
|||
|
|
|
|||
|
|
- Двойная трата невозможна в пределах окна τ₁.
|
|||
|
|
- Anti-инфляция (баланс не растёт без эмиссии).
|
|||
|
|
- Replay protection через seq + τ-привязку.
|
|||
|
|
|
|||
|
|
### 2.4 Лотерея
|
|||
|
|
|
|||
|
|
- Победитель окна детерминирован при заданных входах.
|
|||
|
|
- Невозможность смещения исхода атакующим с f<n/3.
|
|||
|
|
|
|||
|
|
## 3. Выбор инструмента
|
|||
|
|
|
|||
|
|
| Инструмент | Сильные стороны | Применимость к Монтане |
|
|||
|
|
|------------|-----------------|------------------------|
|
|||
|
|
| **TLA+** | Распределённые системы, model checking | ✅ Идеально для PoT consensus |
|
|||
|
|
| **Coq** | Полная теорема-проверка | Для криптографических редукций |
|
|||
|
|
| **Isabelle/HOL** | Аналог Coq | Для математической части |
|
|||
|
|
| **K Framework** | Operational semantics | Не нужен — нет VM |
|
|||
|
|
| **Lean 4** | Современный mathlib | Альтернатива Coq |
|
|||
|
|
|
|||
|
|
**Рекомендация:** начать с **TLA+** (consensus + safety/liveness), затем дополнить **Coq** (крипто-редукции) при необходимости.
|
|||
|
|
|
|||
|
|
## 4. План работ
|
|||
|
|
|
|||
|
|
### Phase 1 — TLA+ модель консенсуса (3-6 месяцев)
|
|||
|
|
|
|||
|
|
- [ ] Спецификация PoT в TLA+ (модель сети, операторы, VDF, лотерея).
|
|||
|
|
- [ ] Доказательство Safety через TLAPS.
|
|||
|
|
- [ ] Liveness через temporal logic.
|
|||
|
|
- [ ] Model checking при малых N (3, 5, 7 операторов) через TLC.
|
|||
|
|
- [ ] Публикация модели в этой папке.
|
|||
|
|
|
|||
|
|
### Phase 2 — Coq крипто-редукции (опционально, если аудит требует)
|
|||
|
|
|
|||
|
|
- [ ] EUF-CMA редукция ML-DSA-65 формализована.
|
|||
|
|
- [ ] Не самостоятельная задача — обычно делается в академическом контексте либо ссылается на сторонние формализации (NIST PQC has some).
|
|||
|
|
|
|||
|
|
### Phase 3 — Account Chain свойства
|
|||
|
|
|
|||
|
|
- [ ] Inv: баланс ≥ 0 на любой τ-точке.
|
|||
|
|
- [ ] Inv: двойная трата невозможна.
|
|||
|
|
- [ ] Inv: эмиссия монотонна и фиксирована.
|
|||
|
|
|
|||
|
|
## 5. Связанные документы
|
|||
|
|
|
|||
|
|
- [01 Консенсус](../01%20Консенсус/) — теоремы, требующие верификации.
|
|||
|
|
- [07 Модель угроз](../07%20Модель%20Угроз/) — допущения, которые модель должна охватить.
|
|||
|
|
- [09 Внешний аудит](../09%20Внешний%20Аудит/) — комплементарный к этому слою.
|
|||
|
|
|
|||
|
|
## 6. Источники
|
|||
|
|
|
|||
|
|
1. Lamport, L. (2002). *Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers*.
|
|||
|
|
2. Buchman, E. et al. (2018). *The latest gossip on BFT consensus* (Tendermint TLA+).
|
|||
|
|
3. Algorand formal model: github.com/algorand/specs.
|
|||
|
|
4. IronFleet (Hawblitzel et al., 2015). *IronFleet: Proving Practical Distributed Systems Correct*. SOSP.
|