Анализ безопасности языка Move: изменяющий правила игры язык смарт-контрактов
Язык Move — это язык смарт-контрактов, который можно компилировать и запускать в блокчейн-среде с реализованной MoveVM. С самого начала своего создания он учитывал множество проблем безопасности блокчейнов и смарт-контрактов, а также заимствовал некоторые элементы дизайна безопасности из языка RUST. Какова же безопасность Move как нового поколения языка смарт-контрактов с основным акцентом на безопасность? Может ли он избежать распространенных угроз безопасности, присущих виртуальным машинам контрактов, таким как EVM и WASM, на уровне языка или связанных механизмов? Существуют ли у него собственные уникальные проблемы безопасности?
В данной статье будет рассмотрена проблема безопасности языка Move с трех аспектов: языковых особенностей, механизма работы и инструментов верификации.
1. Безопасные характеристики языка Move
В отличие от многих существующих языков программирования, язык Move был разработан с целью поддержки написания программ, которые могут безопасно взаимодействовать с ненадежным кодом, при этом поддерживая статическую проверку. Для достижения этой цели Move отказался от нелинейной логики, основанной на гибкости, не поддерживает динамическое распределение и рекурсивные внешние вызовы, вместо этого вводя концепции, такие как обобщения, глобальное хранилище, ресурсы и т.д., для реализации альтернативной модели программирования. Например, Move опустил характеристики динамического распределения и рекурсивных вызовов, которые в других языках смарт-контрактов могут привести к дорогостоящим уязвимостям повторного входа.
Основные функции безопасности Move включают:
Модуль (Module): Каждый модуль Move состоит из ряда определений типов структур и процедур. Модуль может импортировать определения типов, объявленные в других модулях, и вызывать процедуры.
Структуры(: могут быть определены как типы ресурсов, представляющие данные, которые могут храниться в постоянном глобальном хранилище ключ/значение.
процесс ) Функция (: определение логики поведения модуля.
Глобальное хранилище: позволяет программе Move хранить постоянные данные, которые могут быть прочитаны и записаны программным образом только модулем, который их владеет.
Проверка инвариантов: можно определить инварианты для статической проверки, чтобы обеспечить сохранение состояния системы.
Байт-код валидатор: принудительное выполнение системы типов на уровне байт-кода, предотвращающее незаконные операции.
Move обеспечивает безопасность кода на этапе компиляции благодаря этим особенностям. Далее мы проанализируем механизм работы Move и посмотрим, как MoveVM обеспечивает безопасность во время выполнения.
![Анализ безопасности Move: смарт-контракты как изменяющий игру язык])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(
2. Механизм работы Move
Программа Move выполняется в виртуальной машине, и во время выполнения она не может получить доступ к системной памяти, что позволяет Move безопасно работать в ненадежной среде. Программа Move выполняется на стеке, глобальное хранилище делится на память ) кучу ( и глобальные переменные ) стек ( на две части. Память является хранилищем первого уровня и не может хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, но способ индексации отличается от памяти.
Байткод инструкций Move выполняется в стековом интерпретаторе. Стековая виртуальная машина проста в реализации и управлении, требует низких требований к аппаратной среде, что делает её подходящей для блокчейн-сценариев. По сравнению с регистровым интерпретатором, стековый интерпретатор легче контролировать и отслеживать копирование и перемещение переменных.
Во время выполнения программы Move ее состояние представлено четырехмерной кортежем ⟨C, M, G, S⟩, который включает: стек вызовов )C(, память )M(, глобальные переменные )G( и операнды )S(. Стек также поддерживает таблицу функций ) и сам модуль ( для разбора инструкций, содержащих тело функции.
MoveVM отделяет логику хранения данных и вызова стека ) от хранения (, что является крупнейшим отличием от EVM. В MoveVM ресурсы ) под адресом учетной записи пользовательского состояния ( хранятся независимо, и вызовы программ должны соответствовать обязательным правилам, связанным с правами доступа и ресурсами. Хотя это жертвует некоторой гибкостью, это значительно улучшает безопасность и эффективность выполнения ), что способствует достижению высокой степени параллельного выполнения (.
![Анализ безопасности Move: смарт-контракты как фактор изменения игры])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. Доказывающий ход
Move Prover — это инструмент формальной верификации на основе вывода. Он использует формальный язык для описания поведения программы и использует алгоритмы вывода для проверки, соответствует ли программа ожиданиям, помогая разработчикам обеспечить правильность смарт-контрактов и тем самым снизить риски транзакций.
Move Prover использует алгоритм дедуктивной верификации для проверки того, соответствует ли программа ожиданиям. Это означает, что Move Prover может, основываясь на известной информации, делать выводы о поведении программы и гарантировать, что оно соответствует ожидаемому поведению. Это помогает обеспечить корректность программы и уменьшить объем ручного тестирования.
Рабочий процесс Move Prover следующий:
Получите файл Move в качестве входных данных, этот файл должен соответствовать спецификации ввода программы )specification(.
Move Parser извлекает спецификацию из исходного кода.
Move компилятор компилирует исходные файлы в байт-код, совместно с нормативной системой преобразует в модель объекта проверяющего )Prover Object Model(.
Переведите модель в промежуточный язык Boogie.
Система проверки Boogie выполняет "генерацию условий проверки")verification condition generation(.
Передать условия проверки в решатель Z3 ), разработанный Microsoft SMT решатель (.
Z3 проверяет, соответствует ли код программы SMT формулы ) спецификации ( и является ли она несоответствующей.
Если не удовлетворяется, это означает, что спецификация подтверждена; в противном случае создается модель, удовлетворяющая условиям, и она преобразуется обратно в формат Boogie для публикации диагностического отчета.
Восстановите диагностический отчет в виде исходного кода ошибки.
Move использует язык спецификаций Move для описания спецификаций системы. Этот язык является подмножеством Move, поддерживает статическое описание корректности поведения программы, не влияя на производство. Можно независимо писать специальные документированные файлы, разделяя бизнес-код и код формальной проверки.
Move Prover — это полезный инструмент, который помогает разработчикам гарантировать корректность смарт-контрактов. Он использует формальный язык для описания поведения программы и применяет алгоритмы вывода для проверки того, соответствует ли программа ожидаемому. Это помогает снизить риски транзакций и позволяет разработчикам более уверенно развертывать смарт-контракты в производственной среде.
![Анализ безопасности Move: Game Changer языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
4. Резюме
Язык Move обладает выдающейся безопасностью, с тщательным учетом языковых особенностей, выполнения виртуальной машины и уровня инструментов безопасности. Языковые особенности жертвуют частью гибкости, принудительная проверка типов и линейная логика облегчают автоматизацию проверки компиляции и формальную верификацию, а также обеспечивают безопасность и возможность верификации. Дизайн MoveVM разделяет состояние и логику, что более соответствует требованиям безопасного управления активами в блокчейне.
С точки зрения языка, Move может эффективно избежать уязвимостей, распространенных в EVM, таких как повторные вызовы, переполнение, инъекции Call/DeleGateCall и т. д. Однако проблемы с аутентификацией, логикой кода и переполнением структур больших целых чисел все еще требуют внимания разработчиков. Move Prover может не сработать, если общий смысл будет упущен.
Несмотря на то, что язык Move учитывает много аспектов безопасности для программистов, не существует абсолютно безопасного языка, и нет абсолютно безопасных программ. Рекомендуется разработчикам смарт-контрактов Move использовать услуги аудита от сторонних компаний по безопасности и передать написание и проверку части кода спецификации сторонним компаниям по безопасности.
![Анализ безопасности Move: Game Changer языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
18 Лайков
Награда
18
3
Поделиться
комментарий
0/400
AirdropBlackHole
· 07-20 03:29
3 года Майнер ищет родственную душу, чтобы поддержать!
Посмотреть ОригиналОтветить0
PumpBeforeRug
· 07-20 03:29
Посмотрите на этот новый любимец move, он также может защитить от уязвимостей.
Посмотреть ОригиналОтветить0
CoinBasedThinking
· 07-20 03:24
Языковая безопасность не имеет смысла, если она не полезна.
Анализ безопасности языка Move: новый защитник смарт-контрактов
Анализ безопасности языка Move: изменяющий правила игры язык смарт-контрактов
Язык Move — это язык смарт-контрактов, который можно компилировать и запускать в блокчейн-среде с реализованной MoveVM. С самого начала своего создания он учитывал множество проблем безопасности блокчейнов и смарт-контрактов, а также заимствовал некоторые элементы дизайна безопасности из языка RUST. Какова же безопасность Move как нового поколения языка смарт-контрактов с основным акцентом на безопасность? Может ли он избежать распространенных угроз безопасности, присущих виртуальным машинам контрактов, таким как EVM и WASM, на уровне языка или связанных механизмов? Существуют ли у него собственные уникальные проблемы безопасности?
В данной статье будет рассмотрена проблема безопасности языка Move с трех аспектов: языковых особенностей, механизма работы и инструментов верификации.
1. Безопасные характеристики языка Move
В отличие от многих существующих языков программирования, язык Move был разработан с целью поддержки написания программ, которые могут безопасно взаимодействовать с ненадежным кодом, при этом поддерживая статическую проверку. Для достижения этой цели Move отказался от нелинейной логики, основанной на гибкости, не поддерживает динамическое распределение и рекурсивные внешние вызовы, вместо этого вводя концепции, такие как обобщения, глобальное хранилище, ресурсы и т.д., для реализации альтернативной модели программирования. Например, Move опустил характеристики динамического распределения и рекурсивных вызовов, которые в других языках смарт-контрактов могут привести к дорогостоящим уязвимостям повторного входа.
Основные функции безопасности Move включают:
Модуль (Module): Каждый модуль Move состоит из ряда определений типов структур и процедур. Модуль может импортировать определения типов, объявленные в других модулях, и вызывать процедуры.
Структуры(: могут быть определены как типы ресурсов, представляющие данные, которые могут храниться в постоянном глобальном хранилище ключ/значение.
процесс ) Функция (: определение логики поведения модуля.
Глобальное хранилище: позволяет программе Move хранить постоянные данные, которые могут быть прочитаны и записаны программным образом только модулем, который их владеет.
Проверка инвариантов: можно определить инварианты для статической проверки, чтобы обеспечить сохранение состояния системы.
Байт-код валидатор: принудительное выполнение системы типов на уровне байт-кода, предотвращающее незаконные операции.
Move обеспечивает безопасность кода на этапе компиляции благодаря этим особенностям. Далее мы проанализируем механизм работы Move и посмотрим, как MoveVM обеспечивает безопасность во время выполнения.
![Анализ безопасности Move: смарт-контракты как изменяющий игру язык])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(
2. Механизм работы Move
Программа Move выполняется в виртуальной машине, и во время выполнения она не может получить доступ к системной памяти, что позволяет Move безопасно работать в ненадежной среде. Программа Move выполняется на стеке, глобальное хранилище делится на память ) кучу ( и глобальные переменные ) стек ( на две части. Память является хранилищем первого уровня и не может хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, но способ индексации отличается от памяти.
Байткод инструкций Move выполняется в стековом интерпретаторе. Стековая виртуальная машина проста в реализации и управлении, требует низких требований к аппаратной среде, что делает её подходящей для блокчейн-сценариев. По сравнению с регистровым интерпретатором, стековый интерпретатор легче контролировать и отслеживать копирование и перемещение переменных.
Во время выполнения программы Move ее состояние представлено четырехмерной кортежем ⟨C, M, G, S⟩, который включает: стек вызовов )C(, память )M(, глобальные переменные )G( и операнды )S(. Стек также поддерживает таблицу функций ) и сам модуль ( для разбора инструкций, содержащих тело функции.
MoveVM отделяет логику хранения данных и вызова стека ) от хранения (, что является крупнейшим отличием от EVM. В MoveVM ресурсы ) под адресом учетной записи пользовательского состояния ( хранятся независимо, и вызовы программ должны соответствовать обязательным правилам, связанным с правами доступа и ресурсами. Хотя это жертвует некоторой гибкостью, это значительно улучшает безопасность и эффективность выполнения ), что способствует достижению высокой степени параллельного выполнения (.
![Анализ безопасности Move: смарт-контракты как фактор изменения игры])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. Доказывающий ход
Move Prover — это инструмент формальной верификации на основе вывода. Он использует формальный язык для описания поведения программы и использует алгоритмы вывода для проверки, соответствует ли программа ожиданиям, помогая разработчикам обеспечить правильность смарт-контрактов и тем самым снизить риски транзакций.
Move Prover использует алгоритм дедуктивной верификации для проверки того, соответствует ли программа ожиданиям. Это означает, что Move Prover может, основываясь на известной информации, делать выводы о поведении программы и гарантировать, что оно соответствует ожидаемому поведению. Это помогает обеспечить корректность программы и уменьшить объем ручного тестирования.
Рабочий процесс Move Prover следующий:
Получите файл Move в качестве входных данных, этот файл должен соответствовать спецификации ввода программы )specification(.
Move Parser извлекает спецификацию из исходного кода.
Move компилятор компилирует исходные файлы в байт-код, совместно с нормативной системой преобразует в модель объекта проверяющего )Prover Object Model(.
Переведите модель в промежуточный язык Boogie.
Система проверки Boogie выполняет "генерацию условий проверки")verification condition generation(.
Передать условия проверки в решатель Z3 ), разработанный Microsoft SMT решатель (.
Z3 проверяет, соответствует ли код программы SMT формулы ) спецификации ( и является ли она несоответствующей.
Если не удовлетворяется, это означает, что спецификация подтверждена; в противном случае создается модель, удовлетворяющая условиям, и она преобразуется обратно в формат Boogie для публикации диагностического отчета.
Восстановите диагностический отчет в виде исходного кода ошибки.
Move использует язык спецификаций Move для описания спецификаций системы. Этот язык является подмножеством Move, поддерживает статическое описание корректности поведения программы, не влияя на производство. Можно независимо писать специальные документированные файлы, разделяя бизнес-код и код формальной проверки.
Move Prover — это полезный инструмент, который помогает разработчикам гарантировать корректность смарт-контрактов. Он использует формальный язык для описания поведения программы и применяет алгоритмы вывода для проверки того, соответствует ли программа ожидаемому. Это помогает снизить риски транзакций и позволяет разработчикам более уверенно развертывать смарт-контракты в производственной среде.
![Анализ безопасности Move: Game Changer языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
4. Резюме
Язык Move обладает выдающейся безопасностью, с тщательным учетом языковых особенностей, выполнения виртуальной машины и уровня инструментов безопасности. Языковые особенности жертвуют частью гибкости, принудительная проверка типов и линейная логика облегчают автоматизацию проверки компиляции и формальную верификацию, а также обеспечивают безопасность и возможность верификации. Дизайн MoveVM разделяет состояние и логику, что более соответствует требованиям безопасного управления активами в блокчейне.
С точки зрения языка, Move может эффективно избежать уязвимостей, распространенных в EVM, таких как повторные вызовы, переполнение, инъекции Call/DeleGateCall и т. д. Однако проблемы с аутентификацией, логикой кода и переполнением структур больших целых чисел все еще требуют внимания разработчиков. Move Prover может не сработать, если общий смысл будет упущен.
Несмотря на то, что язык Move учитывает много аспектов безопасности для программистов, не существует абсолютно безопасного языка, и нет абсолютно безопасных программ. Рекомендуется разработчикам смарт-контрактов Move использовать услуги аудита от сторонних компаний по безопасности и передать написание и проверку части кода спецификации сторонним компаниям по безопасности.
![Анализ безопасности Move: Game Changer языка смарт-контрактов])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(