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

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

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