Анализ безопасности языка Move

Введение

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

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

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

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

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

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

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

3. процесс ( функция ): определение конкретной функции модуля.

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

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

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

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

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

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

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

В отличие от EVM, MoveVM разделяет хранение данных и стек вызовов, что лучше подходит для потребностей управления безопасностью активов в блокчейне. Эта конструкция значительно улучшает безопасность и эффективность выполнения.

3. Переместить Провайдер

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

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

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

1. Принимать файл Move как входные данные
2. Извлечь спецификации и скомпилировать в байт-код
3. Преобразовать в модель объекта валидатора
4. Перевести на промежуточный язык Boogie
5. Генерация условий проверки
6. Использование решателя Z3 для проверки формул SMT
7. Сгенерировать отчет о диагностике и восстановить до исходного уровня ошибки

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

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

4. Итоги

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

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

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