Web3 ученый саммит: профессор Йельского университета впервые представляет модель LiDO

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