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

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

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