Что такое Securify, или как потерять 30 секунд, но сэкономить 30 миллионов долларов
Введение
Смарт-контракты, как известно, это это самоисполняющиеся контракты, в которых условия соглашения между покупателем и продавцом непосредственно прописаны в строках кода. Код и содержащиеся в нем соглашения существуют в распределенной децентрализованной сети блокчейна. Код контролирует выполнение, а транзакции отслеживаются и необратимы.
Так как контракты зачастую содержат на себе крупные денежные суммы, а транзакции необратимы, то проверка их на безопасность и наличие багов является необходимой.
Для примера, несколько дней назад был исправлен связанный с округлением баг в одном из контрактов библиотеки Solana Program Library, который использовался в множестве других контрактов. Суммарно этот баг мог привести к потерям на сумму около 2.6 миллиардов долларов США, если бы не был обнаружен аудиторской компанией Neodyme несколькими месяцами ранее.
Один из инструментов работы таких аудиторских компаний на другом, более популярном, но значительно менее быстром блокчейне ethereum является securify.
Хочется отметить, что данная статья не является гайдом по использованию securify, а является скорее заметкой о принципах работы данного инструмента.
Базовый принцип работы securify
Первым делом, securify переводит байт-код нашего смарт-контракта в последовательность семантических фактов на языке Datalog, после этого производится непосредственно проверка на уязвимости.
Разработчики securify довольно справедливо заметили, что существуют определенные конкретные шаблоны в data-flow графе смарт контрактов, которые означают конкретную уязвимость или отсутствие этой уязвимости (в зависимости от шаблона).
Основываясь на этой идее разработчики создали шаблоны на DSL языке для 37 уязвимостей из регистра уязвимости смарт-контрактов SWC Registry разного уровня критичности. Для каждой уязвимости существует по два шаблона:
Compliance — если этот шаблон присутствует в data-flow графе, значит уязвимость гарантированно отсутствует в контракте.
Violation — если этот шаблон присутствует в data-flow графе, значит уязвимость гарантированно присутствует в контракте.
Если для конкретной уязвимости не удалось найти присутствие ни одного из двух шаблонов, она помечается как Warning и требует ручной проверки.
Упрощенная схема работы securify
Securify имеет преимущество перед символьными анализаторами уязвимостей, позволяя сократить количество потенциальных уязвимостей, требующих ручной проверки в среднем на 65%, а проверяет один контракт в среднем за 30 секунд.
Более глубоко рассмотрим работу securify на примере:
Пример. Похищение Ethereum
Пусть мы разрабатываем кошелек на языке solidity
Мы написали две функции: инициализатор кошелька и функцию вывода.
Исходный код нашего простого кошелька
Предполагается следующий функционал:
Конструктор вызывает функцию initWallet, которая устанавливает значение переменной owner равным адресу, принимаемому функцией в качестве аргумента.
Функция withdraw принимает на вход аргумент _amount и, если адрес вызывающего эту функцию совпадает со значением переменной owner, переводит на адрес owner _amount монет.
Уязвимость заключается в том, что функция initWallet на самом деле может быть вызвана не только конструктором, но и любым внешним пользователем. То есть любой внешний пользователь может установить владельцем любого кошелька который будет работать на нашем смарт-контракте кого угодно, например, самого себя.
Кажется, что уязвимость довольно очевидная, и Вы бы, конечно, никогда её не допустили, а пример исключительно модельный и нерелевантный. С Вами не согласится компания Parity, которая допустила такую ошибку в разработке своего кошелька, что закономерно привело к тому, что в июле 2017 года с кошельков, которые работали на их смарт-контракте было украдено 30 миллионов долларов.
Сформулируем, что собой представляют уязвимость и, как не странно, её отсутствие:
Уязвимость заключается в том, что поле
ownerне имеет ограничения на запись, то есть все пользователи могут его модифицировать.Отсутствие уязвимости заключается в том, что поле
ownerимеет ограничение на запись, то есть некоторые пользователи не могут его модифицировать.
Чтобы доказать отсутствие уязвимости нам нужно показать, что существует пользователь, который не может отправить транзакцию изменяющую поле owner.
И наоборот, чтобы доказать наличие уязвимости нам нужно показать, что все пользователи могут отправить транзакцию изменяющую поле owner.
Предположим, что мы скомпилировали код нашего кошелька и подали полученный бинарный файл на вход securify.
Ниже представлены и описаны шаги, которые производит securify для проверки конкретной уязвимости:
Шаг 1. Декомпиляция байт-кода
На первом шаге Securify переводит байт-код в форму SSA, то есть избавляется от использования стека.
Например, инструкция push 0x04 переходит в инструкцию a = 0x04, а инструкции с 09 по 0E (являющиеся представлением функции initWallet) превращаются в метод ABI_9DA8(b) .
Шаг 2. Вывод семантических фактов
После декомпиляции securify анализирует полученный код на наличие семантических фактов, включющих зависимости в потоках данных и управления, которые, по сути, полностью описывают поведение контракта. Например, факт MayDepOn(b, dataload) фиксирует, что значение переменной b может зависеть от функции dataload. Eq(c, 0x00) фиксирует, что переменная c равна константе 0x00.
Вывод семантических фактов Securify определяется декларативно на языке Datalog, что позволяет легко расширять набор фактов и правил вывода при необходимости.
Шаг 3. Проверка шаблонов уязвимостей
После получения семантических фактов securify проверяет набор шаблонов, поданых на вход.
Шаблоны должны быть написаны на специальном DSL языке, который позволяет пользователю добавлять кастомные шаблоны.
На картинке видно, что securify сопоставляет шаблон уязвимости с инструкцией sstore(c, b). Данная инструкция записывает в ячейку памяти c (место расположения переменной owner) значение b.
Этот шаблон проверяет, существует ли в коде хотя бы одна инструкция sstore(X, L), в которой ни X ни L не зависят от значения caller (адрес, который вызывает функцию), то есть ищет поля без ограничения на запись.
На языке шаблонов Securify этот шаблон будет выглядеть следующим образом:
Видно, что такая инструкция существует, что и отобразится в результате отработки Securify.
Таким образом, securify предоставляет из себя модифицируемый и расширяемый инструмент для анализа уязвимостей в смарт-контрактах на Ethereum.
C документацией по использованию можно ознакомиться на гитхабе проекта.
