Професор Єльського університету вперше представив модель LiDO на саміті вчених Web3

На саміті вчених Web3 2025 року професор кафедри комп'ютерних наук Єльського університету Чжао Чжун виступив з основною доповіддю на тему "Безпека та активність доказів на основі уточнених консенсусних протоколів: LiDO та його розширення", вперше представивши модель LiDO та розширену структуру LiDO-DAG, розроблені його командою. Цей інноваційний результат має на меті забезпечити механізовано перевіряємий рівень безпеки та активності для складних протоколів консенсусу з байєрською толерантністю (BFT), закладаючи технічну основу для надійності та масштабованого розвитку екосистеми Web3.

Професор Шао Чжун у своїй доповіді зазначив, що існуючі консенсусні протоколи (такі як PBFT, Jolteon), хоча і широко використовуються, але через свою складність часто приховують потенційні вразливості. Для вирішення цієї проблеми модель LiDO запропонувала тришарову уточнену верифікаційну структуру:

1. Безпечний абстрактний рівень: відображення протоколу в лінійну машину станів, що забезпечує узгодженість журналу (безпека);
2. Активний рівень забезпечення: впровадження механізму "Pacemaker", що дозволяє вирішити проблему затримки в мережі через тайм-аутне широкомовлення та синхронізацію раундів;
3. Розширювальний рівень DAG: підтримує новітні протоколи DAG, забезпечуючи ефективну верифікацію без лідерства.

Наразі LiDO успішно застосовується в промисловому протоколі Jolteon (двоступенева BFT) та кількох протоколах DAG, завершивши механізоване підтвердження понад десяти тисяч рядків коду Coq, при цьому обсяг коду для перевірки безпеки та активності становить відповідно 4000 рядків і 1700 рядків. Професор Шао Чжун у своїй промові підкреслив: "На сьогоднішній день протоколи консенсусу PoS загалом стикаються з труднощами, пов'язаними з безпекою, активністю та децентралізацією, які важко поєднати. Модель LiDO була запропонована як системне проектне рішення для подолання цієї проблеми."

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

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