/ Полная формальная проверка Web3 стека программного обеспечения/
CertiK недавно выпустила расширенный формальный отчет о проверке модуля Cosmos SDK Bank, который, насколько нам известно, является первой успешной попыткой формальной проверки Cosmos SDK. Формальная проверка — это метод, использующий математическую логику для обеспечения соответствия системы спецификациям и ее поведения ожидаемым образом при всех возможных входных данных и условиях. В этой статье мы представим конкретные этапы формальной проверки модуля Cosmos SDK Bank, а также некоторые результаты проверки.
Что такое Cosmos SDK?
Cosmos Software Development Kit (сокращенно SDK) — это платформа, которая позволяет разработчикам создавать собственные блокчейн-приложения. Используя Cosmos SDK, разработчики могут легко запустить свой собственный блокчейн уровня 1, не беспокоясь о проектировании и реализации, от уровня консенсуса до уровня приложения. Cosmos SDK предоставляет стандартные основные модули, которые можно напрямую импортировать и использовать в любой цепочке, например модули ставок, аутентификации, управления и монетного двора.
источник:
Банковский модуль
Банковский модуль в Cosmos SDK отвечает за все функции, связанные с управлением токенами, например передачу собственных токенов. Отправка токенов должна соответствовать множеству ограничений и условий, например, наличие достаточного количества доступных токенов в учетной записи, за исключением тех, которые были поставлены, заблокированы или отсоединены. Благодаря поддержке таких модулей, как стейкинг и аутентификация, банковский модуль управляет всем процессом отправки токенов. Хотя банковский модуль зависит от нескольких других модулей, поскольку они выходят за рамки этой формальной проверки, мы делаем некоторые предположения об их функциональности, чтобы упростить процесс.
Банковский модуль SDK состоит из нескольких подмодулей, включая хранитель и типы, которые являются основными компонентами, определяющими поведение модуля и типы данных. Мы сосредоточимся на подмодуле Keeper, поскольку он охватывает основные функциональные возможности и возможности модуля.
Подмодуль Keeper имеет два ключевых компонента: просмотр и отправка. Хранитель представления отвечает за управление учетными записями и балансами, а хранитель отправки отвечает за изменение балансов счетов, например, за передачу и размещение заблокированных или разблокированных токенов. Ход работы банковского модуля показан на рисунке ниже, а стрелка указывает направление от компонента к функции или Keeper.
источник:
Метод аутентификации
Как упоминалось ранее, объем этой проверки ограничен банковским модулем. Прежде чем начать проверку, мы сначала сформулируем формальную спецификацию типов данных в банковском модуле. Например, в банковском модуле есть структура данных токена, содержащая номинал типа string и сумму типа big.Int, которая определена в исходном коде следующим образом:
Структура проста, и мы определяем ее на Coq (нашем языке моделирования и формальной проверки) следующим образом:
Основываясь на этом определении, мы сначала доказываем некоторые свойства основных операций с монетой, чтобы заложить основу функциональной целостности банковского модуля, поскольку это требует частой модификации и манипуляций с типом монеты. Например:
Эта лемма доказывает фундаментальную инвариантность: вычитание двух монет не меняет их номинала и не вызывает отрицательного баланса.
Как и в предыдущем примере, базовые компоненты каждого перехода между состояниями моделируются в Coq, включая KV Store, GasMeter, обработку ошибок и контекст.
Подробные характеристики типов данных и их проверку см.:
Модель хранителя
После завершения моделирования основных компонентов мы можем смоделировать ядро хранителя банковского модуля для описания функций модуля. У хранителя банка есть два интерфейса: один для доступа только для чтения к данным токена, а другой для передачи токенов и обслуживания поставок.
Viewkeeper отвечает за обработку доступа только для чтения к остаткам на счетах и содержит четыре функции для расчета остатков на счетах:
GetBalance: запрос баланса счета определенного номинала через адрес. Он рассматривает два случая: последовательность нулевых байтов и последовательность ненулевых байтов. Формальная проверка гарантирует, что функция GetBalance дает правильные результаты в обоих случаях.
LockedCoins: возвращает все нерасходуемые токены в учетной записи, соответствующей адресу. Из-за нехватки времени мы сделали предположения о некоторых реализациях модуля auth.
GetAllBalances: возвращает все остатки на счетах по указанному адресу.
GetAccountsBalances: возвращает все балансы счетов из хранилища и принимает поля BAddress и BCoins как записи.
Менеджер отправки занимается передачей и поставкой токенов. Во время процесса передачи он поддерживает запас токенов, поэтому новые токены не создаются.
SetBalance: установите баланс токенов для учетной записи через адрес. Эта функция рассматривает два случая: балансы, установленные в ноль, и балансы, установленные в ненулевые значения. В обоих случаях корректность SetBalance доказана.
subUnlockedCoin: вычесть указанную сумму (токен) из адреса. Рекурсивная функция subUnlockedCoins выполняет ту же операцию с набором монет. Соответствующие свойства этих функций считаются аксиоматическими предположениями.
addCoin: добавьте указанную сумму (токен) к адресу. Рекурсивная функция addCoins выполняет ту же операцию с набором токенов. Соответствующие свойства этих функций рассматриваются как аксиоматические предположения.
SendCoins: отправьте сумму с одного адреса учетной записи на другой адрес учетной записи, чтобы средства обоих адресов были обновлены. Если получатель не существует, для него будет создана новая учетная запись.
Используя модель вышеупомянутых основных компонентов, мы можем начать проверку.
Процесс проверки
Наша проверка осуществляется путем формального описания инвариантных свойств этих функций и их доказательства с помощью вспомогательной системы доказательств, уделяя основное внимание основным функциям «View Keeper» и «Send Keeper».
Например, спецификация и лемма setBalance_ok доказывают корректность функции setBalance модуля BaseSendKeeper, а именно доказывают следующие свойства:
Когда send.setBalance возвращается в состояние «ОК», существует новыйMultiStore. В это время обновленная среда 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 предоставляет стандартные основные модули, которые можно напрямую импортировать и использовать в любой цепочке, например модули ставок, аутентификации, управления и монетного двора.
источник:
Банковский модуль
Банковский модуль в Cosmos SDK отвечает за все функции, связанные с управлением токенами, например передачу собственных токенов. Отправка токенов должна соответствовать множеству ограничений и условий, например, наличие достаточного количества доступных токенов в учетной записи, за исключением тех, которые были поставлены, заблокированы или отсоединены. Благодаря поддержке таких модулей, как стейкинг и аутентификация, банковский модуль управляет всем процессом отправки токенов. Хотя банковский модуль зависит от нескольких других модулей, поскольку они выходят за рамки этой формальной проверки, мы делаем некоторые предположения об их функциональности, чтобы упростить процесс.
Банковский модуль SDK состоит из нескольких подмодулей, включая хранитель и типы, которые являются основными компонентами, определяющими поведение модуля и типы данных. Мы сосредоточимся на подмодуле Keeper, поскольку он охватывает основные функциональные возможности и возможности модуля.
Подмодуль Keeper имеет два ключевых компонента: просмотр и отправка. Хранитель представления отвечает за управление учетными записями и балансами, а хранитель отправки отвечает за изменение балансов счетов, например, за передачу и размещение заблокированных или разблокированных токенов. Ход работы банковского модуля показан на рисунке ниже, а стрелка указывает направление от компонента к функции или Keeper.
источник:
Метод аутентификации
Как упоминалось ранее, объем этой проверки ограничен банковским модулем. Прежде чем начать проверку, мы сначала сформулируем формальную спецификацию типов данных в банковском модуле. Например, в банковском модуле есть структура данных токена, содержащая номинал типа string и сумму типа big.Int, которая определена в исходном коде следующим образом:
Структура проста, и мы определяем ее на Coq (нашем языке моделирования и формальной проверки) следующим образом:
Основываясь на этом определении, мы сначала доказываем некоторые свойства основных операций с монетой, чтобы заложить основу функциональной целостности банковского модуля, поскольку это требует частой модификации и манипуляций с типом монеты. Например:
Эта лемма доказывает фундаментальную инвариантность: вычитание двух монет не меняет их номинала и не вызывает отрицательного баланса.
Как и в предыдущем примере, базовые компоненты каждого перехода между состояниями моделируются в Coq, включая KV Store, GasMeter, обработку ошибок и контекст.
Подробные характеристики типов данных и их проверку см.:
Модель хранителя
После завершения моделирования основных компонентов мы можем смоделировать ядро хранителя банковского модуля для описания функций модуля. У хранителя банка есть два интерфейса: один для доступа только для чтения к данным токена, а другой для передачи токенов и обслуживания поставок.
Viewkeeper отвечает за обработку доступа только для чтения к остаткам на счетах и содержит четыре функции для расчета остатков на счетах:
GetBalance: запрос баланса счета определенного номинала через адрес. Он рассматривает два случая: последовательность нулевых байтов и последовательность ненулевых байтов. Формальная проверка гарантирует, что функция GetBalance дает правильные результаты в обоих случаях.
LockedCoins: возвращает все нерасходуемые токены в учетной записи, соответствующей адресу. Из-за нехватки времени мы сделали предположения о некоторых реализациях модуля auth.
GetAllBalances: возвращает все остатки на счетах по указанному адресу.
GetAccountsBalances: возвращает все балансы счетов из хранилища и принимает поля BAddress и BCoins как записи.
Менеджер отправки занимается передачей и поставкой токенов. Во время процесса передачи он поддерживает запас токенов, поэтому новые токены не создаются.
SetBalance: установите баланс токенов для учетной записи через адрес. Эта функция рассматривает два случая: балансы, установленные в ноль, и балансы, установленные в ненулевые значения. В обоих случаях корректность SetBalance доказана.
subUnlockedCoin: вычесть указанную сумму (токен) из адреса. Рекурсивная функция subUnlockedCoins выполняет ту же операцию с набором монет. Соответствующие свойства этих функций считаются аксиоматическими предположениями.
addCoin: добавьте указанную сумму (токен) к адресу. Рекурсивная функция addCoins выполняет ту же операцию с набором токенов. Соответствующие свойства этих функций рассматриваются как аксиоматические предположения.
SendCoins: отправьте сумму с одного адреса учетной записи на другой адрес учетной записи, чтобы средства обоих адресов были обновлены. Если получатель не существует, для него будет создана новая учетная запись.
Используя модель вышеупомянутых основных компонентов, мы можем начать проверку.
Процесс проверки
Наша проверка осуществляется путем формального описания инвариантных свойств этих функций и их доказательства с помощью вспомогательной системы доказательств, уделяя основное внимание основным функциям «View Keeper» и «Send Keeper».
Например, спецификация и лемма setBalance_ok доказывают корректность функции setBalance модуля BaseSendKeeper, а именно доказывают следующие свойства:
Когда send.setBalance возвращается в состояние «ОК», существует новыйMultiStore. В это время обновленная среда 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, что в конечном итоге создаст более надежную и надежную платформу для разработчиков и пользователей.