Язык Move, как новое поколение языков смарт-контрактов, с самого начала проектирования учитывал проблемы безопасности блокчейна и смарт-контрактов. В этой статье будет проанализирована безопасность языка Move с трех сторон: особенностей языка, механизма работы и инструментов верификации.
1. Безопасные характеристики языка Move
В отличие от многих существующих языков программирования, язык Move отказывается от нелинейной логики, основанной на соображениях гибкости, не поддерживает динамическое распределение и рекурсивные внешние вызовы, а вместо этого использует концепции, такие как обобщения, глобальное хранилище, ресурсы и т.д., чтобы реализовать альтернативные модели программирования. Эти конструкции помогают избежать уязвимостей, таких как повторный вход.
Основные функции безопасности Move включают:
Модульность: каждый модуль Move состоит из определения структурного типа и процедур, может импортировать типы из других модулей и вызывать процедуры из других модулей.
Тип ресурса: Структура типа ресурса определяется с помощью синтаксиса has key и может храниться в глобальном хранилище ключ-значение.
Глобальное хранилище: позволяет долговременное хранение данных, которые могут быть прочитаны и записаны программно только обладателями модуля, но хранятся в общедоступном реестре для просмотра.
Контроль доступа: можно ограничить права на вызов процесса с помощью предварительных условий и т.д.
Невариантные условия: можно определить статические проверки невариантов, чтобы гарантировать согласованность состояния системы.
Верификатор байт-кода: принудительное выполнение типовой системы на уровне байт-кода, предотвращающее незаконное создание, распаковку, копирование и уничтожение ресурсов.
Эти особенности обеспечивают высокий уровень безопасности на уровне языка в Move.
2. Механизм работы Move
Программа Move выполняется в виртуальной машине и не может напрямую получить доступ к системной памяти. MoveVM использует стековый интерпретатор для выполнения байт-кодовых инструкций, что облегчает реализацию и контроль.
Основной механизм работы MoveVM включает:
Статусное представление: Используется кортеж ⟨C, M, G, S⟩ для представления состояния программы, включая стек вызовов, память, глобальные переменные и операнды.
Стек вызовов: содержит информацию о контексте выполнения процесса и номер инструкции.
Статический переход: не поддерживает динамическое распределение, зависимости вызова функции без циклов, что предотвращает повторный вход.
Разделение данных и логики: разделение состояния пользователя ( и ресурсов ) от логики программы улучшает безопасность и эффективность выполнения.
Эти механизмы обеспечивают высокую безопасность Move во время выполнения.
3. Движущийся Доказатель
Move Prover — это инструмент формальной верификации, основанный на выводах, который может помочь разработчикам гарантировать правильность смарт-контрактов. Его основные характеристики включают:
Используйте формальный язык для описания поведения программы
Использование алгоритма дедуктивной проверки
Поддержка написания спецификаций с использованием языка спецификаций Move
Может быть написан независимо от бизнес-кода
Генерация отчета об ошибках на уровне исходного кода
Move Prover предоставляет мощные возможности автоматической проверки для смарт-контрактов Move, что помогает повысить безопасность кода.
В целом, язык Move в своем дизайне уделяет большое внимание безопасности и демонстрирует отличные результаты в таких аспектах, как особенности языка, выполнение виртуальной машины и инструменты безопасности. Тем не менее, рекомендуется разработчикам использовать услуги стороннего аудита безопасности и передавать написание и проверку кода спецификаций профессиональным командам безопасности для дальнейшего повышения безопасности контрактов.
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
8 Лайков
Награда
8
4
Репост
Поделиться
комментарий
0/400
PumpStrategist
· 08-03 05:54
Анализ неплохой, посмотрим, поддерживает ли форма Свечи.
Посмотреть ОригиналОтветить0
SchrödingersNode
· 08-02 03:33
Move слишком хорош! Я уже давно на него нацелился!
Посмотреть ОригиналОтветить0
GateUser-e51e87c7
· 07-31 07:25
Этот Move выглядит гораздо стабильнее, чем Solidity...
Анализ безопасности языка Move: полное исследование языковых характеристик, механизма работы и инструментов верификации
Анализ безопасности языка Move
Язык Move, как новое поколение языков смарт-контрактов, с самого начала проектирования учитывал проблемы безопасности блокчейна и смарт-контрактов. В этой статье будет проанализирована безопасность языка Move с трех сторон: особенностей языка, механизма работы и инструментов верификации.
1. Безопасные характеристики языка Move
В отличие от многих существующих языков программирования, язык Move отказывается от нелинейной логики, основанной на соображениях гибкости, не поддерживает динамическое распределение и рекурсивные внешние вызовы, а вместо этого использует концепции, такие как обобщения, глобальное хранилище, ресурсы и т.д., чтобы реализовать альтернативные модели программирования. Эти конструкции помогают избежать уязвимостей, таких как повторный вход.
Основные функции безопасности Move включают:
Модульность: каждый модуль Move состоит из определения структурного типа и процедур, может импортировать типы из других модулей и вызывать процедуры из других модулей.
Тип ресурса: Структура типа ресурса определяется с помощью синтаксиса has key и может храниться в глобальном хранилище ключ-значение.
Глобальное хранилище: позволяет долговременное хранение данных, которые могут быть прочитаны и записаны программно только обладателями модуля, но хранятся в общедоступном реестре для просмотра.
Контроль доступа: можно ограничить права на вызов процесса с помощью предварительных условий и т.д.
Невариантные условия: можно определить статические проверки невариантов, чтобы гарантировать согласованность состояния системы.
Верификатор байт-кода: принудительное выполнение типовой системы на уровне байт-кода, предотвращающее незаконное создание, распаковку, копирование и уничтожение ресурсов.
Эти особенности обеспечивают высокий уровень безопасности на уровне языка в Move.
2. Механизм работы Move
Программа Move выполняется в виртуальной машине и не может напрямую получить доступ к системной памяти. MoveVM использует стековый интерпретатор для выполнения байт-кодовых инструкций, что облегчает реализацию и контроль.
Основной механизм работы MoveVM включает:
Статусное представление: Используется кортеж ⟨C, M, G, S⟩ для представления состояния программы, включая стек вызовов, память, глобальные переменные и операнды.
Стек вызовов: содержит информацию о контексте выполнения процесса и номер инструкции.
Статический переход: не поддерживает динамическое распределение, зависимости вызова функции без циклов, что предотвращает повторный вход.
Разделение данных и логики: разделение состояния пользователя ( и ресурсов ) от логики программы улучшает безопасность и эффективность выполнения.
Эти механизмы обеспечивают высокую безопасность Move во время выполнения.
3. Движущийся Доказатель
Move Prover — это инструмент формальной верификации, основанный на выводах, который может помочь разработчикам гарантировать правильность смарт-контрактов. Его основные характеристики включают:
Move Prover предоставляет мощные возможности автоматической проверки для смарт-контрактов Move, что помогает повысить безопасность кода.
В целом, язык Move в своем дизайне уделяет большое внимание безопасности и демонстрирует отличные результаты в таких аспектах, как особенности языка, выполнение виртуальной машины и инструменты безопасности. Тем не менее, рекомендуется разработчикам использовать услуги стороннего аудита безопасности и передавать написание и проверку кода спецификаций профессиональным командам безопасности для дальнейшего повышения безопасности контрактов.