На саміті Web3 професор Єльського університету поділився дослідженнями безпеки консенсус-протоколів

На саміті Web3 Scholar 2025 року професор кафедри комп'ютерних наук Єльського університету Шао Чжун виступив з доповіддю під заголовком «Безпека та активність доказу на основі уточненого протоколу консенсусу: LiDO та його розширення», вперше представивши модель LiDO та розширену структуру LiDO-DAG, розроблені його командою. Цей прорив має на меті забезпечити механічно перевірювану безпеку та активність доказу для складних протоколів консенсусу з баптистською толерантністю (BFT), закладаючи технічну основу для надійності та масштабованого розвитку екосистеми Web3.

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

1. Безпечний абстрактний рівень: відображення протоколу як лінійної машини станів, що забезпечує узгодженість журналів (безпека);
2. Активний рівень захисту: впровадження механізму "Pacemaker" для розв'язання проблеми затримки в мережі через трансляцію за тайм-аутом і синхронізацію раундів;
3. Розширення DAG: підтримка нових DAG-протоколів, таких як Narwhal і Bullshark, для ефективної верифікації безлідерного консенсусу.

На даний момент LiDO успішно застосовується в промисловому протоколі Jolteon (двоступеневий BFT) та в кількох DAG-протоколах, завершивши механізоване доведення понад тисячі рядків коду Coq, обсяги перевірки безпеки та активності становлять відповідно 4000 і 1700 рядків. Професор Шао Чжун у своїй доповіді зазначив: "На сьогоднішній день протоколи консенсусу PoS загалом стикаються з труднощами у досягненні безпеки, активності та децентралізації одночасно. Модель LiDO була запропонована як системне дизайнерське рішення для подолання цієї проблеми."

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

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