Анализ безопасности языка Move: прорыв нового поколения смарт-контрактов
Язык Move является языком смарт-контрактов, разработанным для блокчейн-окружения и обладающим уникальными характеристиками безопасности. В данной статье рассматриваются особенности языка, механизм работы и инструменты верификации с точки зрения безопасности языка Move.
1. Безопасные характеристики языка Move
Язык Move отказался от более гибких, но небезопасных характеристик, таких как динамическая диспетчеризация и рекурсивные внешние вызовы, и вместо этого использует такие концепции, как обобщения, глобальное хранилище и ресурсы для реализации альтернативных моделей программирования. Эти разработки помогают избежать таких распространенных уязвимостей, как повторный ввод.
Основные механизмы безопасности Move включают:
Модуль: каждый модуль состоит из определения типа структуры и определения процесса, может импортировать определения типов других модулей и вызывать их процессы.
Структура: может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Процесс: определяет функции и логику контракта.
Глобальное хранилище: позволяет постоянно хранить данные, доступ к которым может быть получен только программным способом владельцем модуля.
Проверка инвариантов: определение консервируемости состояния системы с помощью языков спецификаций.
Проверка байт-кода: Принудительное соблюдение типовой системы на уровне байт-кода для предотвращения незаконных операций с чувствительными значениями.
2. Механизм работы Move
Программа Move выполняется в виртуальной машине и не может напрямую обращаться к системной памяти. MoveVM использует стековый интерпретатор для выполнения байт-кодовых инструкций, разделяя управление хранилищем данных и стеком вызовов.
Состояние программы Move состоит из стека вызовов, памяти, глобальных переменных и операций. В процессе выполнения стек вызовов сохраняет информацию о контексте, статические переходы избегают динамической диспетчеризации, тем самым усиливая неизменность вызова функции.
Этот дизайн отделяет состояние пользователя (, ресурсы ) и программную логику, что повышает безопасность и эффективность исполнения.
3. Переместить Провер
Move Prover — это инструмент формальной верификации, который использует алгоритмы дедуктивной проверки для проверки соответствия программы ожиданиям. Его рабочий процесс следующий:
Получить исходные файлы Move и спецификации
Компиляция в байт-код и объектную модель валидатора
Преобразовать в промежуточный язык Boogie
Генерация условий проверки
Используйте решатель Z3 для проверки выполнимости формулы
Генерация диагностического отчета
Язык спецификации Move используется для описания нормативов поведения программы и может быть написан независимо от бизнес-кода. Это предоставляет третьим лицам, занимающимся безопасностью, дополнительный способ верификации.
Резюме
Язык Move был разработан с учетом безопасности; все аспекты, от особенностей языка до выполнения на виртуальной машине и инструментов верификации, были тщательно оптимизированы. Он эффективно предотвращает общие уязвимости, такие как повторные входы и переполнение, но все же необходимо обращать внимание на проблемы безопасности в таких аспектах, как аутентификация и логика.
Хотя Move предлагает хорошую безопасность, рекомендуется, чтобы разработчики все же использовали услуги стороннего аудита и рассматривали возможность передачи написания и проверки спецификаций профессиональным командам безопасности для повышения безопасности смарт-контрактов.
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
11 Лайков
Награда
11
9
Поделиться
комментарий
0/400
DaoResearcher
· 07-23 18:12
Ссылаясь на третью главу теоретической работы Виталика, такой стековый дизайн более безопасен в более чем 67% случаев по сравнению с EVM.
Посмотреть ОригиналОтветить0
ShibaOnTheRun
· 07-23 17:08
Аудит, аудит, всё равно нужен аудит.
Посмотреть ОригиналОтветить0
BearMarketSurvivor
· 07-23 03:14
move такой мощный? Учись!
Посмотреть ОригиналОтветить0
NullWhisperer
· 07-23 01:37
теоретически безопасно, все равно требует пен-тестирования... типичное самодовольство в формальных методах, если честно
Анализ характеристик безопасности языка Move: создание более безопасной среды разработки смарт-контрактов
Анализ безопасности языка Move: прорыв нового поколения смарт-контрактов
Язык Move является языком смарт-контрактов, разработанным для блокчейн-окружения и обладающим уникальными характеристиками безопасности. В данной статье рассматриваются особенности языка, механизм работы и инструменты верификации с точки зрения безопасности языка Move.
1. Безопасные характеристики языка Move
Язык Move отказался от более гибких, но небезопасных характеристик, таких как динамическая диспетчеризация и рекурсивные внешние вызовы, и вместо этого использует такие концепции, как обобщения, глобальное хранилище и ресурсы для реализации альтернативных моделей программирования. Эти разработки помогают избежать таких распространенных уязвимостей, как повторный ввод.
Основные механизмы безопасности Move включают:
Модуль: каждый модуль состоит из определения типа структуры и определения процесса, может импортировать определения типов других модулей и вызывать их процессы.
Структура: может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Процесс: определяет функции и логику контракта.
Глобальное хранилище: позволяет постоянно хранить данные, доступ к которым может быть получен только программным способом владельцем модуля.
Проверка инвариантов: определение консервируемости состояния системы с помощью языков спецификаций.
Проверка байт-кода: Принудительное соблюдение типовой системы на уровне байт-кода для предотвращения незаконных операций с чувствительными значениями.
2. Механизм работы Move
Программа Move выполняется в виртуальной машине и не может напрямую обращаться к системной памяти. MoveVM использует стековый интерпретатор для выполнения байт-кодовых инструкций, разделяя управление хранилищем данных и стеком вызовов.
Состояние программы Move состоит из стека вызовов, памяти, глобальных переменных и операций. В процессе выполнения стек вызовов сохраняет информацию о контексте, статические переходы избегают динамической диспетчеризации, тем самым усиливая неизменность вызова функции.
Этот дизайн отделяет состояние пользователя (, ресурсы ) и программную логику, что повышает безопасность и эффективность исполнения.
3. Переместить Провер
Move Prover — это инструмент формальной верификации, который использует алгоритмы дедуктивной проверки для проверки соответствия программы ожиданиям. Его рабочий процесс следующий:
Язык спецификации Move используется для описания нормативов поведения программы и может быть написан независимо от бизнес-кода. Это предоставляет третьим лицам, занимающимся безопасностью, дополнительный способ верификации.
Резюме
Язык Move был разработан с учетом безопасности; все аспекты, от особенностей языка до выполнения на виртуальной машине и инструментов верификации, были тщательно оптимизированы. Он эффективно предотвращает общие уязвимости, такие как повторные входы и переполнение, но все же необходимо обращать внимание на проблемы безопасности в таких аспектах, как аутентификация и логика.
Хотя Move предлагает хорошую безопасность, рекомендуется, чтобы разработчики все же использовали услуги стороннего аудита и рассматривали возможность передачи написания и проверки спецификаций профессиональным командам безопасности для повышения безопасности смарт-контрактов.