Перший публічний показ моделі LiDO професором Єльського університету на саміті веб3
Сьогодні відбулася конференція Web3 Scholar Summit 2025, на якій професор кафедри комп'ютерних наук Єльського університету Шао Чжун виступив з основним доповіддю, в якій представив модель LiDO та розширену структуру LiDO-DAG, розроблені його командою. Цей інноваційний результат має на меті забезпечити механізовану верифікацію безпеки та активності для складних протоколів узгодження з байєзантською помилкою (BFT), закладаючи технічну основу для надійності та масштабованості екосистеми Web3.
Професор Шао Чжун у своїй промові зазначив, що, незважаючи на те, що існуючі консенсусні протоколи (такі як PBFT і Jolteon) широко використовуються, через їхню складність реалізації часто виникають потенційні вразливості. Щоб вирішити цю проблему, модель LiDO запропонувала трирівневу структуру перевірки.
Безпечний абстрактний рівень: відображення протоколу в лінійний автомат, що забезпечує консистентність журналів (безпека);
Активний захисний рівень: впровадження механізму "Pacemaker", що дозволяє вирішити проблему затримки в мережі за допомогою широкомасштабної трансляції та синхронізації раундів;
Розширювальний шар DAG: підтримка нових DAG-протоколів, таких як Narwhal, Bullshark тощо, забезпечує ефективну верифікацію безлідерної консенсусу.
Модель LiDO була успішно застосована до промислового протоколу Jolteon (двофазний BFT) та кількох DAG-протоколів, завершивши механізоване доведення більше ніж 10 тисяч рядків коду Coq. Зокрема, обсяг коду для перевірки безпеки та активності становить відповідно 4000 рядків та 1700 рядків. Професор Шао Чжун у своїй доповіді підкреслив: "На сьогодні протоколи консенсусу PoS зазвичай стикаються з труднощами досягнення безпеки, активності та децентралізації одночасно. Модель LiDO була запропонована як системний дизайн для подолання цієї труднощі."
Як головний розробник першої у світі операційної системи "без вад" CertiKOS, яка пройшла формальну валідацію, професор Шао Чжун має глибокі знання в галузі системної безпеки. В останні роки він зосередив свої дослідження на безпеці блокчейнів, прагнучи застосувати технології формальної валідації для забезпечення безпеки смарт-контрактів та протоколів на ланцюгу, щоб забезпечити захист криптоактивів на десятки мільярдів доларів.
Модель LiDO наразі завершила проектування та формальну верифікацію, і вони досліджують можливості інтеграції з основними публічними ланцюгами та децентралізованими протоколами. Професор Шао Чжун заявив, що вони прагнуть верифікувати ключові механізми у Web3.0, щоб забезпечити продукти та послуги на весь життєвий цикл, краще підтримуючи стратегію довгострокового розвитку Web3 компаній та екосистем.
Професор Шао Чжун під час завершення своєї промови підкреслив: "Достовірний, безпечний і перевіряємий стек мережевих протоколів стане ключовим шляхом до справжнього децентралізованого майбутнього."
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
14 лайків
Нагородити
14
4
Репост
Поділіться
Прокоментувати
0/400
WalletInspector
· 12год тому
Ця технологія оновлюється занадто швидко.
Переглянути оригіналвідповісти на0
SleepyValidator
· 13год тому
Ай, ще одна верифікаційна модель, криптографи про всі змагаються.
Професор Єльського університету оприлюднив модель LiDO для формалізованої безпекової перевірки екосистеми Web3.
Перший публічний показ моделі LiDO професором Єльського університету на саміті веб3
Сьогодні відбулася конференція Web3 Scholar Summit 2025, на якій професор кафедри комп'ютерних наук Єльського університету Шао Чжун виступив з основним доповіддю, в якій представив модель LiDO та розширену структуру LiDO-DAG, розроблені його командою. Цей інноваційний результат має на меті забезпечити механізовану верифікацію безпеки та активності для складних протоколів узгодження з байєзантською помилкою (BFT), закладаючи технічну основу для надійності та масштабованості екосистеми Web3.
Професор Шао Чжун у своїй промові зазначив, що, незважаючи на те, що існуючі консенсусні протоколи (такі як PBFT і Jolteon) широко використовуються, через їхню складність реалізації часто виникають потенційні вразливості. Щоб вирішити цю проблему, модель LiDO запропонувала трирівневу структуру перевірки.
Модель LiDO була успішно застосована до промислового протоколу Jolteon (двофазний BFT) та кількох DAG-протоколів, завершивши механізоване доведення більше ніж 10 тисяч рядків коду Coq. Зокрема, обсяг коду для перевірки безпеки та активності становить відповідно 4000 рядків та 1700 рядків. Професор Шао Чжун у своїй доповіді підкреслив: "На сьогодні протоколи консенсусу PoS зазвичай стикаються з труднощами досягнення безпеки, активності та децентралізації одночасно. Модель LiDO була запропонована як системний дизайн для подолання цієї труднощі."
Як головний розробник першої у світі операційної системи "без вад" CertiKOS, яка пройшла формальну валідацію, професор Шао Чжун має глибокі знання в галузі системної безпеки. В останні роки він зосередив свої дослідження на безпеці блокчейнів, прагнучи застосувати технології формальної валідації для забезпечення безпеки смарт-контрактів та протоколів на ланцюгу, щоб забезпечити захист криптоактивів на десятки мільярдів доларів.
Модель LiDO наразі завершила проектування та формальну верифікацію, і вони досліджують можливості інтеграції з основними публічними ланцюгами та децентралізованими протоколами. Професор Шао Чжун заявив, що вони прагнуть верифікувати ключові механізми у Web3.0, щоб забезпечити продукти та послуги на весь життєвий цикл, краще підтримуючи стратегію довгострокового розвитку Web3 компаній та екосистем.
Професор Шао Чжун під час завершення своєї промови підкреслив: "Достовірний, безпечний і перевіряємий стек мережевих протоколів стане ключовим шляхом до справжнього децентралізованого майбутнього."