Язык Move, как язык смарт-контрактов нового поколения, изначально учитывал проблемы безопасности блокчейна и смарт-контрактов в своем дизайне. В данной статье будет исследоваться безопасность языка Move с трех аспектов: особенностей языка, механизма выполнения и инструментов верификации.
1. Безопасные характеристики языка Move
Язык Move обладает следующими основными характеристиками безопасности:
Отказался от нелинейной логики, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы
Реализация альтернативных программных моделей с использованием таких концепций, как обобщения, глобальное хранилище, ресурсы и т.д.
Модульный дизайн, каждый модуль состоит из типа структуры и определения процесса
Тип ресурса и глобальный механизм хранения обеспечивают безопасность хранения и ресурсов
Имплементация проверок безопасности на этапе компиляции с помощью инвариантов и валидаторов байт-кода
Виртуальная машина проверяет три типа проверок:
Проверка законности структуры
Семантическое обнаружение логики процесса
Обнаружение ошибок при подключении
С помощью этих механизмов Move может обеспечить высокую безопасность уже на этапе компиляции.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может напрямую обращаться к системной памяти. Ее состояние состоит из стека вызовов, памяти, глобальных переменных и операционного массива.
В отличие от EVM, MoveVM разделяет хранение данных и стек вызовов. Пользовательское состояние хранится независимо, а вызовы программ должны соответствовать правилам доступа и ресурсам. Этот дизайн повышает безопасность и эффективность выполнения.
3. Переместить доказательства
Move Prover — это инструмент формальной верификации, который использует алгоритмы дедуктивной верификации для проверки соответствия программы ожидаемым требованиям. Процесс верификации следующий:
Получить исходные файлы Move и спецификации
Компиляция в байт-код и модель объекта валидатора
Перевести на промежуточный язык Boogie
Генерация условий проверки
Проверка с помощью решателя Z3
Генерация диагностического отчета
Язык спецификаций Move используется для описания систем спецификаций и является подмножеством языка Move.
В целом, Move Prover является мощным инструментом безопасности, но не может полностью заменить ручной аудит. Рекомендуется, чтобы разработчики по-прежнему использовали услуги стороннего аудита безопасности и передали часть спецификаций специализированным компаниям по безопасности.
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
Анализ безопасности языка Move: особенности языка, механизм выполнения и Формальная верификация
Анализ безопасности языка Move
Язык Move, как язык смарт-контрактов нового поколения, изначально учитывал проблемы безопасности блокчейна и смарт-контрактов в своем дизайне. В данной статье будет исследоваться безопасность языка Move с трех аспектов: особенностей языка, механизма выполнения и инструментов верификации.
1. Безопасные характеристики языка Move
Язык Move обладает следующими основными характеристиками безопасности:
Виртуальная машина проверяет три типа проверок:
С помощью этих механизмов Move может обеспечить высокую безопасность уже на этапе компиляции.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может напрямую обращаться к системной памяти. Ее состояние состоит из стека вызовов, памяти, глобальных переменных и операционного массива.
В отличие от EVM, MoveVM разделяет хранение данных и стек вызовов. Пользовательское состояние хранится независимо, а вызовы программ должны соответствовать правилам доступа и ресурсам. Этот дизайн повышает безопасность и эффективность выполнения.
3. Переместить доказательства
Move Prover — это инструмент формальной верификации, который использует алгоритмы дедуктивной верификации для проверки соответствия программы ожидаемым требованиям. Процесс верификации следующий:
Язык спецификаций Move используется для описания систем спецификаций и является подмножеством языка Move.
В целом, Move Prover является мощным инструментом безопасности, но не может полностью заменить ручной аудит. Рекомендуется, чтобы разработчики по-прежнему использовали услуги стороннего аудита безопасности и передали часть спецификаций специализированным компаниям по безопасности.