На саммите 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, из которых объем кода для проверки безопасности и активности составляет соответственно 4 000 и 1 700 строк. Профессор Шао Чжун в своей речи подчеркнул: "В настоящее время протоколы согласия PoS сталкиваются с трудностями в обеспечении безопасности, активности и децентрализации одновременно. Модель LiDO является системным решением, предложенным для преодоления этой проблемы."

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

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