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

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

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

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

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

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

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

• процес)Функція(: визначає ініціалізацію, безпечний процес та небезпечний процес.

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

• Перевірка інваріантів: можна визначити статичну перевірку інваріантів, щоб забезпечити збереження стану системи.

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

![Аналіз безпеки Move: ігрова зміна мови смарт-контрактів])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(

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

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

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

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

![Аналіз безпеки Move: зміна правил гри для мов смарт-контрактів])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

3. Рух Ровер

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

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

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

![Аналіз безпеки Move: зміна правил гри для мов смарт-контрактів])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

4. Підсумок

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

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

![Move безпеки аналіз: ігровий змінник мови смарт-контрактів])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(