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

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

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

Мова Move має такі особливості безпеки:

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

Валідація байт-коду переважно виконується:

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

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

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

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

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

3. Рух Ровер

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

• Використання алгоритму дедуктивної перевірки для перевірки правильності програми
• Отримати вихідний файл Move та специфікації як вхідні дані
• Перетворити код у проміжну мову Boogie
• Використання Z3 SMT-солвера для перевірки дійсності специфікації
• Підтримка специфікацій мови Move Specification Language
• Можна самостійно писати специфікації, не впливаючи на бізнес-код

Move Prover може допомогти розробникам забезпечити правильність смарт-контрактів, зменшуючи ризики транзакцій.

Підсумок

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