Яскраві моменти саміту вчених Web3: вперше публічно представлена модель перевірки безпеки нового протоколу консенсусу

На нещодавньому саміті Web3 дослідників 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, з яких обсяги коду для перевірки безпеки та активності становлять відповідно 4 000 і 1 700 рядків. Доповідач підкреслив: "На сьогодні протоколи консенсусу PoS загалом стикаються з труднощами досягнення балансу між безпекою, активністю та децентралізацією. Модель LiDO є системним дизайнерським рішенням, запропонованим для подолання цього обмеження."

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

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