Аналіз безпеки Move: прорив нового покоління смартконтрактів
Мова Move – це мова смарт-контрактів, розроблена для блокчейн-середовищ з унікальними функціями безпеки. У цій статті обговорюється безпека мови Move з трьох аспектів: характеристики мови, механізм роботи та інструменти верифікації.
1. Безпекові особливості мови Move
Мова Move відмовилася від більш гнучких, але небезпечних функцій, таких як динамічний виклик і рекурсивні зовнішні виклики, натомість впроваджуючи концепції, такі як генерики, глобальне зберігання, ресурси тощо, для реалізації альтернативних моделей програмування. Ці дизайни допомагають уникнути поширених вразливостей, таких як повторний вхід.
Основний механізм безпеки Move включає:
Модуль: кожен модуль складається з типу структури та визначення процесу, може імпортувати визначення типів інших модулів і викликати їх процеси.
Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення.
Процес: визначає функції та логіку смартконтракту.
Глобальне сховище: дозволяє постійно зберігати дані, доступ до яких може бути програмно зчитаний і записаний лише володарем модуля.
Перевірка незмінних: визначення консервності стану системи за допомогою мови специфікацій.
Верифікатор байт-коду: примусове виконання системи типів на рівні байт-коду, запобігання незаконним операціям з чутливими значеннями.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині і не може безпосередньо отримати доступ до системної пам'яті. MoveVM використовує стековий інтерпретатор для виконання байт-коду, відокремлюючи управління сховищем даних і стеком викликів.
Стан програми Move складається з стеку викликів, пам'яті, глобальних змінних та масиву операцій. Під час виконання стек викликів зберігає контекстну інформацію, статичний перехід уникає динамічної диспетчеризації, що підсилює незмінність виклику функцій.
Цей дизайн відокремлює стан користувача ( ресурси ) і логіку програми, що підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної верифікації, який використовує алгоритми дедуктивної верифікації для перевірки того, чи відповідає програма очікуванням. Його робочий процес виглядає так:
Отримайте вихідний файл Move та специфікацію
Скомпілювати в байт-код і модель об'єкта валідатора
Перетворити в проміжну мову Boogie
Генерація умов верифікації
Використовуйте Z3-решатель для перевірки задовільності формули
Генерація діагностичного звіту
Move Specification Language використовується для опису специфікацій поведінки програми, може бути написана незалежно від бізнес-коду. Це надає додатковий шлях для верифікації третім сторонам безпеки.
Підсумок
Мова Move була спроектована з урахуванням безпеки, з повною оптимізацією характеристик мови, виконання віртуальної машини та інструментів перевірки. Вона може ефективно уникати поширених вразливостей, таких як повторні входи та переповнення, але все ще потрібно звертати увагу на питання безпеки, такі як аутентифікація та логіка.
Хоча Move забезпечує хорошу безпеку, рекомендується, щоб розробники все ж використовували послуги стороннього аудиту та розглянули можливість передати написання та перевірку стандартів професійній безпековій команді для подальшого підвищення безпеки смартконтрактів.
Ця сторінка може містити контент третіх осіб, який надається виключно в інформаційних цілях (не в якості запевнень/гарантій) і не повинен розглядатися як схвалення його поглядів компанією Gate, а також як фінансова або професійна консультація. Див. Застереження для отримання детальної інформації.
11 лайків
Нагородити
11
9
Поділіться
Прокоментувати
0/400
DaoResearcher
· 07-23 18:12
Цитуючи третю главу теорії управління Віталіка, цей стековий дизайн безпечніший за EVM у понад 67% випадків.
Переглянути оригіналвідповісти на0
ShibaOnTheRun
· 07-23 17:08
Аудит, аудит, все ж таки потрібно проводити аудит.
Переглянути оригіналвідповісти на0
BearMarketSurvivor
· 07-23 03:14
переміщення таке сильне? Вивчи це
Переглянути оригіналвідповісти на0
NullWhisperer
· 07-23 01:37
теоретично безпечний, все ще потребує пен-тестування... типова надмірна впевненість у формальних методах, чесно кажучи
Переглянути оригіналвідповісти на0
MEVHunterLucky
· 07-20 19:12
Знову прийшли спекуляції щодо move
Переглянути оригіналвідповісти на0
MEVHunterBearish
· 07-20 19:11
переміщення все ще потрібно підніматися
Переглянути оригіналвідповісти на0
¯\_(ツ)_/¯
· 07-20 19:11
Тестування є тестуванням, безпека на першому місці
Аналіз безпечних характеристик мови Move: створення більш безпечного середовища для розробки смартконтрактів
Аналіз безпеки Move: прорив нового покоління смартконтрактів
Мова Move – це мова смарт-контрактів, розроблена для блокчейн-середовищ з унікальними функціями безпеки. У цій статті обговорюється безпека мови Move з трьох аспектів: характеристики мови, механізм роботи та інструменти верифікації.
1. Безпекові особливості мови Move
Мова Move відмовилася від більш гнучких, але небезпечних функцій, таких як динамічний виклик і рекурсивні зовнішні виклики, натомість впроваджуючи концепції, такі як генерики, глобальне зберігання, ресурси тощо, для реалізації альтернативних моделей програмування. Ці дизайни допомагають уникнути поширених вразливостей, таких як повторний вхід.
Основний механізм безпеки Move включає:
Модуль: кожен модуль складається з типу структури та визначення процесу, може імпортувати визначення типів інших модулів і викликати їх процеси.
Структура: може бути визначена як тип ресурсу, зберігається в глобальному сховищі ключ-значення.
Процес: визначає функції та логіку смартконтракту.
Глобальне сховище: дозволяє постійно зберігати дані, доступ до яких може бути програмно зчитаний і записаний лише володарем модуля.
Перевірка незмінних: визначення консервності стану системи за допомогою мови специфікацій.
Верифікатор байт-коду: примусове виконання системи типів на рівні байт-коду, запобігання незаконним операціям з чутливими значеннями.
2. Механізм роботи Move
Програма Move виконується у віртуальній машині і не може безпосередньо отримати доступ до системної пам'яті. MoveVM використовує стековий інтерпретатор для виконання байт-коду, відокремлюючи управління сховищем даних і стеком викликів.
Стан програми Move складається з стеку викликів, пам'яті, глобальних змінних та масиву операцій. Під час виконання стек викликів зберігає контекстну інформацію, статичний перехід уникає динамічної диспетчеризації, що підсилює незмінність виклику функцій.
Цей дизайн відокремлює стан користувача ( ресурси ) і логіку програми, що підвищує безпеку та ефективність виконання.
3. Рух Ровер
Move Prover є інструментом формальної верифікації, який використовує алгоритми дедуктивної верифікації для перевірки того, чи відповідає програма очікуванням. Його робочий процес виглядає так:
Move Specification Language використовується для опису специфікацій поведінки програми, може бути написана незалежно від бізнес-коду. Це надає додатковий шлях для верифікації третім сторонам безпеки.
Підсумок
Мова Move була спроектована з урахуванням безпеки, з повною оптимізацією характеристик мови, виконання віртуальної машини та інструментів перевірки. Вона може ефективно уникати поширених вразливостей, таких як повторні входи та переповнення, але все ще потрібно звертати увагу на питання безпеки, такі як аутентифікація та логіка.
Хоча Move забезпечує хорошу безпеку, рекомендується, щоб розробники все ж використовували послуги стороннього аудиту та розглянули можливість передати написання та перевірку стандартів професійній безпековій команді для подальшого підвищення безпеки смартконтрактів.