Аналіз безпеки Move: революціонер нової генерації смартконтрактів

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

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

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

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

• Модуль (Module): складається з ряду типів структур та визначень процесів
• Структура (Structs): може бути визначена як тип ресурсу, зберігається в постійній глобальній ключ/значення сховищі
• процес (функція ): визначення конкретних функцій смартконтракту

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

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

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

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

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

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

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

3. Рух Ровер

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

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

Move Prover використовує Move Specification Language для опису специфікацій системи, є підмножиною мови Move.

Підсумок

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