Мова Move, як нове покоління мови смарт-контрактів, при її створенні враховувала питання безпеки блокчейну та смарт-контрактів. У цій статті ми розглянемо безпеку мови Move з трьох аспектів: характеристик мови, механізму виконання та інструментів верифікації.
1. Безпекові характеристики мови Move
Мова Move має кілька основних характеристик безпеки:
Відмовилися від нелінійної логіки, не підтримують динамічну диспетчеризацію та рекурсивні зовнішні виклики
Використання концепцій генералізації, глобального зберігання, ресурсів тощо для реалізації альтернативних моделей програмування
Модульний дизайн, кожен модуль складається з типу структури та визначення процесу
Типи ресурсів та глобальний механізм зберігання забезпечують безпеку зберігання та ресурсів
Реалізація неперервних умов і перевірка байт-коду для забезпечення безпеки під час компіляції
Валідатор байт-коду проводить три основні перевірки:
Перевірка законності структури
Семантичне виявлення логіки процесу
Виявлення помилок при підключенні
Ці механізми забезпечують високу безпеку Move під час компіляції.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині і не може безпосередньо отримати доступ до системної пам'яті. Її стан складається з викликів стеку, пам'яті, глобальних змінних та операційних масивів.
На відміну від EVM, MoveVM відокремлює зберігання даних і стек викликів. Користувацький стан зберігається незалежно, а виклики програм повинні відповідати правилам доступу та ресурсів. Цей дизайн підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної верифікації, який використовує алгоритми дедуктивної верифікації для перевірки того, чи відповідає програма очікуванням. Процес верифікації виглядає наступним чином:
Отримати вихідні файли Move та специфікацію
Компіляція в байт-код та модель об'єкта валідатора
Перекласти на проміжну мову Boogie
Генерація умов верифікації
Використання Z3 рішувача для перевірки
Генерація діагностичного звіту
Move Specification Language використовується для опису систем специфікацій, є підмножиною мови Move.
Загалом, Move Prover є потужним інструментом безпеки, але не може повністю замінити ручний аудит. Рекомендується, щоб розробники все ще використовували послуги стороннього безпеки аудиту і передавали частину специфікації безпековій компанії.
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
Аналіз безпеки мови Move: характеристики мови, механізм виконання та Формальна верифікація
Аналіз безпеки мови Move
Мова Move, як нове покоління мови смарт-контрактів, при її створенні враховувала питання безпеки блокчейну та смарт-контрактів. У цій статті ми розглянемо безпеку мови Move з трьох аспектів: характеристик мови, механізму виконання та інструментів верифікації.
1. Безпекові характеристики мови Move
Мова Move має кілька основних характеристик безпеки:
Валідатор байт-коду проводить три основні перевірки:
Ці механізми забезпечують високу безпеку Move під час компіляції.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині і не може безпосередньо отримати доступ до системної пам'яті. Її стан складається з викликів стеку, пам'яті, глобальних змінних та операційних масивів.
На відміну від EVM, MoveVM відокремлює зберігання даних і стек викликів. Користувацький стан зберігається незалежно, а виклики програм повинні відповідати правилам доступу та ресурсів. Цей дизайн підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної верифікації, який використовує алгоритми дедуктивної верифікації для перевірки того, чи відповідає програма очікуванням. Процес верифікації виглядає наступним чином:
Move Specification Language використовується для опису систем специфікацій, є підмножиною мови Move.
Загалом, Move Prover є потужним інструментом безпеки, але не може повністю замінити ручний аудит. Рекомендується, щоб розробники все ще використовували послуги стороннього безпеки аудиту і передавали частину специфікації безпековій компанії.