Обеспечение движения

Dec 13 2022
Aptos Labs и OtterSec Сеть Aptos использует язык смарт-контрактов Move в качестве базовой модели программирования. Хотя Move разработан для экосистемы безопасных смарт-контрактов, неправильная реализация самого Move может поставить под угрозу эти свойства.

от Aptos Labs и OtterSec

Сеть Aptos использует язык смарт-контрактов Move в качестве базовой модели программирования. Хотя Move разработан для экосистемы безопасных смарт-контрактов, неправильная реализация самого Move может поставить под угрозу эти свойства. В Aptos Labs мы стремимся сделать Move максимально безопасным вместе с сообществом. Мы оба инвестируем в инструменты для написания правильных смарт-контрактов (например, Move Prover, разработанный преимущественно Aptos), а также в корректность основных компонентов среды выполнения, таких как виртуальная машина Move. В этой статье мы описываем, как мы вместе с нашими партнерами достигаем последнего посредством аудита, вознаграждения за обнаружение ошибок, фаззинга и усиления безопасности базовой реализации.

Что мы защищаем?

Безопасность Move основана на нескольких основных свойствах. Эти свойства определяются в терминах байт -кода , который использует механизм выполнения Move, и не зависят от исходного языка:

  • Безопасность типов : каждое значение имеет уникальный и не поддающийся подделке тип. Например, невозможно взять какое-либо значение типа «адрес» и превратить его в относящийся к безопасности токен типа «подписавший».
  • Модульная инкапсуляция : ресурсами в хранилище можно управлять только из кода в модулях, которые объявляют эти ресурсы. Кроссмодульными могут называться только функции с совпадающей видимостью.
  • Право собственности и время жизни : система способностей Move гарантирует, что значение не будет скопировано, удалено, сохранено или использовано в качестве ключа, если соответствующая способность не объявлена ​​для типа значения.
  • Безопасность ссылок : ссылки не переживают значения, на которые они указывают. Изменяемая ссылка является исключительной собственностью, поэтому псевдоним невозможен.

Нас интересуют следующие вопросы:

  1. Является ли верификатор байт-кода полным и гарантирует ли он, что все вышеперечисленные свойства выполняются для каждой программы? Это важно, потому что нарушение любого из вышеперечисленных свойств потенциально может привести к потере активов.
  2. Может ли данная программа с байт-кодом Move привести к сбою механизма выполнения? Поскольку в реплицированном конечном автомате все узлы выполняют одни и те же программы, это можно использовать для остановки сети.
  3. Может ли данная программа вызвать исчерпание ресурсов (памяти или времени) механизма выполнения? Это можно использовать для DoS-атак, замедляющих или приостанавливающих работу сети.

В основе разработки безошибочного кода лежат дисциплинированные методы разработки программного обеспечения в сочетании с правильными инструментами. В Aptos мы следуем строгому процессу обязательной проверки кода, непрерывного тестирования и интеграции в сочетании с лучшими практиками экосистемы Rust. В дополнение к этим традиционным аспектам мы также применяем следующие меры, чтобы обеспечить максимальную безопасность Move.

Аудит и Консалтинг

Одним из самых уважаемых в отрасли способов завоевать доверие к блокчейн-сетям является аудит. В Aptos Labs мы заключили контракт с Certik ( отчет ) и Holburn на аудит виртуальной машины Move. Было обнаружено несколько критических проблем, одна из них относится к категории безопасности типов.

В дополнение к внешнему аудиту Aptos Labs возглавила и организовала аудит сообщества, сосредоточив внимание на верификаторе байт -кода. Инженеры из Mysten Labs, Starcoin и аудиторских компаний, таких как MoveBit и OtterSec, объединились с инженерами Aptos для этой работы, потратив около 6 человеко-недель на аудит. Результаты этого отражены в этой электронной таблице со ссылкой на десятки документов, созданных в ходе этого аудита. Эта проверка выявила и устранила множество проблем до того, как Aptos попала в основную сеть.

И последнее, но не менее важное: мы тесно сотрудничаем с OtterSec . Команда OtterSec провела проверку кода вручную и разработала технологию фаззинга для различных целей, выявив несколько критических проблем как в коде Move VM, так и в коде платформы Aptos. Они также возглавили усилия по добавлению избыточной логики глубокоэшелонированной защиты в виртуальную машину Move (см. ниже), что повлияло на нашу текущую работу по проектированию, направленную на устранение дальнейших уязвимостей, связанных с потерей средств.

Баг Баунти

Aptos Labs запускает программу вознаграждения за обнаружение ошибок . За критические ошибки, которые могут привести к потере активов, предлагаются награды до 1 000 000 долларов. Точно так же за ошибки, связанные с сбоем, можно получить до 100 000 долларов.

В рамках программы вознаграждений мы тесно сотрудничали с группой талантливых исследователей безопасности, чтобы найти и исправить ошибки. Некоторые из этих ошибок относились к критической категории, а другие ошибки были обнаружены с помощью фаззеров.

Aptos Labs выполнила свои обязательства по вознаграждениям за ошибки, и были выплачены значительные вознаграждения. Более того, Aptos Labs продолжает использовать опыт белых хакеров, с которыми мы познакомились в рамках программы вознаграждений, и намерена продолжать работать вместе с этим сообществом.

Фаззинг

Программа поощрения побудила нас инвестировать в фаззинг в Aptos Labs. Код Move VM был изменен для реализации свойства фаззинга Rust «Произвольный» в соответствующих точках, что позволяет использовать «грузовой фазз» для динамической генерации и проверки модулей байт-кода. У нас есть несколько непрерывных заданий, выполняемых с этими целями фаззинга.

Избыточность

Одним из способов достижения дополнительной гарантии безопасности является резервирование. Мы добавили в Move VM так называемый параноидальный режим , который обеспечивает безопасность типов и другие упомянутые выше правила во время выполнения. В то время как верификатор байт-кода уже проверяет такие свойства, когда код входит в систему, параноидальный режим повторно проверяет те же самые проверки во время выполнения байт-кода. Параноидальный режим широко обсуждался в сообществе Move, а инженеры Aptos руководили разработкой. Для получения дополнительной информации см. этот PR (окончательная версия) и этот PR (промежуточная версия).

Что дальше?

В Aptos Labs мы стремимся сделать Move максимально безопасным и вложили значительные средства в эту область. Здесь мы описали текущие усилия по аудиту, вознаграждениям за ошибки, фаззингу и усилению безопасности, проводимые нами и нашими партнерами. В дальнейшем мы планируем продолжать инвестировать в это пространство. Мы продолжим предлагать программу вознаграждения за обнаружение ошибок, сотрудничать с авторитетными аудиторами безопасности и стимулировать разработку средств повышения безопасности, например технологии фаззинга.