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