Аналіз безпеки мови Move: рушій змін у сфері смартконтрактів

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

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

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

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

Валідатор байт-коду проводить такі перевірки:

1. Перевірка законності структури
2. Семантичне виявлення логіки процесу
3. Перевірка помилок при з'єднанні

Завдяки цим механізмам, Move вже на стадії компіляції може забезпечити високу безпеку коду.

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

Програма Move працює у віртуальній машині і має такі характеристики безпеки:

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

Цей дизайн має значні покращення в безпеці та ефективності виконання.

3. Рух Ровер

Move Prover є формальним інструментом верифікації на основі міркувань, який може:

• Використання формальної мови для опису поведінки програми
• перевірка правильності програми за допомогою алгоритмів висновку
• Використання алгоритму дедуктивної верифікації
• Використовуйте мову специфікації Move для опису перевірки
• Генерація звіту про перевірку, вказуючи на потенційні проблеми

Move Prover є дуже корисним інструментом автоматизованого аудиту, який може допомогти розробникам підвищити безпеку смартконтрактів.

Підсумок

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

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

! Пояснення безпеки переміщення: зміна правил гри для мови смарт-контрактів