На конференції Web3 вперше представлено модель LiDO: механізм верифікації для складних протоколів консенсусу

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

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