Саммит ученых Web3 сосредоточен на безопасности новой рамки протокола соглашения

На недавней конференции Web3 Scholars Summit 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 компаний и экосистемы. В конце выступления профессор Шао Чжун подчеркнул: "Достоверный, безопасный и проверяемый стек сетевых протоколов будет ключевым путем к настоящему децентрализованному будущему."