Саммит ученых 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 является первой в мире операционной системой с "нулевыми уязвимостями", прошедшей формальную верификацию, и считается "вехой безопасности киберфизических систем". Это достижение не только демонстрирует глубокие накопления его команды в области системной безопасности, но и закладывает прочный фундамент для последующих исследований в области безопасности блокчейна.

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

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