Мова Move, як нове покоління мов програмування для смарт-контрактів, з самого початку проектувалася з урахуванням безпеки блокчейну та смарт-контрактів. У цій статті буде розглянуто безпеку мови Move з трьох аспектів: характеристик мови, механізмів виконання та інструментів верифікації.
1. Безпекові характеристики мови Move
Мова Move відмовляється від нелінійної логіки, заснованої на гнучкості, не підтримує динамічну диспетчеризацію та рекурсивні зовнішні виклики, натомість використовує концепції таких, як узагальнення, глобальне зберігання, ресурси тощо для реалізації альтернативних моделей програмування. Ці дизайнерські рішення допомагають уникнути вразливостей безпеки, таких як повторне входження.
Основні складові мови Move включають:
Модуль: складається з визначень типів структури та процесу, може імпортувати визначення типів з інших модулів і викликати процеси з інших модулів.
Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення.
Процес: визначення функцій модуля, які можуть включати ініціалізацію, безпечні та небезпечні процеси.
Глобальний механізм зберігання даних мови Move дозволяє модулям зберігати постійні дані та має виключні права на читання та запис для оголошених типів ресурсів. Цей механізм допомагає забезпечити дотримання вимог безпеки.
Дві важливі статичні перевірки мови Move:
Перевірка незмінності: визначення збереження стану системи через мову специфікацій.
Біткод валідація: примусове виконання безпечних типів та лінійності, запобігання незаконним операціям.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині, не може безпосередньо отримати доступ до системної пам'яті. Виконання програми базується на стеку, глобальне сховище ділиться на пам'ять ( купу ) та глобальні змінні ( стек ).
Стан виконання Move VM складається з викликової пам'яті, пам'яті, глобальних змінних та масиву операцій. Його особливості включають:
Сусідність стеку викликів, щоб уникнути повторних входів
Розділення зберігання та виклику даних
Цей дизайн підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної перевірки, що використовує алгоритми дедуктивної перевірки для верифікації того, чи відповідає програма очікуванням. Його робочий процес:
Отримання Move вихідного файлу та стандартів
Скомпілювати в байт-код та об'єктну модель валідатора
Перетворити на проміжну мову Boogie
Генерація умов перевірки
Використання Z3 розв'язувача для верифікації
Генерація діагностичного звіту
Move Specification Language використовується для опису специфікацій поведінки програми, може бути написаний незалежно від бізнес-коду.
Підсумок
Мова 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.
17 лайків
Нагородити
17
8
Поділіться
Прокоментувати
0/400
HashBard
· 6год тому
все ще є вразливості... театральна безпека в найкращому вигляді, чесно кажучи
Переглянути оригіналвідповісти на0
AirdropHarvester
· 18год тому
бик Потрібно дотримуватися безпеки понад усе!
Переглянути оригіналвідповісти на0
CryptoNomics
· 18год тому
*сумно* ще один L1, що намагається провести формальну верифікацію... статистично незначний без належного аналізу рівноваги Неша, на мою думку
Переглянути оригіналвідповісти на0
ForumMiningMaster
· 18год тому
Просто люблю такі надійні гроші
Переглянути оригіналвідповісти на0
DegenGambler
· 18год тому
Статичний аналіз і все?
Переглянути оригіналвідповісти на0
ponzi_poet
· 18год тому
Все залежить від конкретних показників, статичне є статичним.
Переглянути оригіналвідповісти на0
fork_in_the_road
· 18год тому
Ще пишеш на solidity? Швидко увійти в позицію Move
Повний аналіз безпеки Move мови: від характеристик до інструментів верифікації
Аналіз безпеки мови Move
Мова Move, як нове покоління мов програмування для смарт-контрактів, з самого початку проектувалася з урахуванням безпеки блокчейну та смарт-контрактів. У цій статті буде розглянуто безпеку мови Move з трьох аспектів: характеристик мови, механізмів виконання та інструментів верифікації.
1. Безпекові характеристики мови Move
Мова Move відмовляється від нелінійної логіки, заснованої на гнучкості, не підтримує динамічну диспетчеризацію та рекурсивні зовнішні виклики, натомість використовує концепції таких, як узагальнення, глобальне зберігання, ресурси тощо для реалізації альтернативних моделей програмування. Ці дизайнерські рішення допомагають уникнути вразливостей безпеки, таких як повторне входження.
Основні складові мови Move включають:
Модуль: складається з визначень типів структури та процесу, може імпортувати визначення типів з інших модулів і викликати процеси з інших модулів.
Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення.
Процес: визначення функцій модуля, які можуть включати ініціалізацію, безпечні та небезпечні процеси.
Глобальний механізм зберігання даних мови Move дозволяє модулям зберігати постійні дані та має виключні права на читання та запис для оголошених типів ресурсів. Цей механізм допомагає забезпечити дотримання вимог безпеки.
Дві важливі статичні перевірки мови Move:
Перевірка незмінності: визначення збереження стану системи через мову специфікацій.
Біткод валідація: примусове виконання безпечних типів та лінійності, запобігання незаконним операціям.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині, не може безпосередньо отримати доступ до системної пам'яті. Виконання програми базується на стеку, глобальне сховище ділиться на пам'ять ( купу ) та глобальні змінні ( стек ).
Стан виконання Move VM складається з викликової пам'яті, пам'яті, глобальних змінних та масиву операцій. Його особливості включають:
Цей дизайн підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної перевірки, що використовує алгоритми дедуктивної перевірки для верифікації того, чи відповідає програма очікуванням. Його робочий процес:
Move Specification Language використовується для опису специфікацій поведінки програми, може бути написаний незалежно від бізнес-коду.
Підсумок
Мова Move враховує всі особливості мови, виконання віртуальної машини та рівень інструментів безпеки, що дозволяє ефективно уникати багатьох поширених вразливостей. Однак все ще рекомендується використовувати послуги стороннього аудиту безпеки та довіряти компаніям безпеки для написання та перевірки стандартного коду.