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

Вступ

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

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

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

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

Основні характеристики безпеки Move включають:

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

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

3. 过程(function): визначення конкретних функцій модуля.

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

5. Перевірка інваріантів: можна визначити статичні перевірки інваріантів, щоб забезпечити цілісність ресурсів у системі.

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

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

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

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

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

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

3. Рух Ровер

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

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

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

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

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

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

4. Підсумок

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

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

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