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

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

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

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

Основные компоненты языка Move включают:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Резюме

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

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