Аналіз безпеки мови Move: революціонер мов смартконтрактів
Вступ
Move мова є мовою смартконтрактів, яка може працювати в середовищі блокчейну, що реалізує MoveVM. Її дизайн враховує численні питання безпеки блокчейну та смартконтрактів і черпає натхнення з частини концепцій безпеки мови Rust. Як нове покоління мов смартконтрактів, основною характеристикою яких є безпека, яка безпека Move? Чи може вона уникнути поширених загроз безпеці, властивих контрактним віртуальним машинам, таким як EVM, WASM, на мовному рівні або через відповідні механізми? Чи має Move свої власні специфічні проблеми безпеки?
У цій статті буде розглянуто питання безпеки мови Move з трьох аспектів: мовні особливості, механізм роботи та інструменти верифікації.
1. Безпекові характеристики мови Move
На відміну від багатьох існуючих мов програмування, мова Move була спроектована так, щоб підтримувати безпечну взаємодію з ненадійним кодом, а також підтримувати статичну верифікацію. Move відмовилася від нелінійної логіки, заснованої на гнучкості, не підтримує динамічний диспетчеризацію та рекурсивні зовнішні виклики, натомість використовує такі концепції, як узагальнення, глобальне зберігання, ресурси та інші, щоб реалізувати альтернативні моделі програмування. Наприклад, Move пропускає динамічну диспетчеризацію та рекурсивні виклики, які можуть призвести до вразливостей повторного входу.
Основні функції безпеки Move включають:
Модуль: кожен модуль Move складається з ряду визначень типів структур і процесів. Модулі можуть імпортувати визначення типів і викликати процеси, оголошені в інших модулях.
Структура: може бути визначена як тип ресурсу, що представляє собою дані, які можуть зберігатися в постійному глобальному сховищі ключ/значення.
Процес: визначено ініціалізацію, безпечний процес та небезпечний процес.
Глобальне сховище: дозволяє програмам Move зберігати постійні дані, які можуть бути прочитані та записані програмно лише модулем, що їх володіє.
Перевірка незмінних: підтримка статичної перевірки незмінних, що гарантує цілісність ресурсів у системі.
Віртуальна машина: на рівні байт-коду забезпечує примусове виконання системи типів, запобігаючи незаконним діям зловмисних клієнтських модулів.
За допомогою двох механізмів: перевірки незмінних значень та валідатора байт-коду, Move забезпечує подвійний рівень безпеки коду на етапі компіляції.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині, під час виконання не має доступу до системної пам'яті. Це дозволяє Move безпечно працювати в ненадійних середовищах, не піддаючись знищенню або зловживанню.
Програма Move виконується на стеку, глобальне сховище поділяється на пам'ять ( купу ) і глобальні змінні ( стек ). Пам'ять є першим порядком зберігання, її одиниці не можуть зберігати вказівники на одиниці пам'яті. Глобальні змінні використовуються для зберігання вказівників на одиниці пам'яті, але спосіб індексації відрізняється від пам'яті.
Байтові коди Move виконуються у стековому інтерпретаторі. Стекова віртуальна машина легко реалізується та контролюється, вимоги до апаратного середовища менші, що робить її підходящою для сценаріїв блокчейну. У порівнянні з регістровим інтерпретатором, стековий інтерпретатор легше контролює та виявляє операції копіювання та переміщення між змінними.
Статус виконання програми Move представлений чотиривимірним кортежем ⟨C, M, G, S⟩, який включає стек викликів (C), пам'ять (M), глобальні змінні (G) та операнди (S). Стек також підтримує таблицю функцій для розшифровки інструкцій, що містять тіла функцій.
MoveVM розділяє зберігання даних та логіку виклику стеку (, що є найбільшою відмінністю від EVM. У MoveVM ресурси під адресою облікового запису користувача ) зберігаються окремо, а виклики програм повинні відповідати правилам обов'язкової відповідності правам доступу та ресурсам. Такий дизайн жертвує певною гнучкістю, але значно покращує безпеку та ефективність виконання (, що допомагає досягти високої паралельності виконання ).
3. Рух Ровер
Move Prover є інструментом формальної верифікації, заснованим на міркуванні. Він використовує формальну мову для опису поведінки програми та використовує алгоритми міркування для перевірки, чи відповідає програма очікуванням, допомагаючи розробникам забезпечити правильність смартконтрактів та зменшити ризики транзакцій.
Move Prover використовує алгоритм дедуктивної верифікації для перевірки відповідності програми очікуванням. Це означає, що він може робити висновки про поведінку програми на основі відомої інформації, забезпечуючи відповідність очікуваній поведінці. Це допомагає забезпечити коректність програми та зменшити обсяг ручного тестування.
Робочий процес Move Prover виглядає наступним чином:
Отримати файл Move як вхідні дані, цей файл повинен відповідати вимогам до вводу програми.
Move Parser витягує специфікацію з вихідного коду.
Move компілятор перетворює вихідний файл у байт-код, спільно з системою стандартів перетворюється у модель об'єкта валідатора.
Ця модель була перекладена на проміжну мову Boogie.
Код Boogie передається в систему верифікації Boogie, що генерує умови верифікації.
Передача умов перевірки до Z3-решателя (, SMT-решателя, розробленого Microsoft ).
Z3 перевіряє, чи SMT-формула є незадовільною. Якщо так, це означає, що специфікація є дійсною; в іншому випадку генерує модель, що задовольняє умови.
Відновити звіт про діагностику до рівня коду помилки.
Move використовує Move Specification Language для опису специфікацій системи. Це підмножина Move мови, яка підтримує статичний опис коректності поведінки програми, не впливаючи на виробництво. Може бути незалежно написано у вигляді спеціалізованих документів специфікацій, розділяючи бізнес-код і код формальної верифікації.
Move Prover є корисним інструментом, який допомагає розробникам забезпечити правильність смартконтрактів. Він використовує формалізовану мову для опису поведінки програми та застосовує алгоритми міркування для перевірки, чи відповідає програма очікуванням, що допомагає зменшити ризики транзакцій, дозволяючи розробникам більш впевнено розгортати смартконтракти у виробничому середовищі.
4. Підсумок
Мова Move відзначається відмінним дизайном безпеки, забезпечуючи всебічний підхід до мовних особливостей, виконання віртуальної машини та рівня безпекових інструментів. Особливості мови жертвують частиною гнучкості, примусова перевірка типів та лінійна логіка полегшують автоматизацію компіляційних перевірок і формальну верифікацію, а також забезпечують безпечною верифікацією. Дизайн MoveVM розділяє стан і логіку, що більше відповідає вимогам безпечного управління активами в блокчейні.
На рівні мови, Move може ефективно уникати поширених вразливостей EVM, таких як повторні виклики, переповнення, ін'єкції Call/DeleGateCall тощо. Але питання авторизації, логіки коду, переповнення структур великих цілих чисел все ще потребують уваги розробників. Move Prover може не спрацювати, якщо загальний зміст буде проігноровано.
Хоча мова Move враховує багато аспектів безпеки для програмістів, не існує абсолютно безпечних мов і програм. Рекомендується розробникам смартконтрактів на Move використовувати послуги аудиту від третіх сторін і доручити написання та перевірку частини коду специфікацій стороннім компаніям з безпеки.
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
Аналіз безпеки мови Move: нова парадигма смартконтрактів
Аналіз безпеки мови Move: революціонер мов смартконтрактів
Вступ
Move мова є мовою смартконтрактів, яка може працювати в середовищі блокчейну, що реалізує MoveVM. Її дизайн враховує численні питання безпеки блокчейну та смартконтрактів і черпає натхнення з частини концепцій безпеки мови Rust. Як нове покоління мов смартконтрактів, основною характеристикою яких є безпека, яка безпека Move? Чи може вона уникнути поширених загроз безпеці, властивих контрактним віртуальним машинам, таким як EVM, WASM, на мовному рівні або через відповідні механізми? Чи має Move свої власні специфічні проблеми безпеки?
У цій статті буде розглянуто питання безпеки мови Move з трьох аспектів: мовні особливості, механізм роботи та інструменти верифікації.
1. Безпекові характеристики мови Move
На відміну від багатьох існуючих мов програмування, мова Move була спроектована так, щоб підтримувати безпечну взаємодію з ненадійним кодом, а також підтримувати статичну верифікацію. Move відмовилася від нелінійної логіки, заснованої на гнучкості, не підтримує динамічний диспетчеризацію та рекурсивні зовнішні виклики, натомість використовує такі концепції, як узагальнення, глобальне зберігання, ресурси та інші, щоб реалізувати альтернативні моделі програмування. Наприклад, Move пропускає динамічну диспетчеризацію та рекурсивні виклики, які можуть призвести до вразливостей повторного входу.
Основні функції безпеки Move включають:
Модуль: кожен модуль Move складається з ряду визначень типів структур і процесів. Модулі можуть імпортувати визначення типів і викликати процеси, оголошені в інших модулях.
Структура: може бути визначена як тип ресурсу, що представляє собою дані, які можуть зберігатися в постійному глобальному сховищі ключ/значення.
Процес: визначено ініціалізацію, безпечний процес та небезпечний процес.
Глобальне сховище: дозволяє програмам Move зберігати постійні дані, які можуть бути прочитані та записані програмно лише модулем, що їх володіє.
Перевірка незмінних: підтримка статичної перевірки незмінних, що гарантує цілісність ресурсів у системі.
Віртуальна машина: на рівні байт-коду забезпечує примусове виконання системи типів, запобігаючи незаконним діям зловмисних клієнтських модулів.
За допомогою двох механізмів: перевірки незмінних значень та валідатора байт-коду, Move забезпечує подвійний рівень безпеки коду на етапі компіляції.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині, під час виконання не має доступу до системної пам'яті. Це дозволяє Move безпечно працювати в ненадійних середовищах, не піддаючись знищенню або зловживанню.
Програма Move виконується на стеку, глобальне сховище поділяється на пам'ять ( купу ) і глобальні змінні ( стек ). Пам'ять є першим порядком зберігання, її одиниці не можуть зберігати вказівники на одиниці пам'яті. Глобальні змінні використовуються для зберігання вказівників на одиниці пам'яті, але спосіб індексації відрізняється від пам'яті.
Байтові коди Move виконуються у стековому інтерпретаторі. Стекова віртуальна машина легко реалізується та контролюється, вимоги до апаратного середовища менші, що робить її підходящою для сценаріїв блокчейну. У порівнянні з регістровим інтерпретатором, стековий інтерпретатор легше контролює та виявляє операції копіювання та переміщення між змінними.
Статус виконання програми Move представлений чотиривимірним кортежем ⟨C, M, G, S⟩, який включає стек викликів (C), пам'ять (M), глобальні змінні (G) та операнди (S). Стек також підтримує таблицю функцій для розшифровки інструкцій, що містять тіла функцій.
MoveVM розділяє зберігання даних та логіку виклику стеку (, що є найбільшою відмінністю від EVM. У MoveVM ресурси під адресою облікового запису користувача ) зберігаються окремо, а виклики програм повинні відповідати правилам обов'язкової відповідності правам доступу та ресурсам. Такий дизайн жертвує певною гнучкістю, але значно покращує безпеку та ефективність виконання (, що допомагає досягти високої паралельності виконання ).
3. Рух Ровер
Move Prover є інструментом формальної верифікації, заснованим на міркуванні. Він використовує формальну мову для опису поведінки програми та використовує алгоритми міркування для перевірки, чи відповідає програма очікуванням, допомагаючи розробникам забезпечити правильність смартконтрактів та зменшити ризики транзакцій.
Move Prover використовує алгоритм дедуктивної верифікації для перевірки відповідності програми очікуванням. Це означає, що він може робити висновки про поведінку програми на основі відомої інформації, забезпечуючи відповідність очікуваній поведінці. Це допомагає забезпечити коректність програми та зменшити обсяг ручного тестування.
Робочий процес Move Prover виглядає наступним чином:
Move використовує Move Specification Language для опису специфікацій системи. Це підмножина Move мови, яка підтримує статичний опис коректності поведінки програми, не впливаючи на виробництво. Може бути незалежно написано у вигляді спеціалізованих документів специфікацій, розділяючи бізнес-код і код формальної верифікації.
Move Prover є корисним інструментом, який допомагає розробникам забезпечити правильність смартконтрактів. Він використовує формалізовану мову для опису поведінки програми та застосовує алгоритми міркування для перевірки, чи відповідає програма очікуванням, що допомагає зменшити ризики транзакцій, дозволяючи розробникам більш впевнено розгортати смартконтракти у виробничому середовищі.
4. Підсумок
Мова Move відзначається відмінним дизайном безпеки, забезпечуючи всебічний підхід до мовних особливостей, виконання віртуальної машини та рівня безпекових інструментів. Особливості мови жертвують частиною гнучкості, примусова перевірка типів та лінійна логіка полегшують автоматизацію компіляційних перевірок і формальну верифікацію, а також забезпечують безпечною верифікацією. Дизайн MoveVM розділяє стан і логіку, що більше відповідає вимогам безпечного управління активами в блокчейні.
На рівні мови, Move може ефективно уникати поширених вразливостей EVM, таких як повторні виклики, переповнення, ін'єкції Call/DeleGateCall тощо. Але питання авторизації, логіки коду, переповнення структур великих цілих чисел все ще потребують уваги розробників. Move Prover може не спрацювати, якщо загальний зміст буде проігноровано.
Хоча мова Move враховує багато аспектів безпеки для програмістів, не існує абсолютно безпечних мов і програм. Рекомендується розробникам смартконтрактів на Move використовувати послуги аудиту від третіх сторін і доручити написання та перевірку частини коду специфікацій стороннім компаніям з безпеки.