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