Конференція веб3-учених зосереджена на новій безпечній верифікаційній рамці протоколу консенсусу

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