На конференції Web3 професор Шао Чжун представив модель LiDO, що сприяє перевірці безпеки консенсус протоколу

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