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

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

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

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

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

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

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

• Процесс ( Функция ): определяет инициализацию, безопасный процесс и небезопасный процесс.

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

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

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

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

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

Байткод инструкции Move выполняется в стековом интерпретаторе. Состояние программы состоит из стека вызовов, памяти, глобальных переменных и операционных массивов. Значения ресурсов могут быть перемещены только разрушительно, некоторые значения (, такие как целые числа ), могут быть скопированы.

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

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

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

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

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

4. Резюме

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

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