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

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