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

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

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

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

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

• Модульность: упаковывать и управлять кодом и ресурсами с помощью модулей
• Тип ресурса: используется для представления и управления цифровыми активами
• Глобальное хранилище: предоставляет возможности постоянного хранения
• Статическая типизация: проверка типов на этапе компиляции
• Линейная логика: гарантирует уникальность и невозможность копирования ресурсов

Move также предоставляет два важных механизма статической проверки:

1. Невариантное ограничение: используется для объявления и проверки инвариантности состояния системы.
2. Проверка байт-кода: принудительное выполнение типобезопасности и линейной логики на уровне байт-кода

Эти особенности и механизмы могут выявлять и предотвращать многие распространенные проблемы безопасности на этапе компиляции.

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

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

• Глобальное хранилище делится на память ( кучу ) и глобальные переменные ( стек )
• Используйте стек вызовов для управления вызовами функций
• Инструкция выполняется в стековом интерпретаторе
• Ресурсные значения могут быть только перемещены, а не скопированы.
• Статический вызов функции, избегая динамической диспетчеризации

Такой дизайн повышает эффективность выполнения и безопасность, эффективно предотвращая атаки, такие как повторный вход.

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

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

Рабочий процесс Move Prover:

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

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

Резюме

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