Мова Move, як нове покоління мов програмування для смарт-контрактів, з самого початку проектувалася з урахуванням безпеки блокчейну та смарт-контрактів. У цій статті буде розглянуто безпеку мови Move з трьох аспектів: характеристик мови, механізмів виконання та інструментів верифікації.
1. Безпекові характеристики мови Move
Мова Move відмовляється від нелінійної логіки, заснованої на гнучкості, не підтримує динамічну диспетчеризацію та рекурсивні зовнішні виклики, натомість використовує концепції таких, як узагальнення, глобальне зберігання, ресурси тощо для реалізації альтернативних моделей програмування. Ці дизайнерські рішення допомагають уникнути вразливостей безпеки, таких як повторне входження.
Основні складові мови Move включають:
Модуль: складається з визначень типів структури та процесу, може імпортувати визначення типів з інших модулів і викликати процеси з інших модулів.
Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення.
Процес: визначення функцій модуля, які можуть включати ініціалізацію, безпечні та небезпечні процеси.
Глобальний механізм зберігання даних мови Move дозволяє модулям зберігати постійні дані та має виключні права на читання та запис для оголошених типів ресурсів. Цей механізм допомагає забезпечити дотримання вимог безпеки.
Дві важливі статичні перевірки мови Move:
Перевірка незмінності: визначення збереження стану системи через мову специфікацій.
Біткод валідація: примусове виконання безпечних типів та лінійності, запобігання незаконним операціям.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині, не може безпосередньо отримати доступ до системної пам'яті. Виконання програми базується на стеку, глобальне сховище ділиться на пам'ять ( купу ) та глобальні змінні ( стек ).
Стан виконання Move VM складається з викликової пам'яті, пам'яті, глобальних змінних та масиву операцій. Його особливості включають:
Сусідність стеку викликів, щоб уникнути повторних входів
Розділення зберігання та виклику даних
Цей дизайн підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної перевірки, що використовує алгоритми дедуктивної перевірки для верифікації того, чи відповідає програма очікуванням. Його робочий процес:
Отримання Move вихідного файлу та стандартів
Скомпілювати в байт-код та об'єктну модель валідатора
Перетворити на проміжну мову Boogie
Генерація умов перевірки
Використання Z3 розв'язувача для верифікації
Генерація діагностичного звіту
Move Specification Language використовується для опису специфікацій поведінки програми, може бути написаний незалежно від бізнес-коду.
Підсумок
Мова Move враховує всі особливості мови, виконання віртуальної машини та рівень інструментів безпеки, що дозволяє ефективно уникати багатьох поширених вразливостей. Однак все ще рекомендується використовувати послуги стороннього аудиту безпеки та довіряти компаніям безпеки для написання та перевірки стандартного коду.
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
Повний аналіз безпеки Move мови: від характеристик до інструментів верифікації
Аналіз безпеки мови Move
Мова Move, як нове покоління мов програмування для смарт-контрактів, з самого початку проектувалася з урахуванням безпеки блокчейну та смарт-контрактів. У цій статті буде розглянуто безпеку мови Move з трьох аспектів: характеристик мови, механізмів виконання та інструментів верифікації.
1. Безпекові характеристики мови Move
Мова Move відмовляється від нелінійної логіки, заснованої на гнучкості, не підтримує динамічну диспетчеризацію та рекурсивні зовнішні виклики, натомість використовує концепції таких, як узагальнення, глобальне зберігання, ресурси тощо для реалізації альтернативних моделей програмування. Ці дизайнерські рішення допомагають уникнути вразливостей безпеки, таких як повторне входження.
Основні складові мови Move включають:
Модуль: складається з визначень типів структури та процесу, може імпортувати визначення типів з інших модулів і викликати процеси з інших модулів.
Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення.
Процес: визначення функцій модуля, які можуть включати ініціалізацію, безпечні та небезпечні процеси.
Глобальний механізм зберігання даних мови Move дозволяє модулям зберігати постійні дані та має виключні права на читання та запис для оголошених типів ресурсів. Цей механізм допомагає забезпечити дотримання вимог безпеки.
Дві важливі статичні перевірки мови Move:
Перевірка незмінності: визначення збереження стану системи через мову специфікацій.
Біткод валідація: примусове виконання безпечних типів та лінійності, запобігання незаконним операціям.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині, не може безпосередньо отримати доступ до системної пам'яті. Виконання програми базується на стеку, глобальне сховище ділиться на пам'ять ( купу ) та глобальні змінні ( стек ).
Стан виконання Move VM складається з викликової пам'яті, пам'яті, глобальних змінних та масиву операцій. Його особливості включають:
Цей дизайн підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної перевірки, що використовує алгоритми дедуктивної перевірки для верифікації того, чи відповідає програма очікуванням. Його робочий процес:
Move Specification Language використовується для опису специфікацій поведінки програми, може бути написаний незалежно від бізнес-коду.
Підсумок
Мова Move враховує всі особливості мови, виконання віртуальної машини та рівень інструментів безпеки, що дозволяє ефективно уникати багатьох поширених вразливостей. Однак все ще рекомендується використовувати послуги стороннього аудиту безпеки та довіряти компаніям безпеки для написання та перевірки стандартного коду.