Язык Move как язык смарт-контрактов нового поколения изначально учитывал вопросы безопасности блокчейна и смарт-контрактов. В этой статье будет рассмотрена безопасность языка Move с трех аспектов: особенности языка, механизм выполнения и инструменты верификации.
1. Безопасные особенности языка Move
Язык Move отказался от нелинейной логики, основанной на гибкости, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы, вместо этого использует концепции обобщений, глобального хранилища, ресурсов и т.д. для реализации альтернативных моделей программирования. Эти разработки помогают избежать уязвимостей безопасности, таких как повторный вход.
Основные компоненты языка Move включают:
Модуль: состоит из определения типов структуры и процессов, может импортировать определения типов других модулей и вызывать процессы других модулей.
Структура: может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Процесс: определение функций модуля, может включать инициализацию, безопасные и небезопасные процессы.
Глобальный механизм хранения языка Move позволяет модулям хранить постоянные данные и иметь исключительные права на чтение и запись для объявленных типов ресурсов. Этот механизм помогает обеспечить соблюдение ограничений безопасности.
Две важные статические проверки языка Move:
Проверка инвариантов: определение сохранения состояния системы с помощью языков спецификаций.
Байт-код валидатор: обязательное выполнение безопасных типов и линейности, предотвращение незаконных операций.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может напрямую обращаться к системной памяти. Выполнение программы основано на стеке, глобальное хранилище делится на память (, кучу ) и глобальные переменные (, стек ).
Состояние выполнения Move VM состоит из стека вызовов, памяти, глобальных переменных и массива операций. Его характеристики включают:
Этот дизайн повышает безопасность и эффективность выполнения.
3. Переместить доказательство
Move Prover — это инструмент формальной верификации, использующий алгоритмы дедуктивной верификации для проверки соответствия программы ожидаемым требованиям. Его рабочий процесс:
Получение исходных файлов и стандартов Move
Компиляция в байт-код и модель объекта валидатора
Преобразовать в промежуточный язык Boogie
Генерация условий проверки
Используйте решатель Z3 для верификации
Генерация диагностического отчета
Язык спецификации Move используется для описания стандартов поведения программы и может быть написан независимо от бизнес-кода.
Резюме
Язык Move учитывает все аспекты языковых особенностей, выполнения виртуальной машины и инструментов безопасности, что позволяет эффективно избегать многих распространенных уязвимостей. Тем не менее, рекомендуется использовать услуги стороннего аудита безопасности и поручить компании по безопасности разработку и проверку нормативного кода.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
17 Лайков
Награда
17
8
Поделиться
комментарий
0/400
HashBard
· 7ч назад
всё равно есть уязвимости... театрализованная безопасность в лучшем её проявлении, честно говоря
Посмотреть ОригиналОтветить0
AirdropHarvester
· 18ч назад
Партия крупного рогатого скота: безопасность превыше всего!
Посмотреть ОригиналОтветить0
CryptoNomics
· 18ч назад
*вздох* еще один L1, пытающийся пройти формальную верификацию... статистически незначительно без надлежащего анализа равновесия Нэша, на мой взгляд
Посмотреть ОригиналОтветить0
ForumMiningMaster
· 18ч назад
Мне нравится такой надежный актив
Посмотреть ОригиналОтветить0
DegenGambler
· 18ч назад
Статическая проверка и всё?
Посмотреть ОригиналОтветить0
ponzi_poet
· 18ч назад
Надо смотреть на конкретные результаты, статические остаются статическими.
Посмотреть ОригиналОтветить0
fork_in_the_road
· 18ч назад
Еще пишете на solidity? Быстро войдите в позицию Move
Полный анализ безопасности языка Move: от характеристик до инструментов валидации
Анализ безопасности языка Move
Язык Move как язык смарт-контрактов нового поколения изначально учитывал вопросы безопасности блокчейна и смарт-контрактов. В этой статье будет рассмотрена безопасность языка Move с трех аспектов: особенности языка, механизм выполнения и инструменты верификации.
1. Безопасные особенности языка Move
Язык Move отказался от нелинейной логики, основанной на гибкости, не поддерживает динамическую диспетчеризацию и рекурсивные внешние вызовы, вместо этого использует концепции обобщений, глобального хранилища, ресурсов и т.д. для реализации альтернативных моделей программирования. Эти разработки помогают избежать уязвимостей безопасности, таких как повторный вход.
Основные компоненты языка Move включают:
Модуль: состоит из определения типов структуры и процессов, может импортировать определения типов других модулей и вызывать процессы других модулей.
Структура: может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Процесс: определение функций модуля, может включать инициализацию, безопасные и небезопасные процессы.
Глобальный механизм хранения языка Move позволяет модулям хранить постоянные данные и иметь исключительные права на чтение и запись для объявленных типов ресурсов. Этот механизм помогает обеспечить соблюдение ограничений безопасности.
Две важные статические проверки языка Move:
Проверка инвариантов: определение сохранения состояния системы с помощью языков спецификаций.
Байт-код валидатор: обязательное выполнение безопасных типов и линейности, предотвращение незаконных операций.
2. Механизм работы Move
Программа Move работает в виртуальной машине и не может напрямую обращаться к системной памяти. Выполнение программы основано на стеке, глобальное хранилище делится на память (, кучу ) и глобальные переменные (, стек ).
Состояние выполнения Move VM состоит из стека вызовов, памяти, глобальных переменных и массива операций. Его характеристики включают:
Этот дизайн повышает безопасность и эффективность выполнения.
3. Переместить доказательство
Move Prover — это инструмент формальной верификации, использующий алгоритмы дедуктивной верификации для проверки соответствия программы ожидаемым требованиям. Его рабочий процесс:
Язык спецификации Move используется для описания стандартов поведения программы и может быть написан независимо от бизнес-кода.
Резюме
Язык Move учитывает все аспекты языковых особенностей, выполнения виртуальной машины и инструментов безопасности, что позволяет эффективно избегать многих распространенных уязвимостей. Тем не менее, рекомендуется использовать услуги стороннего аудита безопасности и поручить компании по безопасности разработку и проверку нормативного кода.