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

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

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

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

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

Ось деякі ключові функції безпеки мови Move:

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

2. Тип ресурсу: структура, визначена за допомогою синтаксису has key, може зберігатися в постійному глобальному сховищі пар ключ-значення.

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

4. Статична типізація: Move має потужну статичну типізацію, яка може вловлювати багато помилок на етапі компіляції.

5. Лінійні типи: типи ресурсів за замовчуванням є лінійними, щоб запобігти їх копіюванню або неявному знищенню.

6. Інваріантні скорочення: можна визначити інваріанти збереження стану для формалізації перевірки.

7. Віртуальний байт-код: примусове виконання типізованої системи на рівні байт-коду, щоб запобігти зловмисним діям.

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

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

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

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

MoveVM відокремлює зберігання даних і стек викликів, що є його найбільшою відмінністю від EVM. Ресурси під обліковим записом користувача ( за адресою ) зберігаються незалежно, виклики програм повинні відповідати обов'язковим правилам, пов'язаним з правами доступу та ресурсами. Такий дизайн жертвує певною гнучкістю, але значно підвищує безпеку та ефективність виконання.

3. Рух Ровер

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

Робочий процес Move Prover виглядає так:

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

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

4. Підсумок

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

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