Конференція Web3: Професор Єльського університету вперше публічно представив модель LiDO

На нещодавній конференції Web3 Scholar Summit 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, з яких обсяг коду для перевірки безпеки та активності становить відповідно 4000 рядків і 1700 рядків. Професор Шао Чжун у своїй доповіді підкреслив: "Наразі протоколи консенсусу PoS загалом стикаються з труднощами досягнення трьох цілей: безпеки, активності та децентралізації. Модель LiDO була запропонована як системний дизайн для подолання цього обмеження."

Варто зазначити, що команда професора Шао Чжуна, яка раніше розробила систему CertiKOS, стала першою у світі, що пройшла формальну верифікацію "без уразливостей" операційної системи, яка була визнана "віхою безпеки кіберфізичних систем". Це досягнення не лише демонструє глибокий досвід його команди в області системної безпеки, але й закладає міцний фундамент для подальших досліджень з безпеки блокчейну.

Модель LiDO наразі завершила проектування та формальну перевірку, і почала досліджувати можливості інтеграції з основними публічними блокчейнами та децентралізованими протоколами. Професор Шао Чжун висловив думку, що вони прагнуть перевірити ключові механізми в Web3.0, щоб забезпечити повний цикл продуктів і послуг, краще підтримуючи довгострокову стратегію розвитку Web3 компаній та екосистем.

Наприкінці виступу професор Шао Чжун підкреслив: "Достовірний, безпечний і перевіряємий стек мережевих протоколів стане ключовим шляхом до справжнього децентралізованого майбутнього." Ця думка підкреслює важливу роль моделі LiDO у просуванні технологій Web3, пропонуючи нові ідеї та методи для забезпечення безпеки та надійності майбутніх децентралізованих систем.