Аналіз безпеки Move: революціонер мови смартконтрактів
Мова Move є мовою смартконтрактів, яка може працювати в середовищі блокчейну, що реалізує MoveVM. При її проектуванні було враховано багато питань безпеки, пов'язаних з блокчейном і смартконтрактами, а також враховано безпекове проектування мови RUST. Як нове покоління смартконтрактної мови з акцентом на безпеку, яка її безпечність? Чи може вона на рівні мови або відповідних механізмів уникнути поширених загроз безпеці, властивих віртуальним машинам контрактів, таким як EVM, WASM тощо? Чи має вона власні специфічні проблеми безпеки?
У цій статті буде розглянуто питання безпеки мови Move з трьох аспектів: мовні характеристики, механізми виконання та інструменти перевірки.
1. Безпекові характеристики мови Move
На відміну від багатьох існуючих мов програмування, мова Move була розроблена так, щоб підтримувати як написання програм, що безпечно взаємодіють з ненадійним кодом, так і статичну валідацію. Move має такі безпечні характеристики, оскільки відмовилася від нелінійної логіки, що базується на гнучкості, не підтримує динамічне призначення, а також не підтримує рекурсивні зовнішні виклики, а використовує поняття, такі як генерики, глобальне зберігання, ресурси тощо, щоб реалізувати деякі альтернативні моделі програмування. Наприклад, Move пропускає динамічне планування та рекурсивні виклики, які в інших мовах смартконтрактів призводять до дорогих вразливостей повторного входу.
Основні безпечні характеристики Move включають:
модуль (Module): кожен модуль Move складається з ряду визначень структурних типів і процесів. Модулі можуть імпортувати визначення типів та викликати процеси, оголошені в інших модулях.
结构体(Structs): може бути визначений як тип ресурсу, що означає, що може зберігатися в постійному глобальному сховищі ключ/значення.
процес(Function): визначає бізнес-логіку контракту.
Глобальне зберігання: дозволяє програмі Move зберігати постійні дані, які можуть бути прочитані/записані програмним способом лише модулем, що їх має.
Перевірка невід'ємності: можна визначити статичну перевірку невід'ємності, що відображає збереження ресурсів у системі.
Байт-код валідація: безпечна типізація та лініаризація байт-коду, примусове виконання правил створення, знищення та доступу до ресурсів.
Завдяки цим характеристикам, Move може гарантувати високу безпеку вже на етапі компіляції. Далі ми проаналізуємо механізм роботи Move, щоб побачити, як MoveVM забезпечує безпеку під час виконання.
2. Механізм роботи Move
Програма Move працює у віртуальній машині, і під час виконання не може отримати доступ до системної пам'яті. Це дозволяє Move безпечно працювати в ненадійних середовищах, не підлягаючи руйнуванню або зловживанню.
Програма Move виконується на стеку. Глобальне сховище ділиться на пам'ять ( купу ) та глобальні змінні ( стек ) на дві частини. Пам'ять є однорівневе сховище, не може зберігати вказівники на одиниці пам'яті. Глобальні змінні використовуються для зберігання вказівників на одиниці пам'яті, але спосіб індексації відрізняється від пам'яті.
Байткод Move виконується в стековому інтерпретаторі. Стекова віртуальна машина легко реалізується та контролюється, має низькі вимоги до апаратного середовища, що робить її придатною для сценаріїв блокчейну. Водночас, на відміну від регістрового інтерпретатора, стековий інтерпретатор легше контролює та виявляє копіювання та переміщення між змінними.
Статус виконання програми Move представлений чотиривимірним кортежем ⟨C, M, G, S⟩, що складається з викликової стеку (C), пам'яті (M), глобальних змінних (G) та операндів (S). Стек також підтримує таблицю функцій для розбору інструкцій, що містять тіло функції.
Стек викликів містить всю контекстну інформацію та номери інструкцій, що виконуються процесом. Новий об'єкт стеку викликів створюється під час виконання інструкції Call, зберігаючи параметри виклику, а потім виконуються нові інструкції контракту. При зустрічі інструкції розгалуження здійснюється статичний перехід всередині процесу. Такий дизайн уникає динамічного розподілу, зміцнює незмінність викликів функцій, що, в свою чергу, запобігає можливості повторного входу.
MoveVM відокремлює зберігання даних і виклик стеку процесу ( логіки ), що є найбільшою відмінністю від EVM. У MoveVM ресурси ( під адресою облікового запису стану користувача ) зберігаються окремо, а виклики програм повинні відповідати вимогам безпеки та ресурсів. Цей дизайн, хоча й жертвує певною гнучкістю, проте забезпечує великий приріст у безпеці та ефективності виконання.
3. Рух Ровер
Move Prover є інструментом формальної перевірки на основі міркувань. Він використовує формальну мову для опису поведінки програми та застосовує алгоритми міркувань для перевірки, чи відповідає програма очікуванням, допомагаючи розробникам забезпечити правильність смартконтрактів та зменшити ризики угод.
Move Prover використовує алгоритм дедуктивної верифікації для перевірки того, чи відповідає програма очікуванням. Він може на основі відомої інформації виводити поведінку програми та забезпечувати її відповідність очікуваній поведінці. Це допомагає забезпечити правильність програми та зменшує обсяг ручного тестування.
Робочий процес Move Prover виглядає наступним чином:
Прийміть файл Move як вхідний, у якому потрібно налаштувати специфікації вхідних даних програми.
Move Parser витягує специфікації з вихідного коду.
Move компілятор перетворює вихідний файл у байт-код, разом зі стандартною системою перетворює в об'єктну модель валідатора.
Ця модель була перекладена на проміжну мову Boogie.
Система верифікації Boogie виконує "генерацію умов верифікації" для введення.
Перевірте умови, передавши їх у Z3-солвер для перевірки.
Якщо стандарти встановлені, верифікація пройдена; інакше генерується діагностичний звіт.
Для опису специфікацій системи Move використовує Move Specification Language, який є підмножиною мови Move і вводить підтримку статичного опису коректності поведінки програми. Move Specification Language може бути незалежно представлений як спеціалізований файл специфікацій, що дозволяє відокремити бізнес-код від коду формальної валідації.
Move Prover є дуже корисним інструментом, який може допомогти розробникам забезпечити правильність смартконтрактів. Він використовує формалізовану мову для опису поведінки програми та використовує алгоритми міркування для перевірки того, чи відповідає програма очікуванням. Це допомагає зменшити ризики угод, дозволяючи розробникам більш впевнено розгортати смартконтракти у виробничому середовищі.
4. Підсумок
Мова Move відзначається відмінним дизайном безпеки, з повним врахуванням на рівні мовних особливостей, виконання віртуальної машини та інструментів безпеки. В мовних особливостях жертвується частина гнучкості, примусова перевірка типів та лінійна логіка, що полегшує автоматизацію під час компіляції, формальної верифікації та забезпечує безпеку, що може бути перевірена. Дизайн MoveVM розділяє стан і логіку, що відповідає вимогам безпечного управління активами в блокчейні.
На мовному рівні Move може ефективно уникати поширених вразливостей EVM, таких як повторні виклики, переповнення, ін'єкції Call/DeleGateCall тощо. Але питання автентифікації, логіки коду, переповнення структур великих цілих чисел все ще потребують додаткової уваги розробників. Хоча Move Prover потужний, він може не спрацювати, якщо загальна сутність буде нехтуватися.
Хоча мова Move враховує багато аспектів безпеки для програмістів, але не існує абсолютно безпечних мов і програм. Рекомендується розробникам смартконтрактів на Move використовувати послуги сторонніх компаній з аудиту безпеки та передати написання та перевірку частини коду специфікації сторонній компанії з безпеки для подальшого підвищення безпеки контракту.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
Глибина безпеки мови Move: новий стандарт розробки смартконтрактів
Аналіз безпеки Move: революціонер мови смартконтрактів
Мова Move є мовою смартконтрактів, яка може працювати в середовищі блокчейну, що реалізує MoveVM. При її проектуванні було враховано багато питань безпеки, пов'язаних з блокчейном і смартконтрактами, а також враховано безпекове проектування мови RUST. Як нове покоління смартконтрактної мови з акцентом на безпеку, яка її безпечність? Чи може вона на рівні мови або відповідних механізмів уникнути поширених загроз безпеці, властивих віртуальним машинам контрактів, таким як EVM, WASM тощо? Чи має вона власні специфічні проблеми безпеки?
У цій статті буде розглянуто питання безпеки мови Move з трьох аспектів: мовні характеристики, механізми виконання та інструменти перевірки.
1. Безпекові характеристики мови Move
На відміну від багатьох існуючих мов програмування, мова Move була розроблена так, щоб підтримувати як написання програм, що безпечно взаємодіють з ненадійним кодом, так і статичну валідацію. Move має такі безпечні характеристики, оскільки відмовилася від нелінійної логіки, що базується на гнучкості, не підтримує динамічне призначення, а також не підтримує рекурсивні зовнішні виклики, а використовує поняття, такі як генерики, глобальне зберігання, ресурси тощо, щоб реалізувати деякі альтернативні моделі програмування. Наприклад, Move пропускає динамічне планування та рекурсивні виклики, які в інших мовах смартконтрактів призводять до дорогих вразливостей повторного входу.
Основні безпечні характеристики Move включають:
модуль (Module): кожен модуль Move складається з ряду визначень структурних типів і процесів. Модулі можуть імпортувати визначення типів та викликати процеси, оголошені в інших модулях.
结构体(Structs): може бути визначений як тип ресурсу, що означає, що може зберігатися в постійному глобальному сховищі ключ/значення.
процес(Function): визначає бізнес-логіку контракту.
Глобальне зберігання: дозволяє програмі Move зберігати постійні дані, які можуть бути прочитані/записані програмним способом лише модулем, що їх має.
Перевірка невід'ємності: можна визначити статичну перевірку невід'ємності, що відображає збереження ресурсів у системі.
Байт-код валідація: безпечна типізація та лініаризація байт-коду, примусове виконання правил створення, знищення та доступу до ресурсів.
Завдяки цим характеристикам, Move може гарантувати високу безпеку вже на етапі компіляції. Далі ми проаналізуємо механізм роботи Move, щоб побачити, як MoveVM забезпечує безпеку під час виконання.
2. Механізм роботи Move
Програма Move працює у віртуальній машині, і під час виконання не може отримати доступ до системної пам'яті. Це дозволяє Move безпечно працювати в ненадійних середовищах, не підлягаючи руйнуванню або зловживанню.
Програма Move виконується на стеку. Глобальне сховище ділиться на пам'ять ( купу ) та глобальні змінні ( стек ) на дві частини. Пам'ять є однорівневе сховище, не може зберігати вказівники на одиниці пам'яті. Глобальні змінні використовуються для зберігання вказівників на одиниці пам'яті, але спосіб індексації відрізняється від пам'яті.
Байткод Move виконується в стековому інтерпретаторі. Стекова віртуальна машина легко реалізується та контролюється, має низькі вимоги до апаратного середовища, що робить її придатною для сценаріїв блокчейну. Водночас, на відміну від регістрового інтерпретатора, стековий інтерпретатор легше контролює та виявляє копіювання та переміщення між змінними.
Статус виконання програми Move представлений чотиривимірним кортежем ⟨C, M, G, S⟩, що складається з викликової стеку (C), пам'яті (M), глобальних змінних (G) та операндів (S). Стек також підтримує таблицю функцій для розбору інструкцій, що містять тіло функції.
Стек викликів містить всю контекстну інформацію та номери інструкцій, що виконуються процесом. Новий об'єкт стеку викликів створюється під час виконання інструкції Call, зберігаючи параметри виклику, а потім виконуються нові інструкції контракту. При зустрічі інструкції розгалуження здійснюється статичний перехід всередині процесу. Такий дизайн уникає динамічного розподілу, зміцнює незмінність викликів функцій, що, в свою чергу, запобігає можливості повторного входу.
MoveVM відокремлює зберігання даних і виклик стеку процесу ( логіки ), що є найбільшою відмінністю від EVM. У MoveVM ресурси ( під адресою облікового запису стану користувача ) зберігаються окремо, а виклики програм повинні відповідати вимогам безпеки та ресурсів. Цей дизайн, хоча й жертвує певною гнучкістю, проте забезпечує великий приріст у безпеці та ефективності виконання.
3. Рух Ровер
Move Prover є інструментом формальної перевірки на основі міркувань. Він використовує формальну мову для опису поведінки програми та застосовує алгоритми міркувань для перевірки, чи відповідає програма очікуванням, допомагаючи розробникам забезпечити правильність смартконтрактів та зменшити ризики угод.
Move Prover використовує алгоритм дедуктивної верифікації для перевірки того, чи відповідає програма очікуванням. Він може на основі відомої інформації виводити поведінку програми та забезпечувати її відповідність очікуваній поведінці. Це допомагає забезпечити правильність програми та зменшує обсяг ручного тестування.
Робочий процес Move Prover виглядає наступним чином:
Для опису специфікацій системи Move використовує Move Specification Language, який є підмножиною мови Move і вводить підтримку статичного опису коректності поведінки програми. Move Specification Language може бути незалежно представлений як спеціалізований файл специфікацій, що дозволяє відокремити бізнес-код від коду формальної валідації.
Move Prover є дуже корисним інструментом, який може допомогти розробникам забезпечити правильність смартконтрактів. Він використовує формалізовану мову для опису поведінки програми та використовує алгоритми міркування для перевірки того, чи відповідає програма очікуванням. Це допомагає зменшити ризики угод, дозволяючи розробникам більш впевнено розгортати смартконтракти у виробничому середовищі.
4. Підсумок
Мова Move відзначається відмінним дизайном безпеки, з повним врахуванням на рівні мовних особливостей, виконання віртуальної машини та інструментів безпеки. В мовних особливостях жертвується частина гнучкості, примусова перевірка типів та лінійна логіка, що полегшує автоматизацію під час компіляції, формальної верифікації та забезпечує безпеку, що може бути перевірена. Дизайн MoveVM розділяє стан і логіку, що відповідає вимогам безпечного управління активами в блокчейні.
На мовному рівні Move може ефективно уникати поширених вразливостей EVM, таких як повторні виклики, переповнення, ін'єкції Call/DeleGateCall тощо. Але питання автентифікації, логіки коду, переповнення структур великих цілих чисел все ще потребують додаткової уваги розробників. Хоча Move Prover потужний, він може не спрацювати, якщо загальна сутність буде нехтуватися.
Хоча мова Move враховує багато аспектів безпеки для програмістів, але не існує абсолютно безпечних мов і програм. Рекомендується розробникам смартконтрактів на Move використовувати послуги сторонніх компаній з аудиту безпеки та передати написання та перевірку частини коду специфікації сторонній компанії з безпеки для подальшого підвищення безпеки контракту.