Move является языком смарт-контрактов, который может компилироваться и выполняться в среде блокчейна, реализующей MoveVM. При его проектировании были учтены многие вопросы безопасности, связанные с блокчейном и смарт-контрактами, и заимствованы некоторые идеи по безопасности из языка RUST. Какова же безопасность Move, нового поколения языков смарт-контрактов, основным признаком которого является безопасность? Может ли он избежать распространенных угроз безопасности виртуальных машин контрактов, таких как EVM и WASM, на уровне языка или связанных механизмов? Существуют ли у самого Move специфические проблемы безопасности?
В этой статье будет рассмотрена безопасность языка Move с трех точек зрения: языковые особенности, механизмы выполнения и инструменты проверки.
1. Безопасные характеристики языка Move
Написание безошибочного кода является сложной задачей, и даже после многократного тестирования невозможно полностью гарантировать его безопасность. При взаимодействии с ненадежным кодом написание кода, который сохраняет ключевые свойства безопасности, становится еще более сложной задачей. Существует множество технологий, которые могут обеспечить безопасность во время выполнения, такие как песочницы, изоляция процессов, блокировки объектов и другие программные модели; также можно задать статическую безопасность на этапе компиляции, например, с помощью строгой статической типизации или проверки утверждений.
Иногда также можно воспользоваться инструментами семантического анализа и статического анализа, чтобы обеспечить соответствие кода правилам безопасности, даже при взаимодействии с ненадежным кодом, сохраняя при этом некоторые доказуемые логические инварианты. Эти методы выглядят неплохо, поскольку могут избежать накладных расходов во время выполнения и заранее обнаружить проблемы безопасности. Однако безопасность, полученная языками программирования с помощью этих методов, чрезвычайно ограничена по двум причинам: во-первых, они обычно имеют языковые особенности, которые трудно анализировать с помощью статических инструментов, такие как динамическое распределение, совместная изменяемость и отражение, которые нарушают правила безопасности инвариантов и предоставляют злоумышленникам широкий спектр возможностей для атак. Во-вторых, большинству языков программирования сложно расширять свои возможности для поддержки статических инструментов, связанных с безопасностью, или выразительных инвариантов, хотя оба этих расширения имеют важное значение.
Дизайн языка Move поддерживает безопасное взаимодействие с ненадежным кодом и статическую проверку. Он обладает этими безопасными характеристиками, потому что отказался от всей нелинейной логики, основанной на соображениях гибкости, не поддерживает динамическое распределение и не поддерживает рекурсивные внешние вызовы, вместо этого использует концепции обобщений, глобального хранилища, ресурсов и т.д. для реализации некоторых альтернативных программных моделей. Например, Move опускает динамическое распределение и рекурсивные вызовы, которые в других языках смарт-контрактов приводят к дорогостоящим уязвимостям повторного входа.
Основные характеристики безопасности языка Move включают:
Модульность: каждый модуль Move состоит из серии определений структур и процессов. Модули могут импортировать определения типов, объявленные в других модулях, и вызывать процессы.
Структура: можно определить структуру типа ресурса, используемую для представления данных, которые можно хранить в глобальном хранилище ключей/значений.
Процесс: определены инициализация, безопасные и небезопасные процессы. Процессы могут иметь ограничения доступа.
Глобальное хранилище: позволяет хранить постоянные данные, которые могут быть прочитаны и записаны программно только тем модулем, который их владеет.
Проверка инвариантов: можно определить статические проверки инвариантов, чтобы обеспечить целостность ресурсов в системе.
Верификатор байткода: принудительное соблюдение системы типов на уровне байткода, предотвращающее неправомерное создание, распаковку или ссылку на ресурсы.
Эти характеристики позволяют Move обеспечивать мощную безопасность как на этапе компиляции, так и во время выполнения.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может напрямую обращаться к системной памяти, что обеспечивает ее безопасное выполнение в ненадежной среде.
Move использует стековую модель выполнения. Глобальное хранилище делится на память ( кучу ) и глобальные переменные ( стек ). Память является первым уровнем хранения и не может хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, доступ к ним осуществляется через адрес и тип.
Move использует стековый интерпретатор для выполнения байт-кода, этот способ легко реализовать и контролировать, он требует низких аппаратных ресурсов и подходит для блокчейн-сценариев. В отличие от регистрового интерпретатора, стековый интерпретатор легче контролировать и отслеживать копирование и перемещение между переменными.
Состояние программы Move во время выполнения представляется кортежем из четырех элементов ⟨C, M, G, S⟩, включая стек вызовов (C), память (M), глобальные переменные (G) и стек операндов (S). Стек вызовов содержит информацию о контексте выполнения процедуры и номера инструкций. При выполнении инструкции Call создается новый объект стека вызовов, в который сохраняются параметры и выполняются инструкции нового контракта. При встрече с инструкцией ветвления выполняется статический переход внутри процедуры.
MoveVM разделяет хранилище данных и стек вызовов, что является его главным отличием от EVM. В Move ресурсы по адресу аккаунта пользователя ( хранятся отдельно, а вызовы программ должны соответствовать правилам доступа и ресурсам. Такой дизайн жертвует определенной гибкостью, но повышает безопасность и эффективность исполнения.
![Анализ безопасности Move: игра в изменении языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. Переместить Провер
Move Prover — это инструмент формальной верификации, основанный на логическом выводе, который может помочь разработчикам обеспечить правильность смарт-контрактов и снизить риски транзакций. Он использует формальный язык для описания поведения программы и проверяет, соответствует ли программа ожиданиям с помощью алгоритмов вывода.
Move Prover использует алгоритм дедуктивной проверки, чтобы на основе известных данных сделать вывод о поведении программы и гарантировать его соответствие ожиданиям. Это помогает обеспечить корректность программы и уменьшить объем ручного тестирования.
Рабочий процесс Move Prover следующий:
Принимаем исходный файл Move в качестве входных данных, который содержит спецификации программы.
Парсер извлекает спецификации, компилятор компилирует исходный код в байт-код
Генерация модели объекта валидатора
Переведите модель в промежуточный язык Boogie
Система верификации Boogie генерирует условия для верификации
Передать условия проверки в решатель Z3 для проверки
Генерация диагностического отчета и преобразование в исходный код ошибок
Move предоставляет язык спецификаций Move Specification Language для описания спецификаций, который является подмножеством языка Move и поддерживает статическое описание корректности поведения программ. Спецификации можно писать независимо от бизнес-кода.
Move Prover является мощным инструментом, который помогает разработчикам гарантировать правильность смарт-контрактов и снижать риски транзакций. Он использует формализованные методы для проверки того, соответствует ли программа ожиданиям, что повышает уверенность разработчиков при развертывании смарт-контрактов.
![Анализ безопасности Move: Игра, меняющая правила для языков смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
Итог
Язык Move уделяет всестороннее внимание безопасности, обеспечивая мощные гарантии как через особенности языка, так и через выполнение виртуальной машины и инструменты безопасности. Он жертвует определенной гибкостью, вводя обязательную проверку типов и линейную логику, что способствует автоматизации компиляционных проверок и формальной верификации. Дизайн MoveVM отделяет состояние от логики, что лучше соответствует требованиям безопасности управления активами в блокчейне.
Язык Move может эффективно избежать распространенных уязвимостей в EVM, таких как повторный вход, переполнение, инъекции Call/DelegateCall и т. д. Однако разработчики все равно должны уделять особое внимание вопросам аутентификации, логике кода и переполнению структур больших целых чисел. Хотя Move Prover мощный, он не может полностью избежать упущений в общей конструкции.
Несмотря на то, что Move уделяет много внимания безопасности, не существует полностью безопасных языков и программ. Рекомендуется разработчикам смарт-контрактов на Move по-прежнему использовать услуги аудита третьих сторон и передавать написание и проверку нормативных частей профессиональным командам безопасности.
![Анализ безопасности Move: Игра с языком смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
23 Лайков
Награда
23
7
Поделиться
комментарий
0/400
GasFeeWhisperer
· 23ч назад
move обновил понимание, вот что называется безопасностью
Посмотреть ОригиналОтветить0
GasGasGasBro
· 08-03 23:15
Слишком сложно, каждый раз, когда смотрю на безопасность, лысею.
Посмотреть ОригиналОтветить0
ForkTongue
· 08-03 07:07
move - это действительно волшебная вещь, мы на самом деле не можем понять.
Глубина безопасных характеристик языка Move: от проектирования языка до Формальная верификация
Анализ безопасности языка Move
Введение
Move является языком смарт-контрактов, который может компилироваться и выполняться в среде блокчейна, реализующей MoveVM. При его проектировании были учтены многие вопросы безопасности, связанные с блокчейном и смарт-контрактами, и заимствованы некоторые идеи по безопасности из языка RUST. Какова же безопасность Move, нового поколения языков смарт-контрактов, основным признаком которого является безопасность? Может ли он избежать распространенных угроз безопасности виртуальных машин контрактов, таких как EVM и WASM, на уровне языка или связанных механизмов? Существуют ли у самого Move специфические проблемы безопасности?
В этой статье будет рассмотрена безопасность языка Move с трех точек зрения: языковые особенности, механизмы выполнения и инструменты проверки.
1. Безопасные характеристики языка Move
Написание безошибочного кода является сложной задачей, и даже после многократного тестирования невозможно полностью гарантировать его безопасность. При взаимодействии с ненадежным кодом написание кода, который сохраняет ключевые свойства безопасности, становится еще более сложной задачей. Существует множество технологий, которые могут обеспечить безопасность во время выполнения, такие как песочницы, изоляция процессов, блокировки объектов и другие программные модели; также можно задать статическую безопасность на этапе компиляции, например, с помощью строгой статической типизации или проверки утверждений.
Иногда также можно воспользоваться инструментами семантического анализа и статического анализа, чтобы обеспечить соответствие кода правилам безопасности, даже при взаимодействии с ненадежным кодом, сохраняя при этом некоторые доказуемые логические инварианты. Эти методы выглядят неплохо, поскольку могут избежать накладных расходов во время выполнения и заранее обнаружить проблемы безопасности. Однако безопасность, полученная языками программирования с помощью этих методов, чрезвычайно ограничена по двум причинам: во-первых, они обычно имеют языковые особенности, которые трудно анализировать с помощью статических инструментов, такие как динамическое распределение, совместная изменяемость и отражение, которые нарушают правила безопасности инвариантов и предоставляют злоумышленникам широкий спектр возможностей для атак. Во-вторых, большинству языков программирования сложно расширять свои возможности для поддержки статических инструментов, связанных с безопасностью, или выразительных инвариантов, хотя оба этих расширения имеют важное значение.
Дизайн языка Move поддерживает безопасное взаимодействие с ненадежным кодом и статическую проверку. Он обладает этими безопасными характеристиками, потому что отказался от всей нелинейной логики, основанной на соображениях гибкости, не поддерживает динамическое распределение и не поддерживает рекурсивные внешние вызовы, вместо этого использует концепции обобщений, глобального хранилища, ресурсов и т.д. для реализации некоторых альтернативных программных моделей. Например, Move опускает динамическое распределение и рекурсивные вызовы, которые в других языках смарт-контрактов приводят к дорогостоящим уязвимостям повторного входа.
Основные характеристики безопасности языка Move включают:
Модульность: каждый модуль Move состоит из серии определений структур и процессов. Модули могут импортировать определения типов, объявленные в других модулях, и вызывать процессы.
Структура: можно определить структуру типа ресурса, используемую для представления данных, которые можно хранить в глобальном хранилище ключей/значений.
Процесс: определены инициализация, безопасные и небезопасные процессы. Процессы могут иметь ограничения доступа.
Глобальное хранилище: позволяет хранить постоянные данные, которые могут быть прочитаны и записаны программно только тем модулем, который их владеет.
Проверка инвариантов: можно определить статические проверки инвариантов, чтобы обеспечить целостность ресурсов в системе.
Верификатор байткода: принудительное соблюдение системы типов на уровне байткода, предотвращающее неправомерное создание, распаковку или ссылку на ресурсы.
Эти характеристики позволяют Move обеспечивать мощную безопасность как на этапе компиляции, так и во время выполнения.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может напрямую обращаться к системной памяти, что обеспечивает ее безопасное выполнение в ненадежной среде.
Move использует стековую модель выполнения. Глобальное хранилище делится на память ( кучу ) и глобальные переменные ( стек ). Память является первым уровнем хранения и не может хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, доступ к ним осуществляется через адрес и тип.
Move использует стековый интерпретатор для выполнения байт-кода, этот способ легко реализовать и контролировать, он требует низких аппаратных ресурсов и подходит для блокчейн-сценариев. В отличие от регистрового интерпретатора, стековый интерпретатор легче контролировать и отслеживать копирование и перемещение между переменными.
Состояние программы Move во время выполнения представляется кортежем из четырех элементов ⟨C, M, G, S⟩, включая стек вызовов (C), память (M), глобальные переменные (G) и стек операндов (S). Стек вызовов содержит информацию о контексте выполнения процедуры и номера инструкций. При выполнении инструкции Call создается новый объект стека вызовов, в который сохраняются параметры и выполняются инструкции нового контракта. При встрече с инструкцией ветвления выполняется статический переход внутри процедуры.
MoveVM разделяет хранилище данных и стек вызовов, что является его главным отличием от EVM. В Move ресурсы по адресу аккаунта пользователя ( хранятся отдельно, а вызовы программ должны соответствовать правилам доступа и ресурсам. Такой дизайн жертвует определенной гибкостью, но повышает безопасность и эффективность исполнения.
![Анализ безопасности Move: игра в изменении языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. Переместить Провер
Move Prover — это инструмент формальной верификации, основанный на логическом выводе, который может помочь разработчикам обеспечить правильность смарт-контрактов и снизить риски транзакций. Он использует формальный язык для описания поведения программы и проверяет, соответствует ли программа ожиданиям с помощью алгоритмов вывода.
Move Prover использует алгоритм дедуктивной проверки, чтобы на основе известных данных сделать вывод о поведении программы и гарантировать его соответствие ожиданиям. Это помогает обеспечить корректность программы и уменьшить объем ручного тестирования.
Рабочий процесс Move Prover следующий:
Move предоставляет язык спецификаций Move Specification Language для описания спецификаций, который является подмножеством языка Move и поддерживает статическое описание корректности поведения программ. Спецификации можно писать независимо от бизнес-кода.
Move Prover является мощным инструментом, который помогает разработчикам гарантировать правильность смарт-контрактов и снижать риски транзакций. Он использует формализованные методы для проверки того, соответствует ли программа ожиданиям, что повышает уверенность разработчиков при развертывании смарт-контрактов.
![Анализ безопасности Move: Игра, меняющая правила для языков смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
Итог
Язык Move уделяет всестороннее внимание безопасности, обеспечивая мощные гарантии как через особенности языка, так и через выполнение виртуальной машины и инструменты безопасности. Он жертвует определенной гибкостью, вводя обязательную проверку типов и линейную логику, что способствует автоматизации компиляционных проверок и формальной верификации. Дизайн MoveVM отделяет состояние от логики, что лучше соответствует требованиям безопасности управления активами в блокчейне.
Язык Move может эффективно избежать распространенных уязвимостей в EVM, таких как повторный вход, переполнение, инъекции Call/DelegateCall и т. д. Однако разработчики все равно должны уделять особое внимание вопросам аутентификации, логике кода и переполнению структур больших целых чисел. Хотя Move Prover мощный, он не может полностью избежать упущений в общей конструкции.
Несмотря на то, что Move уделяет много внимания безопасности, не существует полностью безопасных языков и программ. Рекомендуется разработчикам смарт-контрактов на Move по-прежнему использовать услуги аудита третьих сторон и передавать написание и проверку нормативных частей профессиональным командам безопасности.
![Анализ безопасности Move: Игра с языком смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(