Анализ безопасности языка Move: новатор в области смарт-контрактов

Язык Move является языком смарт-контрактов, который может работать в блокчейн-средах, поддерживающих MoveVM. Его первоначальный замысел учитывает множество вопросов безопасности, связанных с блокчейном и смарт-контрактами, и заимствовал некоторые концепции безопасности из языка Rust. Какова же безопасность Move как языка смарт-контрактов нового поколения, сосредоточенного на безопасности? Может ли он избежать распространенных угроз безопасности, связанных с виртуальными машинами контрактов, такими как EVM и WASM, на уровне языка или через связанные механизмы? Существуют ли уникальные угрозы безопасности у самого Move?

В этой статье будет рассмотрено вопрос безопасности языка Move с трех сторон: языковые особенности, механизмы работы и инструменты верификации.

1. Безопасные характеристики языка Move

В отличие от многих существующих языков программирования, цель дизайна языка Move заключается в поддержке написания программ, которые могут безопасно взаимодействовать с ненадежным кодом, а также в поддержке статической проверки. Move отказывается от нелинейной логики, основанной на гибкости, не поддерживает динамическое распределение и рекурсивные внешние вызовы, а вместо этого вводит такие концепции, как обобщения, глобальное хранилище, ресурсы и т.д., для реализации альтернативных моделей программирования. Например, Move опускает динамическое распределение и рекурсивные вызовы, которые в других языках смарт-контрактов могут легко привести к дорогостоящим уязвимостям повторного входа.

Основные функции безопасности Move включают:

1. Модуль: Каждый модуль Move состоит из ряда определений типов структур и процессов. Модуль может импортировать определения типов, объявленные в других модулях, и вызывать процессы.

2. Структура: может быть определена как тип ресурса, который может храниться в постоянном глобальном хранилище ключей/значений.

3. Процесс: определение функций и логики модуля.

4. Глобальное хранилище: позволяет программам Move хранить постоянные данные, которые могут быть прочитаны и записаны программным способом только модулем, который их владеет.

5. Проверка инвариантов: можно определить статическую проверку инвариантов, чтобы обеспечить сохранение состояния системы.

6. Байт-код валидатор: принудительное выполнение системы типов на уровне байт-кода, предотвращающее незаконные операции.

Благодаря этим функциям безопасности, Move предоставляет более безопасную и надежную среду программирования для смарт-контрактов.

2. Механизм работы Move

Программа Move выполняется в виртуальной машине, и в процессе выполнения не может получить доступ к системной памяти, что позволяет Move безопасно работать в ненадежной среде.

Программа Move выполняется на стеке, глобальное хранилище делится на память (, кучу ) и глобальные переменные ( стек ) на две части. Память является хранилищем первого уровня и не может хранить указатели на ячейки памяти. Глобальные переменные используются для хранения указателей на ячейки памяти, но способ индексации отличается от памяти.

Байткод инструкций Move выполняется в стековом интерпретаторе. По сравнению с регистровым интерпретатором, стековый интерпретатор легче контролировать и отслеживать операции копирования и перемещения между переменными.

Во время выполнения программы Move состояние представлено четверкой ⟨C, M, G, S⟩, которая включает в себя стек вызовов (C), память (M), глобальные переменные (G) и операнды (S). Стек также поддерживает таблицу функций для разрешения инструкций, содержащих тела функций.

MoveVM разделяет логику хранения данных и вызова стека (, что является основным отличием от EVM. Ресурсы ) по адресу учетной записи пользователя ( хранятся независимо, и вызовы программы должны соответствовать обязательным правилам, связанным с разрешениями и ресурсами. Хотя такой дизайн жертвует некоторой гибкостью, он значительно повышает безопасность и эффективность выполнения.

![Анализ безопасности Move: смарт-контракты как изменяющий игру язык])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

3. Доказывающий ход

Move Prover — это инструмент формальной верификации, основанный на дедукции, который использует формальный язык для описания поведения программы и алгоритмы вывода для проверки соответствия программы ожидаемым результатам. Он может помочь разработчикам обеспечить корректность смарт-контрактов и снизить риски сделок.

Move Prover использует алгоритм дедуктивной верификации, чтобы на основе известных данных выводить поведение программы и гарантировать его соответствие ожидаемому поведению. Это помогает обеспечить корректность программы и уменьшить объем ручного тестирования.

Рабочий процесс Move Prover следующий:

1. Прием файла Move в качестве входных данных, который содержит спецификацию входных данных программы.

2. Move Parser извлекает спецификации из исходного кода.

3. Move компилятор компилирует исходный файл в байт-код, совместно с нормативной системой преобразует в модель объекта валидатора.

4. Объектная модель была переведена в промежуточный язык Boogie.

5. Система верификации Boogie выполняет "генерацию условий проверки" для ввода.

6. Передача условий проверки в решатель Z3 ), SMT-решатель, разработанный Microsoft (.

7. Z3 проверяет, является ли SMT формула невыполнимой. Если да, то это означает, что спецификация выполнена; в противном случае генерируется модель, удовлетворяющая условиям.

8. Восстановите отчет о диагностике до уровня исходного кода.

Move использует язык спецификаций Move для описания спецификаций системы, который является подмножеством языка Move и поддерживает статическое описание правильности поведения программы, не влияя на производство. Спецификации могут быть написаны независимо, что облегчает отделение бизнес-кода от кода формальной верификации.

Move Prover — это мощный инструмент, который помогает разработчикам гарантировать правильность смарт-контрактов, снижать риски транзакций и повышать уверенность в развертывании смарт-контрактов в производственной среде.

![Анализ безопасности Move: смарт-контракты как изменяющее игру решение])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

4. Резюме

Язык Move отлично спроектирован с точки зрения безопасности, учитывая все аспекты — от языковых особенностей и выполнения виртуальной машины до уровня инструментов безопасности. Языковые особенности жертвуют частью гибкости, принудительная проверка типов и линейная логика способствуют автоматизации и проверяемости компиляционной проверки и формальной верификации. Дизайн MoveVM разделяет состояние и логику, что лучше соответствует требованиям безопасности управления активами на блокчейне.

С точки зрения языка, Move может эффективно избегать распространенных уязвимостей EVM, таких как повторный вход, переполнение, инъекции Call/DeleGateCall и т.д. Однако вопросы аутентификации, логики кода и переполнения структур больших целых чисел все еще требуют осторожного обращения разработчиков. Хотя Move Prover мощен, он может не сработать в случае общей проектной небрежности.

Несмотря на то, что язык Move предоставляет программистам множество уровней безопасности, не существует полностью безопасного языка и программы. Рекомендуется, чтобы разработчики смарт-контрактов на Move по-прежнему использовали услуги аудита третьих лиц и передавали написание и верификацию части кода спецификации профессиональным командам безопасности для дальнейшего повышения безопасности контракта.

![Анализ безопасности Move: смарт-контракты как фактор изменений в игре])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(