8 квітня на Web3 Scholars Conference 2025, що проходила в Гонконзі, Шао Чжун, професор кафедри комп'ютерних наук Єльського університету та співзасновник CertiK, виступив із ключовою доповіддю під назвою «Доказ безпеки та активність протоколів консенсусу на основі уточнення: LiDO та його розширення», вперше розкривши модель LiDO та фреймворк розширення LiDO-DAG, розроблений його командою. Це проривне досягнення має на меті забезпечити механічно перевірений доказ безпеки та життєздатності для складного візантійського протоколу консенсусу Byzantine Fault Tolerance (BFT), закладаючи технічну основу для надійності та масштабного розвитку екосистеми Web3.
У своїй промові професор Шао Чжун вказав, що існуючі протоколи консенсусу (такі як PBFT, Jolteon) хоча і широко використовуються, але через складність реалізації часто приховують потенційні вразливості. Для вирішення цієї проблеми модель LiDO інноваційно пропонує триступеневу рамку деталізованої валідації:
Рівень абстракції безпеки: відображення протоколів як лінеаризованих машин станів для забезпечення узгодженості журналів (безпеки);
Активний рівень захисту: впровадження механізму «Pacemaker», що дозволяє вирішити проблему затримки в мережі за допомогою тайм-аутного трансляції та синхронізації раундів;
DAG Extension Layer: підтримує нові протоколи DAG, такі як Narwhal і Bullshark, для досягнення ефективної перевірки консенсусу без лідера.
В даний час LiDO успішно застосовується до протоколу промислового класу Jolteon (двоступеневий BFT) і декількох протоколів DAG, завершивши механізовану перевірку більш ніж 10 000 рядків коду Coq, з 4 000 лініями безпеки і 1 700 лініями коду перевірки активності. «В даний час протоколи консенсусу PoS, як правило, стикаються з дилемою безпеки, життєздатності та децентралізації», – зазначив у своєму виступі професор Шао Чжун. «Модель LiDO є системним дизайнерським рішенням, щоб подолати цю дилему».
Професор Шао Чжун, очолюючи команду, розробив CertiKOS, першу у світі операційну систему без вад, перевірену формальною верифікацією, яка була названа «віхою безпеки кіберфізичних систем». Це досягнення не лише заклало технологічний фундамент безпекової компанії CertiK, але й продемонструвало її глибокі накопичення в області системної безпеки. У останні роки професор Шао Чжун активно досліджує безпеку блокчейну, у 2017 році заснував CertiK разом зі своїм учнем професором Гу Ронгхуєм, впровадивши технологію формальної верифікації для забезпечення безпеки смарт-контрактів та протоколів на ланцюзі, охороняючи безпеку криптоактивів вартістю у сотні мільярдів доларів.
LiDO завершив розробку моделі та офіційну верифікацію, а також почав вивчати можливість інтеграції з основними публічними ланцюгами та децентралізованими протоколами. Професор Шао Чжун сказав, що CertiK прагне перевірити ключові механізми Web3.0 для надання продуктів і послуг повного циклу для кращої підтримки довгострокових стратегій розвитку підприємств та екосистем Web3. Наприкінці виступу професор Шао Чжун підкреслив: «Надійний, безпечний і перевірений стек мережевих протоколів стане ключовим шляхом до справді децентралізованого майбутнього. ”
Контент має виключно довідковий характер і не є запрошенням до участі або пропозицією. Інвестиційні, податкові чи юридичні консультації не надаються. Перегляньте Відмову від відповідальності , щоб дізнатися більше про ризики.
Професор Шао Чжун, співзасновник CertiK, взяв участь у саміті вчених Web3, де вперше було представлено модель LiDO.
8 квітня на Web3 Scholars Conference 2025, що проходила в Гонконзі, Шао Чжун, професор кафедри комп'ютерних наук Єльського університету та співзасновник CertiK, виступив із ключовою доповіддю під назвою «Доказ безпеки та активність протоколів консенсусу на основі уточнення: LiDO та його розширення», вперше розкривши модель LiDO та фреймворк розширення LiDO-DAG, розроблений його командою. Це проривне досягнення має на меті забезпечити механічно перевірений доказ безпеки та життєздатності для складного візантійського протоколу консенсусу Byzantine Fault Tolerance (BFT), закладаючи технічну основу для надійності та масштабного розвитку екосистеми Web3.
У своїй промові професор Шао Чжун вказав, що існуючі протоколи консенсусу (такі як PBFT, Jolteon) хоча і широко використовуються, але через складність реалізації часто приховують потенційні вразливості. Для вирішення цієї проблеми модель LiDO інноваційно пропонує триступеневу рамку деталізованої валідації:
Рівень абстракції безпеки: відображення протоколів як лінеаризованих машин станів для забезпечення узгодженості журналів (безпеки);
Активний рівень захисту: впровадження механізму «Pacemaker», що дозволяє вирішити проблему затримки в мережі за допомогою тайм-аутного трансляції та синхронізації раундів;
DAG Extension Layer: підтримує нові протоколи DAG, такі як Narwhal і Bullshark, для досягнення ефективної перевірки консенсусу без лідера.
В даний час LiDO успішно застосовується до протоколу промислового класу Jolteon (двоступеневий BFT) і декількох протоколів DAG, завершивши механізовану перевірку більш ніж 10 000 рядків коду Coq, з 4 000 лініями безпеки і 1 700 лініями коду перевірки активності. «В даний час протоколи консенсусу PoS, як правило, стикаються з дилемою безпеки, життєздатності та децентралізації», – зазначив у своєму виступі професор Шао Чжун. «Модель LiDO є системним дизайнерським рішенням, щоб подолати цю дилему».
Професор Шао Чжун, очолюючи команду, розробив CertiKOS, першу у світі операційну систему без вад, перевірену формальною верифікацією, яка була названа «віхою безпеки кіберфізичних систем». Це досягнення не лише заклало технологічний фундамент безпекової компанії CertiK, але й продемонструвало її глибокі накопичення в області системної безпеки. У останні роки професор Шао Чжун активно досліджує безпеку блокчейну, у 2017 році заснував CertiK разом зі своїм учнем професором Гу Ронгхуєм, впровадивши технологію формальної верифікації для забезпечення безпеки смарт-контрактів та протоколів на ланцюзі, охороняючи безпеку криптоактивів вартістю у сотні мільярдів доларів.
LiDO завершив розробку моделі та офіційну верифікацію, а також почав вивчати можливість інтеграції з основними публічними ланцюгами та децентралізованими протоколами. Професор Шао Чжун сказав, що CertiK прагне перевірити ключові механізми Web3.0 для надання продуктів і послуг повного циклу для кращої підтримки довгострокових стратегій розвитку підприємств та екосистем Web3. Наприкінці виступу професор Шао Чжун підкреслив: «Надійний, безпечний і перевірений стек мережевих протоколів стане ключовим шляхом до справді децентралізованого майбутнього. ”