На проводимой сегодня конференции Web3 Scholars Conference 2025 профессор кафедры компьютерных наук Йельского университета и соучредитель CertiK Шао Чжун выступил с основной темой «Безопасность и доказательство активности на основе уточненных консенсусных протоколов: LiDO и его расширение», впервые представив разработанную его командой модель LiDO и расширяющуюся структуру LiDO-DAG. Этот прорывной результат направлен на обеспечение механически проверяемой безопасности и доказательства активности для сложных протоколов консенсуса с байантийскойFault-Tolerance (BFT), что закладывает технологическую основу для надежности и масштабирования экосистемы Web3.
В своем выступлении профессор Шао Чжун указал, что существующие протоколы консенсуса (такие как PBFT, Jolteon), хотя и широко используются, но из-за сложности реализации часто скрывают потенциальные уязвимости. Для решения этой проблемы модель LiDO инновационно предлагает трехуровневую уточняющую верификационную структуру:
Безопасный абстрактный уровень: отображение протокола в линейную машину состояний, обеспечение согласованности журналов (безопасность);
Уровень активной защиты: введение механизма "Pacemaker", который решает проблему задержки сети с помощью тайм-аутов и синхронизации раундов;
Расширенный уровень DAG: поддержка новых DAG-протоколов, таких как Narwhal и Bullshark, для эффективной валидации без лидера.
На данный момент LiDO успешно применен в промышленных протоколах Jolteon (двухфазный BFT) и нескольких DAG-протоколах, завершив механизированное доказательство более чем 10 000 строк кода Coq, при этом объем кода для проверки безопасности и активности составил 4000 и 1700 строк соответственно. "В настоящее время протоколы согласия PoS в целом сталкиваются с трудностью достижения безопасности, активности и децентрализации одновременно," отметил профессор Шао Чжун в своем выступлении. "Модель LiDO была предложена как системное решение для преодоления этой проблемы."
Профессор Шао Чжун и его команда разработали CertiKOS, первая в мире операционная система "без уязвимостей", прошедшая формальную верификацию, которая была названа "вехой в области безопасности киберфизических систем". Это достижение не только заложило технологическую основу для компании безопасности CertiK, но и продемонстрировало ее глубокие накопления в области системной безопасности. В последние годы профессор Шао Чжун углубился в безопасность блокчейна и в 2017 году совместно с учеником профессором Гу Ронгхуэем основал CertiK, внедрив технологии формальной верификации для обеспечения безопасности смарт-контрактов и цепочечных протоколов, что обеспечивает безопасность криптоактивов на уровне миллиардов долларов.
LiDO в настоящее время завершила проектирование модели и формальную верификацию, и начала исследовать возможности интеграции с основными публичными цепочками и децентрализованными протоколами. Профессор Шао Чжун отметил, что CertiK стремится к верификации ключевых механизмов в Web3.0, чтобы предоставить продукты и услуги на всех этапах, лучше поддерживая долгосрочную стратегию развития Web3 компаний и экосистемы. В конце выступления профессор Шао Чжун подчеркнул: "Достоверный, безопасный и проверяемый стек сетевых протоколов станет ключевым путем к действительно децентрализованному будущему."
Содержание носит исключительно справочный характер и не является предложением или офертой. Консультации по инвестициям, налогообложению или юридическим вопросам не предоставляются. Более подробную информацию о рисках см. в разделе «Дисклеймер».
Соучредитель CertiK профессор Шао Чжун присутствовал на саммите ученых Web3, впервые представив модель LiDO.
На проводимой сегодня конференции Web3 Scholars Conference 2025 профессор кафедры компьютерных наук Йельского университета и соучредитель CertiK Шао Чжун выступил с основной темой «Безопасность и доказательство активности на основе уточненных консенсусных протоколов: LiDO и его расширение», впервые представив разработанную его командой модель LiDO и расширяющуюся структуру LiDO-DAG. Этот прорывной результат направлен на обеспечение механически проверяемой безопасности и доказательства активности для сложных протоколов консенсуса с байантийскойFault-Tolerance (BFT), что закладывает технологическую основу для надежности и масштабирования экосистемы Web3.
В своем выступлении профессор Шао Чжун указал, что существующие протоколы консенсуса (такие как PBFT, Jolteon), хотя и широко используются, но из-за сложности реализации часто скрывают потенциальные уязвимости. Для решения этой проблемы модель LiDO инновационно предлагает трехуровневую уточняющую верификационную структуру:
На данный момент LiDO успешно применен в промышленных протоколах Jolteon (двухфазный BFT) и нескольких DAG-протоколах, завершив механизированное доказательство более чем 10 000 строк кода Coq, при этом объем кода для проверки безопасности и активности составил 4000 и 1700 строк соответственно. "В настоящее время протоколы согласия PoS в целом сталкиваются с трудностью достижения безопасности, активности и децентрализации одновременно," отметил профессор Шао Чжун в своем выступлении. "Модель LiDO была предложена как системное решение для преодоления этой проблемы."
Профессор Шао Чжун и его команда разработали CertiKOS, первая в мире операционная система "без уязвимостей", прошедшая формальную верификацию, которая была названа "вехой в области безопасности киберфизических систем". Это достижение не только заложило технологическую основу для компании безопасности CertiK, но и продемонстрировало ее глубокие накопления в области системной безопасности. В последние годы профессор Шао Чжун углубился в безопасность блокчейна и в 2017 году совместно с учеником профессором Гу Ронгхуэем основал CertiK, внедрив технологии формальной верификации для обеспечения безопасности смарт-контрактов и цепочечных протоколов, что обеспечивает безопасность криптоактивов на уровне миллиардов долларов.
LiDO в настоящее время завершила проектирование модели и формальную верификацию, и начала исследовать возможности интеграции с основными публичными цепочками и децентрализованными протоколами. Профессор Шао Чжун отметил, что CertiK стремится к верификации ключевых механизмов в Web3.0, чтобы предоставить продукты и услуги на всех этапах, лучше поддерживая долгосрочную стратегию развития Web3 компаний и экосистемы. В конце выступления профессор Шао Чжун подчеркнул: "Достоверный, безопасный и проверяемый стек сетевых протоколов станет ключевым путем к действительно децентрализованному будущему."