На峰шере Web3 профессор Йельского университета делится прогрессом в исследованиях безопасности соглашения

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