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

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

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

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

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

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

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

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

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

Две важные статические проверки языка Move:

1. Проверка инвариантов: определение сохранения состояния системы с помощью языков спецификаций.

2. Байт-код валидатор: обязательное выполнение безопасных типов и линейности, предотвращение незаконных операций.

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

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

Состояние выполнения Move VM состоит из стека вызовов, памяти, глобальных переменных и массива операций. Его характеристики включают:

• Статический переход, избегая динамической диспетчеризации
• Соседние вызовы стека, предотвращение повторного входа
• Разделение хранения данных и стека вызовов

Этот дизайн повышает безопасность и эффективность выполнения.

3. Переместить доказательство

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

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

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

Резюме

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