Аналіз безпеки мови Move

Вступ

Move є мовою смарт-контрактів, розробленою для блокчейн-середовища, яка може працювати на ланцюгах, що підтримують MoveVM. Її дизайн враховує питання безпеки блокчейну та смарт-контрактів і запозичує деякі концепції безпеки з Rust. У цій статті буде проаналізовано безпеку мови Move з трьох аспектів: мовні особливості, механізм виконання та інструменти валідації.

1. Безпекові характеристики Move

Мова Move підвищує безпеку, відмовляючись від певної гнучкості, не підтримує динамічне розподілення та рекурсивні зовнішні виклики, а натомість використовує концепції, такі як узагальнення, глобальне сховище, ресурси тощо, для реалізації альтернативних програмних моделей.

Основні складові частини Move включають:

• Модуль: складається з типу структури та визначення процесу
• Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення
• Процес: визначення логіки контракту

Глобальне сховище Move дозволяє зберігати дані, які можна програмно читати та записувати лише власникам модуля, але їх можна переглядати в публічній книзі обліку.

Move гарантує безпеку компіляції коду за допомогою двох механізмів:

1. Невід'ємна редукція: для статичного контролю, визначає збереження стану системи

2. Біт-код перевірник: забезпечує виконання безпечних типів і лінійності, запобігаючи незаконним операціям

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

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

Стан Move складається з викликів стеку, пам'яті, глобальних змінних та операційного масиву. Під час виконання викликів стек зберігає інформацію про контекст, статичний перехід запобігає динамічній диспетчеризації, тим самим запобігаючи атакам повторного входу.

MoveVM відокремлює зберігання даних та стек викликів, на відміну від EVM. Цей дизайн підвищує безпеку та ефективність виконання.

3. Перемістити доказ

Move Prover є інструментом формальної верифікації, який використовує алгоритми дедуктивної верифікації для перевірки правильності програм. Його робочий процес такий:

1. Отримати вихідні файли Move та специфікації
2. Скомпілювати в байт-код та перевірити об'єктну модель
3. Перетворення на проміжну мову Boogie
4. Генерація умов верифікації
5. Використання Z3-решателя для верифікації
6. Генерація діагностичного звіту

Move Specification Language використовується для опису специфікацій програм, може бути написаний незалежно від бізнес-коду.

4. Підсумок

Move враховує всі аспекти дизайну мови, виконання віртуальної машини та інструментів безпеки. Він жертвує частиною гнучкості, але підвищує безпеку та перевіряємість. Загальні вразливості EVM, такі як повторний вхід, переповнення тощо, можна ефективно уникнути, але все ще потрібно звертати увагу на проблеми авторизації, логіки та переповнення великих цілих чисел.

Хоча Move надає багато рівнів безпеки, все ж рекомендується, щоб розробники користувалися послугами сторонніх аудиторів безпеки та передавали написання та перевірку стандартів професійним компаніям з безпеки.