На саміті веб3 професор Єльського університету вперше представив модель LiDO

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

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

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

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