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

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

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

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