Язык Move как язык смарт-контрактов нового поколения изначально учитывал многие проблемы безопасности. В этой статье будет проанализирована безопасность языка Move с трех точек зрения: особенности языка, механизм выполнения и инструменты проверки.
1. Безопасные характеристики языка Move
Язык Move обладает следующими характеристиками безопасности:
Отказавшись от динамического распределения, рекурсивных внешних вызовов и другой нелинейной логики, мы избежали уязвимостей, таких как повторный вход.
Используйте такие концепции, как обобщения, глобальное хранилище, ресурсы и т. д., для реализации безопасных моделей программирования
Модульный дизайн, каждый модуль состоит из типа структуры и определения процесса
Структура может быть определена как тип ресурса, хранящийся в глобальном хранилище ключ-значение.
Глобальное хранилище позволяет сохранять данные, к которым могут обращаться только владельцы модуля.
Проведение статической проверки с использованием инвариантных редукций и проверщика байт-кода
Основное назначение проверщика байт-кода:
Проверка законности структуры
семантическое обнаружение логики процесса
Ошибка проверки при подключении
С помощью этих механизмов язык Move может обеспечить безопасность кода на этапе компиляции.
2. Механизм работы Move
Программа Move работает в виртуальной машине, основные характеристики включают:
Невозможно получить доступ к системной памяти, можно безопасно работать в ненадежной среде
Выполнение в стеке, глобальное хранилище делится на память ( кучу ) и глобальные переменные ( стек )
Выполнение байт-кодовых инструкций с помощью стекового интерпретатора
Ресурсное значение может быть только разрушительно перемещено, не может быть скопировано
Состояние программы состоит из стека вызовов, памяти, глобальных переменных и операций массива.
Стек вызовов содержит контекст выполнения, поддерживает статический переход
Хранение данных и стек вызовов разделены, что повышает безопасность и эффективность выполнения.
3. Переместить Провер
Move Prover — это инструмент формальной верификации, который может выполнять автоматизированный аудит:
Используйте алгоритм дедуктивной проверки для проверки правильности программы
Получите исходный файл Move и спецификации в качестве входных данных
Преобразовать код в промежуточный язык Boogie
Используйте Z3 SMT-решатель для проверки, выполняется ли спецификация.
Поддержка спецификации языка Move Specification Language
Можно самостоятельно писать спецификационные документы, не влияя на бизнес-код
Move Prover может помочь разработчикам гарантировать корректность смарт-контрактов и снизить риски транзакций.
Итог
Язык Move учитывает безопасность во всех аспектах, включая особенности языка, выполнение виртуальной машины и инструменты безопасности. Он эффективно предотвращает общие уязвимости, такие как повторный вход и переполнение, но необходимо обращать внимание на такие вопросы, как аутентификация и логика. Рекомендуется использовать услуги аудита третьих сторон и поручить написание проверочного кода профессионалам.
На этой странице может содержаться сторонний контент, который предоставляется исключительно в информационных целях (не в качестве заявлений/гарантий) и не должен рассматриваться как поддержка взглядов компании Gate или как финансовый или профессиональный совет. Подробности смотрите в разделе «Отказ от ответственности» .
9 Лайков
Награда
9
8
Поделиться
комментарий
0/400
GateUser-e51e87c7
· 07-28 16:10
move немного интересен
Посмотреть ОригиналОтветить0
ForumLurker
· 07-28 02:09
Безопасность не так проста, как говорят!
Посмотреть ОригиналОтветить0
UnluckyValidator
· 07-26 08:52
Эй, у официальных ПИ довольно большой размах.
Посмотреть ОригиналОтветить0
SelfMadeRuggee
· 07-25 19:11
Согласно стандартам, вот и все его особенности.
Посмотреть ОригиналОтветить0
ForkTongue
· 07-25 19:07
Когда можно будет есть move?
Посмотреть ОригиналОтветить0
BlockImposter
· 07-25 19:06
Ай-яй-яй, move гораздо надежнее, чем solidity.
Посмотреть ОригиналОтветить0
MetaverseMigrant
· 07-25 19:03
Аудит тоже не всегда гарантирует безопасность, верно?
Посмотреть ОригиналОтветить0
GasWrangler
· 07-25 19:02
технически переоценённо, если честно. Solidity всё ещё математически превосходит для Газ оптимизации.
Анализ безопасности языка Move: полное объяснение характеристик, механизмов и инструментов проверки
Анализ безопасности языка Move
Язык Move как язык смарт-контрактов нового поколения изначально учитывал многие проблемы безопасности. В этой статье будет проанализирована безопасность языка Move с трех точек зрения: особенности языка, механизм выполнения и инструменты проверки.
1. Безопасные характеристики языка Move
Язык Move обладает следующими характеристиками безопасности:
Основное назначение проверщика байт-кода:
С помощью этих механизмов язык Move может обеспечить безопасность кода на этапе компиляции.
2. Механизм работы Move
Программа Move работает в виртуальной машине, основные характеристики включают:
3. Переместить Провер
Move Prover — это инструмент формальной верификации, который может выполнять автоматизированный аудит:
Move Prover может помочь разработчикам гарантировать корректность смарт-контрактов и снизить риски транзакций.
Итог
Язык Move учитывает безопасность во всех аспектах, включая особенности языка, выполнение виртуальной машины и инструменты безопасности. Он эффективно предотвращает общие уязвимости, такие как повторный вход и переполнение, но необходимо обращать внимание на такие вопросы, как аутентификация и логика. Рекомендуется использовать услуги аудита третьих сторон и поручить написание проверочного кода профессионалам.