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