На саммите ученых Web3 впервые представлен модель LiDO: механизированная верификация для сложных соглашений протоколов

На саммите Web3 ученых в 2025 году профессор кафедры компьютерных наук Йельского университета Чжао Чжун выступил с докладом на тему «Безопасность и доказательства активности на основе уточненного соглашения: LiDO и его расширение», впервые представив модель LiDO и расширяющую структуру LiDO-DAG, разработанные его командой. Это прорывное достижение направлено на предоставление механически проверяемых доказательств безопасности и активности для сложных протоколов согласия с стойкостью к сбоям (BFT), закладывая технологическую основу для надежности и масштабируемого развития экосистемы Web3.

Профессор Шао Чжун в своей речи отметил, что, несмотря на то, что существующие соглашения о протоколах (такие как PBFT, Jolteon) широко применяются, из-за сложности реализации они часто скрывают потенциальные уязвимости. Чтобы решить эту проблему, модель LiDO инновационно предложила трехуровневую рамку уточненной проверки:

1. Безопасный абстрактный уровень: отображение протокола в линейную машину состояний, обеспечение согласованности журналов (безопасность);
2. Активный уровень защиты: введение механизма "Pacemaker", который решает проблему сетевой задержки через тайм-аут вещания и синхронизацию раундов;
3. Расширение DAG-слоя: поддержка новых DAG-протоколов, таких как Narwhal и Bullshark, для эффективной проверки безлидерского соглашения.

В настоящее время LiDO успешно применяется в промышленных протоколах Jolteon (двухфазный BFT) и нескольких DAG-протоколах, завершив механизированное доказательство более 10 000 строк кода Coq, где объем кода для проверки безопасности и активности составляет соответственно 4000 и 1700 строк. Профессор Шао Чжун подчеркивает: "В настоящее время протоколы согласия PoS в целом сталкиваются с трудностью одновременного достижения безопасности, активности и децентрализации. Модель LiDO была предложена как системное решение для преодоления этой проблемы."

В качестве главного разработчика первой в мире операционной системы "без уязвимостей" CertiKOS, прошедшей формальную верификацию, профессор Шао Чжун накопил глубокий опыт в области системной безопасности. Это достижение не только укрепило его позицию в области технологий безопасности, но и продемонстрировало профессиональные способности его команды в области системной безопасности. В последние годы профессор Шао Чжун сосредоточил свои исследования на безопасности блокчейна и в 2017 году вместе с партнерами основал компанию, специализирующуюся на безопасности блокчейна, внедрив технологии формальной верификации для обеспечения безопасности смарт-контрактов и цепочных протоколов, предоставляя безопасность для криптоактивов на сумму в сотни миллиардов долларов.

Модель LiDO уже завершила проектирование и формальную проверку, и начала исследовать возможности интеграции с основными публичными цепочками и децентрализованными протоколами. Профессор Шао Чжун отметил, что они стремятся проверить ключевые механизмы в Web3.0, чтобы предоставить продукты и услуги на протяжении всего жизненного цикла, лучше поддерживая долгосрочную стратегию развития Web3 компаний и экосистемы. В конце выступления профессор Шао Чжун подчеркнул: "Достоверный, безопасный, проверяемый сетевой протокол стек станет ключевым путем к настоящему децентрализованному будущему."