/ Розширена формальна перевірка повного стеку програмного забезпечення Web3 /
CertiK нещодавно випустив розширений формальний звіт про перевірку модуля Cosmos SDK Bank, який, наскільки нам відомо, є першою успішною спробою формальної перевірки Cosmos SDK. Формальна верифікація — це метод, який використовує математичну логіку, щоб переконатися, що система відповідає специфікаціям, щоб вона поводилася, як очікувалося, за всіх можливих вхідних даних і умов. У цій статті ми представимо конкретні кроки для офіційної перевірки модуля Cosmos SDK Bank, а також деякі результати перевірки.
Що таке Cosmos SDK?
Cosmos Software Development Kit (SDK) — це фреймворк, який дає змогу розробникам створювати спеціальні блокчейн-додатки. Використовуючи Cosmos SDK, розробники можуть легко запустити власний блокчейн рівня 1, не турбуючись про дизайн і впровадження від консенсусного рівня до прикладного рівня. Cosmos SDK надає стандартні основні модулі, які можна безпосередньо імпортувати та використовувати в будь-якому ланцюжку, наприклад модулі стекінгу, автентифікації, gov і mint.
джерело:
Банківський модуль
Банківський модуль у Cosmos SDK відповідає за всі функції, пов’язані з керуванням токеном, наприклад передачу нативних токенів. Надсилання токенів має відповідати багатьом обмеженням і умовам, таким як наявність достатньої кількості доступних токенів в обліковому записі, за винятком тих, які були розставлені, заблоковані або роз’єднані. Завдяки підтримці таких модулів, як стекінг і авторизація, модуль банку керує всім процесом надсилання токенів. Незважаючи на те, що банківський модуль залежить від кількох інших модулів, оскільки вони виходять за межі цієї формальної перевірки, ми робимо деякі припущення щодо їх функціональності, щоб спростити процес.
Банківський модуль SDK складається з кількох підмодулів, у тому числі зберігача та типів, які є основними компонентами, які визначають поведінку модуля та типи даних. Ми зосередимося на підмодулі Keeper, оскільки він охоплює основні функції та особливості модуля.
Підмодуль keeper має два ключових компоненти: перегляд і надсилання. Зберігач переглядів відповідає за керування рахунками та балансами, тоді як зберігач надсилання відповідає за зміну балансів облікового запису, наприклад за передачу та розміщення заблокованих або розблокованих токенів. Потік модуля банку показано на малюнку нижче.Стрілки вказують напрямок від компонентів до функцій або Keepers.
джерело:
Метод автентифікації
Як зазначалося раніше, сфера дії цієї перевірки обмежена банківським модулем. Перед початком перевірки ми спочатку формулюємо формальні специфікації для типів даних у банківському модулі. Наприклад, у банківському модулі існує структура даних маркера, яка містить значення типу рядка та кількість типу big.Int, який визначено у вихідному коді таким чином:
Ця структура дуже проста. Ми використовуємо Coq (наша мова моделювання та формальної верифікації), щоб визначити її таким чином:
Базуючись на цьому визначенні, ми спочатку підтверджуємо деякі властивості основних операцій монет, щоб закласти основу для функціональної цілісності банківського модуля, який вимагає частої модифікації та маніпулювання типом монети. Наприклад:
Ця лема доводить фундаментальну інваріантність: віднімання двох монет не змінює їхніх номіналів і не призводить до негативного балансу.
Подібно до попереднього прикладу, основні компоненти кожного переходу стану моделюються в Coq, включаючи KV Store, GasMeter, Error Handling і Context.
Докладні специфікації типів даних і їх перевірку див.
Змоделюйте захисника
Після завершення моделювання базових компонентів ми можемо змоделювати core keeper банківського модуля, щоб описати функції модуля. Зберігач банку має два інтерфейси: один для доступу лише для читання до даних маркерів, а інший для передачі маркерів і обслуговування постачання.
View keeper відповідає за керування доступом лише для читання до балансів рахунків і містить чотири функції для обчислення балансів рахунків:
GetBalance: запитайте баланс рахунку певного номіналу за допомогою адреси. Він розглядає два випадки: послідовність нульових байтів і послідовність ненульових байтів. Формальна перевірка гарантує, що функція GetBalance дає правильні результати в обох випадках.
LockedCoins: повертає всі невитрачені токени в обліковому записі, що відповідає адресі. Через обмеження часу ми зробили припущення щодо деяких реалізацій із модуля автентифікації.
GetAllBalances: повертає всі залишки на рахунку за вказаною адресою.
GetAccountsBalances: повертає всі баланси облікового запису зі сховища та бере поля BAddress і BCoins як записи.
Менеджер надсилання обробляє передачу та постачання токенів. Під час процесу передачі він підтримує запас токенів, тому нові токени не карбуються.
SetBalance: встановіть символічний баланс для облікового запису за допомогою адреси. Ця функція розглядає два випадки: нульовий баланс і ненульовий баланс. В обох випадках правильність SetBalance доведена.
subUnlockedCoin: відніміть вказану суму (токен) з адреси. Рекурсивна функція subUnlockedCoins виконує ту саму операцію з набором монет. Відповідні властивості цих функцій вважаються аксіоматичними припущеннями.
addCoin: додайте вказану суму (токени) до адреси. Рекурсивна функція addCoins виконує ту саму операцію з набором монет. Відповідні властивості цих функцій вважаються аксіоматичними припущеннями.
SendCoins: надішліть суму з адреси одного облікового запису на адресу іншого облікового запису, щоб кошти обох адрес оновлювалися. Якщо одержувач не існує, для нього буде створено новий обліковий запис.
Використовуючи модель вищевказаних основних компонентів, ми можемо почати перевірку.
Процес перевірки
Наша перевірка виконується шляхом формального опису інваріантних властивостей цих функцій і доведення їх у допоміжній системі доказів, зосереджуючись на основних функціях «View Keeper» і «Send Keeper».
Наприклад, специфікація та лема setBalance_ok доводять правильність функції setBalance модуля BaseSendKeeper, зокрема, доводячи такі властивості:
Коли send.setBalance повертається до стану "Ok", є newMultiStore. У цей час оновлене середовище uctx походить від оригінального старого середовища ctx шляхом оновлення newMultiStore.
Баланс, що встановлюється, є дійсним токеном (він має необхідні властивості токена в системі).
Зв’язок setBalance_prop підтримується, щоб гарантувати, що функція оновлює баланс у newMultiStore очікуваним чином і генерує оновлене середовище uctx.
Після завершення налаштування балансу скористайтеся адресою рахунку та номінал балансу (Denom), щоб викликати view.GetBalance в оновленому середовищі uctx, і буде повернено той самий баланс, установлений send.setBalance.
Ці властивості описані мовою специфікації Coq наступним чином:
Щоб отримати код Coq іншого характеру, відвідайте:
майбутня кар'єра
Основа цієї перевірки побудована на кількох припущеннях і аксіомах, які ми можемо перевірити глибше, щоб розширити сферу перевірки. Майбутня робота зосереджена на наступних напрямках:
Перевірка припущень: поточна перевірка спирається на серію припущень як основу для доказу. Ці припущення можна перевірити в майбутньому, щоб переконатися, що вони точно відображають заплановану поведінку та властивості системи.
Автентифікація модуля Auth: цей модуль відповідає за керування даними облікового запису та механізмами підписів і є основним компонентом Cosmos SDK. У майбутньому його можна буде повністю офіційно перевірити, щоб переконатися, що впровадження модуля та взаємодія з іншими модулями точні.
Більше теорем про делегування, карбування та продаж монет: Розширення сфери перевірки та введення додаткових теорем про делегування, карбування та продаж монет допоможе більш повно зрозуміти механізм роботи системи. Ці теореми можна об’єднати з перевіркою модуля авторизації, щоб забезпечити загальну послідовність і коректність системи.
Розширте всю інфраструктуру Cosmos SDK: поточна робота з перевірки в основному зосереджена на банківському модулі та його пов’язаних компонентах. У майбутньому формальний процес перевірки можна буде поширити на всю інфраструктуру Cosmos SDK, тим самим підвищуючи загальну точність, безпеку та стабільність платформи та надаючи розробникам і користувачам більш стабільне та надійне середовище.
Інтеграція з іншими модулями: Оскільки Cosmos SDK включає різні взаємопов’язані модулі, корисно вивчити взаємодію та залежності між ними. Це вимагає перевірки правильності взаємодії між модулями та забезпечення того, щоб будь-які зміни в одному модулі не вплинули негативно на інші модулі.
Моделювання та перевірка механізмів заохочення: Cosmos SDK також інтегрує механізми заохочення, такі як ставки та розподіл винагороди. Подальші дослідження змоделюють і перевірять ці механізми, щоб переконатися, що вони правильні та відповідають очікуваним економічним стимулам.
Ця стаття демонструє перший успішний випадок розширеної формальної перевірки модуля Cosmos SDKbank, який виконує ефективну роботу для створення основи безпеки та надійності екосистеми блокчейну. Подальша робота розширить це досягнення шляхом перевірки припущень, перевірки інших модулів і охоплення всієї інфраструктури Cosmos SDK, зрештою створюючи надійнішу та надійнішу платформу для розробників і користувачів.
Переглянути оригінал
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
Детальне пояснення формальної перевірки стандартних модулів Cosmos SDK
/ Розширена формальна перевірка повного стеку програмного забезпечення Web3 /
CertiK нещодавно випустив розширений формальний звіт про перевірку модуля Cosmos SDK Bank, який, наскільки нам відомо, є першою успішною спробою формальної перевірки Cosmos SDK. Формальна верифікація — це метод, який використовує математичну логіку, щоб переконатися, що система відповідає специфікаціям, щоб вона поводилася, як очікувалося, за всіх можливих вхідних даних і умов. У цій статті ми представимо конкретні кроки для офіційної перевірки модуля Cosmos SDK Bank, а також деякі результати перевірки.
Що таке Cosmos SDK?
Cosmos Software Development Kit (SDK) — це фреймворк, який дає змогу розробникам створювати спеціальні блокчейн-додатки. Використовуючи Cosmos SDK, розробники можуть легко запустити власний блокчейн рівня 1, не турбуючись про дизайн і впровадження від консенсусного рівня до прикладного рівня. Cosmos SDK надає стандартні основні модулі, які можна безпосередньо імпортувати та використовувати в будь-якому ланцюжку, наприклад модулі стекінгу, автентифікації, gov і mint.
джерело:
Банківський модуль
Банківський модуль у Cosmos SDK відповідає за всі функції, пов’язані з керуванням токеном, наприклад передачу нативних токенів. Надсилання токенів має відповідати багатьом обмеженням і умовам, таким як наявність достатньої кількості доступних токенів в обліковому записі, за винятком тих, які були розставлені, заблоковані або роз’єднані. Завдяки підтримці таких модулів, як стекінг і авторизація, модуль банку керує всім процесом надсилання токенів. Незважаючи на те, що банківський модуль залежить від кількох інших модулів, оскільки вони виходять за межі цієї формальної перевірки, ми робимо деякі припущення щодо їх функціональності, щоб спростити процес.
Банківський модуль SDK складається з кількох підмодулів, у тому числі зберігача та типів, які є основними компонентами, які визначають поведінку модуля та типи даних. Ми зосередимося на підмодулі Keeper, оскільки він охоплює основні функції та особливості модуля.
Підмодуль keeper має два ключових компоненти: перегляд і надсилання. Зберігач переглядів відповідає за керування рахунками та балансами, тоді як зберігач надсилання відповідає за зміну балансів облікового запису, наприклад за передачу та розміщення заблокованих або розблокованих токенів. Потік модуля банку показано на малюнку нижче.Стрілки вказують напрямок від компонентів до функцій або Keepers.
джерело:
Метод автентифікації
Як зазначалося раніше, сфера дії цієї перевірки обмежена банківським модулем. Перед початком перевірки ми спочатку формулюємо формальні специфікації для типів даних у банківському модулі. Наприклад, у банківському модулі існує структура даних маркера, яка містить значення типу рядка та кількість типу big.Int, який визначено у вихідному коді таким чином:
Ця структура дуже проста. Ми використовуємо Coq (наша мова моделювання та формальної верифікації), щоб визначити її таким чином:
Базуючись на цьому визначенні, ми спочатку підтверджуємо деякі властивості основних операцій монет, щоб закласти основу для функціональної цілісності банківського модуля, який вимагає частої модифікації та маніпулювання типом монети. Наприклад:
Ця лема доводить фундаментальну інваріантність: віднімання двох монет не змінює їхніх номіналів і не призводить до негативного балансу.
Подібно до попереднього прикладу, основні компоненти кожного переходу стану моделюються в Coq, включаючи KV Store, GasMeter, Error Handling і Context.
Докладні специфікації типів даних і їх перевірку див.
Змоделюйте захисника
Після завершення моделювання базових компонентів ми можемо змоделювати core keeper банківського модуля, щоб описати функції модуля. Зберігач банку має два інтерфейси: один для доступу лише для читання до даних маркерів, а інший для передачі маркерів і обслуговування постачання.
View keeper відповідає за керування доступом лише для читання до балансів рахунків і містить чотири функції для обчислення балансів рахунків:
GetBalance: запитайте баланс рахунку певного номіналу за допомогою адреси. Він розглядає два випадки: послідовність нульових байтів і послідовність ненульових байтів. Формальна перевірка гарантує, що функція GetBalance дає правильні результати в обох випадках.
LockedCoins: повертає всі невитрачені токени в обліковому записі, що відповідає адресі. Через обмеження часу ми зробили припущення щодо деяких реалізацій із модуля автентифікації.
GetAllBalances: повертає всі залишки на рахунку за вказаною адресою.
GetAccountsBalances: повертає всі баланси облікового запису зі сховища та бере поля BAddress і BCoins як записи.
Менеджер надсилання обробляє передачу та постачання токенів. Під час процесу передачі він підтримує запас токенів, тому нові токени не карбуються.
SetBalance: встановіть символічний баланс для облікового запису за допомогою адреси. Ця функція розглядає два випадки: нульовий баланс і ненульовий баланс. В обох випадках правильність SetBalance доведена.
subUnlockedCoin: відніміть вказану суму (токен) з адреси. Рекурсивна функція subUnlockedCoins виконує ту саму операцію з набором монет. Відповідні властивості цих функцій вважаються аксіоматичними припущеннями.
addCoin: додайте вказану суму (токени) до адреси. Рекурсивна функція addCoins виконує ту саму операцію з набором монет. Відповідні властивості цих функцій вважаються аксіоматичними припущеннями.
SendCoins: надішліть суму з адреси одного облікового запису на адресу іншого облікового запису, щоб кошти обох адрес оновлювалися. Якщо одержувач не існує, для нього буде створено новий обліковий запис.
Використовуючи модель вищевказаних основних компонентів, ми можемо почати перевірку.
Процес перевірки
Наша перевірка виконується шляхом формального опису інваріантних властивостей цих функцій і доведення їх у допоміжній системі доказів, зосереджуючись на основних функціях «View Keeper» і «Send Keeper».
Наприклад, специфікація та лема setBalance_ok доводять правильність функції setBalance модуля BaseSendKeeper, зокрема, доводячи такі властивості:
Коли send.setBalance повертається до стану "Ok", є newMultiStore. У цей час оновлене середовище uctx походить від оригінального старого середовища ctx шляхом оновлення newMultiStore.
Баланс, що встановлюється, є дійсним токеном (він має необхідні властивості токена в системі).
Зв’язок setBalance_prop підтримується, щоб гарантувати, що функція оновлює баланс у newMultiStore очікуваним чином і генерує оновлене середовище uctx.
Після завершення налаштування балансу скористайтеся адресою рахунку та номінал балансу (Denom), щоб викликати view.GetBalance в оновленому середовищі uctx, і буде повернено той самий баланс, установлений send.setBalance.
Ці властивості описані мовою специфікації Coq наступним чином:
Щоб отримати код Coq іншого характеру, відвідайте:
майбутня кар'єра
Основа цієї перевірки побудована на кількох припущеннях і аксіомах, які ми можемо перевірити глибше, щоб розширити сферу перевірки. Майбутня робота зосереджена на наступних напрямках:
Перевірка припущень: поточна перевірка спирається на серію припущень як основу для доказу. Ці припущення можна перевірити в майбутньому, щоб переконатися, що вони точно відображають заплановану поведінку та властивості системи.
Автентифікація модуля Auth: цей модуль відповідає за керування даними облікового запису та механізмами підписів і є основним компонентом Cosmos SDK. У майбутньому його можна буде повністю офіційно перевірити, щоб переконатися, що впровадження модуля та взаємодія з іншими модулями точні.
Більше теорем про делегування, карбування та продаж монет: Розширення сфери перевірки та введення додаткових теорем про делегування, карбування та продаж монет допоможе більш повно зрозуміти механізм роботи системи. Ці теореми можна об’єднати з перевіркою модуля авторизації, щоб забезпечити загальну послідовність і коректність системи.
Розширте всю інфраструктуру Cosmos SDK: поточна робота з перевірки в основному зосереджена на банківському модулі та його пов’язаних компонентах. У майбутньому формальний процес перевірки можна буде поширити на всю інфраструктуру Cosmos SDK, тим самим підвищуючи загальну точність, безпеку та стабільність платформи та надаючи розробникам і користувачам більш стабільне та надійне середовище.
Інтеграція з іншими модулями: Оскільки Cosmos SDK включає різні взаємопов’язані модулі, корисно вивчити взаємодію та залежності між ними. Це вимагає перевірки правильності взаємодії між модулями та забезпечення того, щоб будь-які зміни в одному модулі не вплинули негативно на інші модулі.
Моделювання та перевірка механізмів заохочення: Cosmos SDK також інтегрує механізми заохочення, такі як ставки та розподіл винагороди. Подальші дослідження змоделюють і перевірять ці механізми, щоб переконатися, що вони правильні та відповідають очікуваним економічним стимулам.
Ця стаття демонструє перший успішний випадок розширеної формальної перевірки модуля Cosmos SDKbank, який виконує ефективну роботу для створення основи безпеки та надійності екосистеми блокчейну. Подальша робота розширить це досягнення шляхом перевірки припущень, перевірки інших модулів і охоплення всієї інфраструктури Cosmos SDK, зрештою створюючи надійнішу та надійнішу платформу для розробників і користувачів.