Язык Move, как язык смарт-контрактов нового поколения, обладает выдающимся уровнем безопасности. В данной статье будет проведен анализ безопасности Move с трех аспектов: особенности языка, механизм работы и инструменты верификации.
1. Безопасные характеристики языка Move
Язык Move изначально отказался от нелинейной логики, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы, а вместо этого использует такие концепции, как обобщения, глобальное хранилище, ресурсы и другие для реализации альтернативной модели программирования. Эти особенности эффективно предотвращают такие распространенные уязвимости, как повторный вход.
Основной механизм безопасности Move включает в себя:
Модуль: каждый модуль состоит из типа структуры и определения процесса, может импортировать определения типов из других модулей.
Структура: может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Глобальное хранилище: позволяет постоянно хранить данные, которые могут быть прочитаны и записаны программно только теми, кто обладает модулем.
Виртуальная машина байт-кода: принудительное выполнение безопасных типов и линейной структуры, предотвращающее незаконные операции с значениями типов ресурсов.
Инвариантное сокращение: можно определить статическую проверку инвариантов, чтобы гарантировать безопасность кода.
2. Механизм работы Move
Программа Move выполняется в виртуальной машине и не может напрямую обращаться к системной памяти. Ее состояние состоит из стека вызовов, памяти, глобальных переменных и операционных массивов.
MoveVM отделяет хранение данных и стек вызовов, что значительно отличается от EVM. Ресурсы под адресом учетной записи пользователя ( хранятся независимо, вызовы программ должны соответствовать правилам доступа и ресурсам, что повышает безопасность и эффективность выполнения.
![Анализ безопасности Move: игра с правилами языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. Переместить Провер
Move Prover — это инструмент формальной верификации, который использует алгоритмы дедуктивной верификации для проверки соответствия программы ожидаемым требованиям. Его рабочий процесс следующий:
Компилировать в байт-код, преобразовать в модель объекта валидатора
Переведите на промежуточный язык Boogie
Генерация условий проверки
Использование решателя Z3 для верификации SMT-формул
Генерация диагностического отчета
Язык спецификации Move используется для описания спецификаций и может быть написан независимо, не влияя на производственный код.
![Анализ безопасности Move: игра, меняющая правила игры для языков смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
Итог
Язык Move учитывает все аспекты, такие как языковые особенности, выполнение виртуальной машины и инструменты безопасности. Он избегает распространенных уязвимостей, таких как повторный вход и переполнение, но проблемы управления доступом и логические ошибки все еще требуют внимания разработчиков. Рекомендуется использовать сторонний аудит безопасности и поручить профессиональной команде разработку проверочного кода.
![Анализ безопасности Move: революция в языке смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
20 Лайков
Награда
20
5
Репост
Поделиться
комментарий
0/400
MEVHunterZhang
· 07-13 14:53
Если безопасность достаточно крепка, то остальное - всё иллюзия.
Полный анализ безопасности языка Move: особенности, механизмы и инструменты проверки
Анализ безопасности языка Move
Язык Move, как язык смарт-контрактов нового поколения, обладает выдающимся уровнем безопасности. В данной статье будет проведен анализ безопасности Move с трех аспектов: особенности языка, механизм работы и инструменты верификации.
1. Безопасные характеристики языка Move
Язык Move изначально отказался от нелинейной логики, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы, а вместо этого использует такие концепции, как обобщения, глобальное хранилище, ресурсы и другие для реализации альтернативной модели программирования. Эти особенности эффективно предотвращают такие распространенные уязвимости, как повторный вход.
Основной механизм безопасности Move включает в себя:
Модуль: каждый модуль состоит из типа структуры и определения процесса, может импортировать определения типов из других модулей.
Структура: может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Глобальное хранилище: позволяет постоянно хранить данные, которые могут быть прочитаны и записаны программно только теми, кто обладает модулем.
Виртуальная машина байт-кода: принудительное выполнение безопасных типов и линейной структуры, предотвращающее незаконные операции с значениями типов ресурсов.
Инвариантное сокращение: можно определить статическую проверку инвариантов, чтобы гарантировать безопасность кода.
2. Механизм работы Move
Программа Move выполняется в виртуальной машине и не может напрямую обращаться к системной памяти. Ее состояние состоит из стека вызовов, памяти, глобальных переменных и операционных массивов.
MoveVM отделяет хранение данных и стек вызовов, что значительно отличается от EVM. Ресурсы под адресом учетной записи пользователя ( хранятся независимо, вызовы программ должны соответствовать правилам доступа и ресурсам, что повышает безопасность и эффективность выполнения.
![Анализ безопасности Move: игра с правилами языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. Переместить Провер
Move Prover — это инструмент формальной верификации, который использует алгоритмы дедуктивной верификации для проверки соответствия программы ожидаемым требованиям. Его рабочий процесс следующий:
Язык спецификации Move используется для описания спецификаций и может быть написан независимо, не влияя на производственный код.
![Анализ безопасности Move: игра, меняющая правила игры для языков смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
Итог
Язык Move учитывает все аспекты, такие как языковые особенности, выполнение виртуальной машины и инструменты безопасности. Он избегает распространенных уязвимостей, таких как повторный вход и переполнение, но проблемы управления доступом и логические ошибки все еще требуют внимания разработчиков. Рекомендуется использовать сторонний аудит безопасности и поручить профессиональной команде разработку проверочного кода.
![Анализ безопасности Move: революция в языке смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(