Основные моменты саммита Web3: Впервые публично представлен новый модель проверки безопасности протокола соглашения

На недавно прошедшем саммите ученых Web3 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 с использованием формальной верификации, которая была признана "вехой в безопасности киберфизических систем". Это достижение не только заложило техническую основу для основанной им позже компании по безопасности, но и продемонстрировало его глубокие накопления в области системной безопасности. В последние годы он сосредоточил свои исследования на безопасности блокчейна, стремясь применить технологии формальной верификации для обеспечения безопасности смарт-контрактов и цепочных протоколов, предоставляя безопасность криптоактивов на сумму в сотни миллиардов долларов.

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