Веб3 наукова конференція: професор Єльського університету оприлюднив модель LiDO, що сприяє підвищенню безпеки консенсусу протоколу

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

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

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

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