Аналіз безпеки мови Move: зміна правил гри для мов смартконтрактів
Мова Move є мовою смартконтрактів, яка може компілюватися та виконуватися в середовищі блокчейну, що реалізує MoveVM. Вона була створена з урахуванням багатьох проблем безпеки блокчейну та смартконтрактів, а також запозичила деякі елементи безпеки з мови RUST. Як нове покоління мов смартконтрактів, що характеризуються безпекою, якою є безпека Move? Чи може вона уникати поширених загроз безпеці, притаманних віртуальним машинам контрактів, таким як EVM, WASM тощо, на мовному рівні або за допомогою відповідних механізмів? Чи існують у неї власні специфічні загрози безпеці?
Ця стаття розгляне проблеми безпеки мови Move з трьох аспектів: мовні особливості, механізм роботи та інструменти верифікації.
1. Безпекові характеристики мови Move
На відміну від багатьох існуючих мов програмування, метою дизайну мови Move є підтримка написання програм, які можуть безпечно взаємодіяти з ненадійним кодом, одночасно підтримуючи статичну валідацію. Для досягнення цієї мети Move відмовилася від нелінійної логіки, що базується на гнучкості, не підтримує динамічну диспетчеризацію та рекурсивні зовнішні виклики, натомість вводить концепції, такі як загальні параметри, глобальне сховище, ресурси та інші, щоб реалізувати альтернативні моделі програмування. Наприклад, Move пропускає динамічну диспетчеризацію та рекурсивні виклики, які в інших мовах смартконтрактів можуть призвести до дорогих вразливостей повторного входу.
Основні функції безпеки Move включають:
модуль (Module): кожен модуль Move складається з ряду визначень типів структур і процедур. Модулі можуть імпортувати визначення типів, оголошених в інших модулях, та викликати процедури.
结构体(Structs): може бути визначено як тип ресурсу, що представляє собою те, що можна зберігати у постійних глобальних ключ/значеннях.
процес(Функція): визначає логіку поведінки модуля.
Глобальне зберігання: дозволяє програмам Move зберігати постійні дані, які можуть бути прочитані та записані програмно лише модулем, що їх має.
Перевірка інваріантів: можна визначити статичні перевірки інваріантів, щоб забезпечити збереження стану системи.
Валідація байт-коду: примусове виконання системи типів на рівні байт-коду, запобігання незаконним операціям.
Move забезпечує безпеку коду під час компіляції завдяки цим характеристикам. Далі ми проаналізуємо механізм роботи Move, щоб побачити, як MoveVM гарантує безпеку під час виконання.
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 Prover такий:
Отримати файл Move як вхідні дані, цей файл повинен встановлювати специфікацію вхідних даних програми (specification).
Move Parser витягує специфікацію з вихідного коду.
Move компілятор перетворює вихідний файл на байт-код, спільно з нормативною системою трансформує в модель об'єкта перевірника (Prover Object Model).
Перекладіть модель на проміжну мову Boogie.
Система верифікації Boogie виконує "генерацію умов верифікації"(verification condition generation).
Передайте умови перевірки в Z3-решатель (, розроблений Microsoft SMT-решателем ).
Z3 перевіряє, чи відповідає програмний код SMT формули ( специфікації ), чи є вона незадовольняльною.
Якщо не можливо задовольнити, це означає, що специфікація є дійсною; в іншому випадку генерується модель, що відповідає умовам, і вона конвертується назад у формат Boogie для публікації діагностичного звіту.
Відновіть діагностичний звіт до рівня коду.
Move використовує Move Specification Language для опису специфікацій системи. Ця мова є підмножиною Move, підтримує статичний опис правильної поведінки програми, не впливаючи на продукцію. Можна незалежно написати спеціалізовані документовані файли, розділивши бізнес-код та код формальної перевірки.
Move Prover є корисним інструментом, що допомагає розробникам забезпечити правильність смартконтрактів. Він використовує формалізовану мову для опису поведінки програми і використовує алгоритми міркування для перевірки відповідності програми очікуванням. Це допомагає зменшити ризики угод, надаючи розробникам більше впевненості у впровадженні смартконтрактів у виробниче середовище.
4. Підсумок
Мова Move має відмінний дизайн безпеки, з усебічним врахуванням мовних характеристик, виконання віртуальної машини та рівня безпеки інструментів. Мовні характеристики жертвують частиною гнучкості, примусова перевірка типів і лінійна логіка полегшують автоматизацію компіляційної перевірки та формальної верифікації, а також безпечну верифікацію. Дизайн MoveVM відокремлює стан від логіки, що краще відповідає вимогам безпечного управління активами в блокчейні.
На мовному рівні Move може ефективно уникати вразливостей, що часто зустрічаються в EVM, таких як повторний вхід, переповнення, ін'єкція Call/DeleGateCall тощо. Але проблеми аутентифікації, логіки коду, переповнення структур великих цілих чисел все ще потребують уваги розробників. Move Prover може не спрацювати, якщо загальна ідея буде проігнорована.
Хоча мова Move враховує багато аспектів безпеки для програмістів, не існує абсолютно безпечних мов, а також не існує абсолютно безпечних програм. Рекомендується, щоб розробники смартконтрактів Move використовували послуги аудиту від третіх сторін, а також передали написання та перевірку частини коду specification стороннім безпековим компаніям.
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
16 лайків
Нагородити
16
3
Поділіться
Прокоментувати
0/400
AirdropBlackHole
· 07-20 03:29
3 роки Майнер шукає того, хто його підтримає!
Переглянути оригіналвідповісти на0
PumpBeforeRug
· 07-20 03:29
Подивіться на цю новинку move, яка також може захистити від вразливостей.
Аналіз безпеки мови Move: новий охоронець безпеки смартконтрактів
Аналіз безпеки мови Move: зміна правил гри для мов смартконтрактів
Мова Move є мовою смартконтрактів, яка може компілюватися та виконуватися в середовищі блокчейну, що реалізує MoveVM. Вона була створена з урахуванням багатьох проблем безпеки блокчейну та смартконтрактів, а також запозичила деякі елементи безпеки з мови RUST. Як нове покоління мов смартконтрактів, що характеризуються безпекою, якою є безпека Move? Чи може вона уникати поширених загроз безпеці, притаманних віртуальним машинам контрактів, таким як EVM, WASM тощо, на мовному рівні або за допомогою відповідних механізмів? Чи існують у неї власні специфічні загрози безпеці?
Ця стаття розгляне проблеми безпеки мови Move з трьох аспектів: мовні особливості, механізм роботи та інструменти верифікації.
1. Безпекові характеристики мови Move
На відміну від багатьох існуючих мов програмування, метою дизайну мови Move є підтримка написання програм, які можуть безпечно взаємодіяти з ненадійним кодом, одночасно підтримуючи статичну валідацію. Для досягнення цієї мети Move відмовилася від нелінійної логіки, що базується на гнучкості, не підтримує динамічну диспетчеризацію та рекурсивні зовнішні виклики, натомість вводить концепції, такі як загальні параметри, глобальне сховище, ресурси та інші, щоб реалізувати альтернативні моделі програмування. Наприклад, Move пропускає динамічну диспетчеризацію та рекурсивні виклики, які в інших мовах смартконтрактів можуть призвести до дорогих вразливостей повторного входу.
Основні функції безпеки Move включають:
модуль (Module): кожен модуль Move складається з ряду визначень типів структур і процедур. Модулі можуть імпортувати визначення типів, оголошених в інших модулях, та викликати процедури.
结构体(Structs): може бути визначено як тип ресурсу, що представляє собою те, що можна зберігати у постійних глобальних ключ/значеннях.
процес(Функція): визначає логіку поведінки модуля.
Глобальне зберігання: дозволяє програмам Move зберігати постійні дані, які можуть бути прочитані та записані програмно лише модулем, що їх має.
Перевірка інваріантів: можна визначити статичні перевірки інваріантів, щоб забезпечити збереження стану системи.
Валідація байт-коду: примусове виконання системи типів на рівні байт-коду, запобігання незаконним операціям.
Move забезпечує безпеку коду під час компіляції завдяки цим характеристикам. Далі ми проаналізуємо механізм роботи Move, щоб побачити, як MoveVM гарантує безпеку під час виконання.
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 Prover такий:
Отримати файл Move як вхідні дані, цей файл повинен встановлювати специфікацію вхідних даних програми (specification).
Move Parser витягує специфікацію з вихідного коду.
Move компілятор перетворює вихідний файл на байт-код, спільно з нормативною системою трансформує в модель об'єкта перевірника (Prover Object Model).
Перекладіть модель на проміжну мову Boogie.
Система верифікації Boogie виконує "генерацію умов верифікації"(verification condition generation).
Передайте умови перевірки в Z3-решатель (, розроблений Microsoft SMT-решателем ).
Z3 перевіряє, чи відповідає програмний код SMT формули ( специфікації ), чи є вона незадовольняльною.
Якщо не можливо задовольнити, це означає, що специфікація є дійсною; в іншому випадку генерується модель, що відповідає умовам, і вона конвертується назад у формат Boogie для публікації діагностичного звіту.
Відновіть діагностичний звіт до рівня коду.
Move використовує Move Specification Language для опису специфікацій системи. Ця мова є підмножиною Move, підтримує статичний опис правильної поведінки програми, не впливаючи на продукцію. Можна незалежно написати спеціалізовані документовані файли, розділивши бізнес-код та код формальної перевірки.
Move Prover є корисним інструментом, що допомагає розробникам забезпечити правильність смартконтрактів. Він використовує формалізовану мову для опису поведінки програми і використовує алгоритми міркування для перевірки відповідності програми очікуванням. Це допомагає зменшити ризики угод, надаючи розробникам більше впевненості у впровадженні смартконтрактів у виробниче середовище.
4. Підсумок
Мова Move має відмінний дизайн безпеки, з усебічним врахуванням мовних характеристик, виконання віртуальної машини та рівня безпеки інструментів. Мовні характеристики жертвують частиною гнучкості, примусова перевірка типів і лінійна логіка полегшують автоматизацію компіляційної перевірки та формальної верифікації, а також безпечну верифікацію. Дизайн MoveVM відокремлює стан від логіки, що краще відповідає вимогам безпечного управління активами в блокчейні.
На мовному рівні Move може ефективно уникати вразливостей, що часто зустрічаються в EVM, таких як повторний вхід, переповнення, ін'єкція Call/DeleGateCall тощо. Але проблеми аутентифікації, логіки коду, переповнення структур великих цілих чисел все ще потребують уваги розробників. Move Prover може не спрацювати, якщо загальна ідея буде проігнорована.
Хоча мова Move враховує багато аспектів безпеки для програмістів, не існує абсолютно безпечних мов, а також не існує абсолютно безпечних програм. Рекомендується, щоб розробники смартконтрактів Move використовували послуги аудиту від третіх сторін, а також передали написання та перевірку частини коду specification стороннім безпековим компаніям.