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

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

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

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