Аналіз безпеки Move: новатори в сфері смартконтрактів

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

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

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

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

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

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

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

3. Процес: визначення функцій та логіки модуля.

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

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

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

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

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

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

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

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

Статус виконання програми Move представлений чотирикутником ⟨C, M, G, S⟩, який включає стек викликів (C), пам'ять (M), глобальні змінні (G) та операнди (S). Стек також підтримує таблицю функцій для розпізнавання інструкцій, що містять тіла функцій.

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

3. Рух Ровер

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

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

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

1. Отримати Move вихідний файл як вхідні дані, який містить специфікацію вхідних даних програми.

2. Move Parser витягує специфікацію з вихідного коду.

3. Move компілятор перетворює вихідний файл у байткод, разом зі стандартною системою перетворює в модель об'єкта валідатора.

4. Об'єктна модель була перекладена в проміжну мову Boogie.

5. Система верифікації Boogie виконує "генерацію умов верифікації" для введення.

6. Перевірка умов передається у Z3 решатель ( розроблений Microsoft SMT решатель ).

7. Z3 перевіряє, чи SMT формула є неспроможною. Якщо так, це означає, що специфікація є дійсною; в іншому випадку генерує модель, що задовольняє умови.

8. Відновити звіт про діагностику до рівня виходу коду.

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

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

4. Підсумок

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

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

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