Анализ безопасности языка Move: революционер языка смарт-контрактов
Введение
Язык Move является языком смарт-контрактов, который может работать в блокчейн-среде, реализующей MoveVM. Его дизайн изначально учитывал множество вопросов безопасности, связанных с блокчейном и смарт-контрактами, и заимствовал некоторые концепции безопасности из языка Rust. Какова безопасность Move как нового поколения языков смарт-контрактов, для которого основной характеристикой является безопасность? Может ли он избежать распространенных угроз безопасности, присущих виртуальным машинам контрактов, таким как EVM и WASM, на уровне языка или через связанные механизмы? Существуют ли у Move собственные специфические проблемы безопасности?
В данной статье будут рассмотрены проблемы безопасности языка Move с трех аспектов: языковые особенности, механизмы работы и инструменты верификации.
1. Безопасные характеристики языка Move
В отличие от многих существующих языков программирования, язык Move был разработан для обеспечения безопасного взаимодействия как с ненадежным кодом, так и для поддержки статической проверки. Move отказался от нелинейной логики, основанной на гибкости, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы, а вместо этого использует концепции, такие как обобщения, глобальное хранилище, ресурсы и т.д., для реализации альтернативных моделей программирования. Например, Move опускает динамическую диспетчеризацию и рекурсивные вызовы, которые могут привести к уязвимостям повторного входа.
Основные функции безопасности Move включают:
Модуль: каждый модуль Move состоит из серии определений структур и процедур. Модуль может импортировать определения типов и вызывать процедуры, объявленные в других модулях.
Структура: может быть определена как тип ресурса, который может быть сохранен в постоянном глобальном хранилище ключ/значение.
Процесс: определены инициализация, безопасный процесс и небезопасный процесс.
Глобальное хранилище: позволяет программам Move хранить постоянные данные, которые могут быть прочитаны и записаны программным образом только модулем, которому они принадлежат.
Проверка инвариантов: поддержка статической проверки инвариантов, гарантирующая целостность ресурсов в системе.
Байт-код валидатор: принудительное выполнение системы типов на уровне байт-кода, предотвращающее незаконные действия злонамеренных клиентских модулей.
Два механизма, такие как проверка инвариантов и валидатор байт-кода, обеспечивают двойную защиту безопасности кода в Move на этапе компиляции.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может получать доступ к системной памяти во время выполнения. Это позволяет Move безопасно работать в ненадежной среде, не подвергаясь разрушению или злоупотреблению.
Программа Move выполняется на стеке, глобальное хранилище делится на память (, кучу ) и глобальные переменные ( стек ) на две части. Память является первичным хранилищем, ее ячейки не могут хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, но способ индексации отличается от памяти.
Байткод инструкций Move выполняется в стековом интерпретаторе. Стековая виртуальная машина легко реализуется и контролируется, требует меньше аппаратных ресурсов, что делает ее подходящей для блокчейн-сценариев. В отличие от регистрового интерпретатора, стековый интерпретатор позволяет легче контролировать и отслеживать операции копирования и перемещения между переменными.
Состояние выполнения программы Move представлено кортежем ⟨C, M, G, S⟩, который включает в себя стек вызовов (C), память (M), глобальные переменные (G) и операнды (S). Стек также поддерживает таблицу функций для разбора инструкций, содержащих тело функции.
MoveVM отделяет логику процесса хранения данных и стека вызовов (, что является самым большим отличием от EVM. В MoveVM ресурсы ) под адресом учетной записи состояния пользователя ( хранятся независимо, а вызовы программы должны соответствовать обязательным правилам, связанным с правами и ресурсами. Эта конструкция жертвует определенной гибкостью, но значительно улучшает безопасность и эффективность выполнения ), способствуя реализации параллельного выполнения (.
![Анализ безопасности Move: Game Changer для языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. Доказывающий ход
Move Prover является инструментом формальной верификации, основанным на логическом выводе. Он использует формальный язык для описания поведения программы и применяет алгоритмы вывода для проверки соответствия программы ожидаемым результатам, помогая разработчикам обеспечить правильность смарт-контрактов и снизить риски транзакций.
Move Prover использует алгоритм дедуктивной верификации для проверки соответствия программы ожидаемому поведению. Это означает, что он может делать выводы о поведении программы на основе известных данных, гарантируя соответствие ожидаемому поведению. Это помогает обеспечить правильность программы и уменьшить объем ручного тестирования.
Рабочий процесс Move Prover следующий:
Получите файл источника Move в качестве входных данных, этот файл должен устанавливать спецификации входных данных программы.
Move Parser извлекает спецификации из исходного кода.
Компилятор Move компилирует исходный файл в байт-код и вместе со стандартной системой преобразует его в модель объекта валидатора.
Модель была переведена на промежуточный язык Boogie.
Код Boogie передается в систему проверки Boogie, генерируя условия проверки.
Условия проверки передаются в Z3-решатель ), разработанный Microsoft SMT-решатель (.
Z3 проверяет, является ли SMT-формула невыполнимой. Если да, то это означает, что спецификация выполнена; в противном случае создается модель, удовлетворяющая условиям.
Восстановите отчет о диагностике в исходный код ошибки.
Move использует язык спецификаций Move для описания спецификаций системы. Это подмножество языка Move, поддерживающее статическое описание правильности поведения программы, не влияя на производство. Может быть независимо написано как специализированный документ спецификации, отделяющий бизнес-код от кода формальной проверки.
Move Prover — это полезный инструмент, который помогает разработчикам обеспечить правильность смарт-контрактов. Он использует формальный язык для описания поведения программы и применяет алгоритмы вывода для проверки соответствия программы ожиданиям, что помогает снизить риски транзакций и позволяет разработчикам более уверенно развертывать смарт-контракты в производственной среде.
![Анализ безопасности Move: Game Changer языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Итоги
Язык Move обладает выдающимися характеристиками безопасности, учитывая все аспекты языковых особенностей, выполнения виртуальной машины и инструментов безопасности. Языковые особенности жертвуют некоторой гибкостью, принудительная типизация и линейная логика облегчают автоматизацию проверки компиляции и формальную верификацию, а также безопасность верификации. Дизайн MoveVM отделяет состояние от логики, что больше соответствует требованиям безопасного управления активами в блокчейне.
На языковом уровне Move может эффективно избегать распространенных уязвимостей EVM, таких как повторный ввод, переполнение, инъекции Call/DeleGateCall и другие. Однако разработчики все еще должны обращать внимание на проблемы, такие как аутентификация, логика кода и переполнение структур больших целых чисел. Move Prover может не сработать в случае общей невнимательности.
Хотя язык Move учитывает множество аспектов безопасности для программистов, полностью безопасных языков и программ не существует. Рекомендуется разработчикам смарт-контрактов на Move использовать услуги аудита от третьих сторон и передать написание и проверку части спецификации кода на аутсорсинг третьим сторонам.
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
Безопасность языка Move: новая парадигма смарт-контрактов
Анализ безопасности языка Move: революционер языка смарт-контрактов
Введение
Язык Move является языком смарт-контрактов, который может работать в блокчейн-среде, реализующей MoveVM. Его дизайн изначально учитывал множество вопросов безопасности, связанных с блокчейном и смарт-контрактами, и заимствовал некоторые концепции безопасности из языка Rust. Какова безопасность Move как нового поколения языков смарт-контрактов, для которого основной характеристикой является безопасность? Может ли он избежать распространенных угроз безопасности, присущих виртуальным машинам контрактов, таким как EVM и WASM, на уровне языка или через связанные механизмы? Существуют ли у Move собственные специфические проблемы безопасности?
В данной статье будут рассмотрены проблемы безопасности языка Move с трех аспектов: языковые особенности, механизмы работы и инструменты верификации.
1. Безопасные характеристики языка Move
В отличие от многих существующих языков программирования, язык Move был разработан для обеспечения безопасного взаимодействия как с ненадежным кодом, так и для поддержки статической проверки. Move отказался от нелинейной логики, основанной на гибкости, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы, а вместо этого использует концепции, такие как обобщения, глобальное хранилище, ресурсы и т.д., для реализации альтернативных моделей программирования. Например, Move опускает динамическую диспетчеризацию и рекурсивные вызовы, которые могут привести к уязвимостям повторного входа.
Основные функции безопасности Move включают:
Модуль: каждый модуль Move состоит из серии определений структур и процедур. Модуль может импортировать определения типов и вызывать процедуры, объявленные в других модулях.
Структура: может быть определена как тип ресурса, который может быть сохранен в постоянном глобальном хранилище ключ/значение.
Процесс: определены инициализация, безопасный процесс и небезопасный процесс.
Глобальное хранилище: позволяет программам Move хранить постоянные данные, которые могут быть прочитаны и записаны программным образом только модулем, которому они принадлежат.
Проверка инвариантов: поддержка статической проверки инвариантов, гарантирующая целостность ресурсов в системе.
Байт-код валидатор: принудительное выполнение системы типов на уровне байт-кода, предотвращающее незаконные действия злонамеренных клиентских модулей.
Два механизма, такие как проверка инвариантов и валидатор байт-кода, обеспечивают двойную защиту безопасности кода в Move на этапе компиляции.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может получать доступ к системной памяти во время выполнения. Это позволяет Move безопасно работать в ненадежной среде, не подвергаясь разрушению или злоупотреблению.
Программа Move выполняется на стеке, глобальное хранилище делится на память (, кучу ) и глобальные переменные ( стек ) на две части. Память является первичным хранилищем, ее ячейки не могут хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, но способ индексации отличается от памяти.
Байткод инструкций Move выполняется в стековом интерпретаторе. Стековая виртуальная машина легко реализуется и контролируется, требует меньше аппаратных ресурсов, что делает ее подходящей для блокчейн-сценариев. В отличие от регистрового интерпретатора, стековый интерпретатор позволяет легче контролировать и отслеживать операции копирования и перемещения между переменными.
Состояние выполнения программы Move представлено кортежем ⟨C, M, G, S⟩, который включает в себя стек вызовов (C), память (M), глобальные переменные (G) и операнды (S). Стек также поддерживает таблицу функций для разбора инструкций, содержащих тело функции.
MoveVM отделяет логику процесса хранения данных и стека вызовов (, что является самым большим отличием от EVM. В MoveVM ресурсы ) под адресом учетной записи состояния пользователя ( хранятся независимо, а вызовы программы должны соответствовать обязательным правилам, связанным с правами и ресурсами. Эта конструкция жертвует определенной гибкостью, но значительно улучшает безопасность и эффективность выполнения ), способствуя реализации параллельного выполнения (.
![Анализ безопасности Move: Game Changer для языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. Доказывающий ход
Move Prover является инструментом формальной верификации, основанным на логическом выводе. Он использует формальный язык для описания поведения программы и применяет алгоритмы вывода для проверки соответствия программы ожидаемым результатам, помогая разработчикам обеспечить правильность смарт-контрактов и снизить риски транзакций.
Move Prover использует алгоритм дедуктивной верификации для проверки соответствия программы ожидаемому поведению. Это означает, что он может делать выводы о поведении программы на основе известных данных, гарантируя соответствие ожидаемому поведению. Это помогает обеспечить правильность программы и уменьшить объем ручного тестирования.
Рабочий процесс Move Prover следующий:
Move использует язык спецификаций Move для описания спецификаций системы. Это подмножество языка Move, поддерживающее статическое описание правильности поведения программы, не влияя на производство. Может быть независимо написано как специализированный документ спецификации, отделяющий бизнес-код от кода формальной проверки.
Move Prover — это полезный инструмент, который помогает разработчикам обеспечить правильность смарт-контрактов. Он использует формальный язык для описания поведения программы и применяет алгоритмы вывода для проверки соответствия программы ожиданиям, что помогает снизить риски транзакций и позволяет разработчикам более уверенно развертывать смарт-контракты в производственной среде.
![Анализ безопасности Move: Game Changer языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Итоги
Язык Move обладает выдающимися характеристиками безопасности, учитывая все аспекты языковых особенностей, выполнения виртуальной машины и инструментов безопасности. Языковые особенности жертвуют некоторой гибкостью, принудительная типизация и линейная логика облегчают автоматизацию проверки компиляции и формальную верификацию, а также безопасность верификации. Дизайн MoveVM отделяет состояние от логики, что больше соответствует требованиям безопасного управления активами в блокчейне.
На языковом уровне Move может эффективно избегать распространенных уязвимостей EVM, таких как повторный ввод, переполнение, инъекции Call/DeleGateCall и другие. Однако разработчики все еще должны обращать внимание на проблемы, такие как аутентификация, логика кода и переполнение структур больших целых чисел. Move Prover может не сработать в случае общей невнимательности.
Хотя язык Move учитывает множество аспектов безопасности для программистов, полностью безопасных языков и программ не существует. Рекомендуется разработчикам смарт-контрактов на Move использовать услуги аудита от третьих сторон и передать написание и проверку части спецификации кода на аутсорсинг третьим сторонам.