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

Мова Move, як нове покоління мов програмування для смарт-контрактів, з самого початку проектувалася з урахуванням безпеки блокчейну та смарт-контрактів. У цій статті буде розглянуто безпеку мови Move з трьох аспектів: характеристик мови, механізмів виконання та інструментів верифікації.

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

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

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

• Модуль: складається з визначень типів структури та процесу, може імпортувати визначення типів з інших модулів і викликати процеси з інших модулів.

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

• Процес: визначення функцій модуля, які можуть включати ініціалізацію, безпечні та небезпечні процеси.

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

Дві важливі статичні перевірки мови Move:

1. Перевірка незмінності: визначення збереження стану системи через мову специфікацій.

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

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

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

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

• Статичний перехід, уникайте динамічної диспетчеризації
• Сусідність стеку викликів, щоб уникнути повторних входів
• Розділення зберігання та виклику даних

Цей дизайн підвищує безпеку та ефективність виконання.

3. Рух Ровер

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

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

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

Підсумок

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