Warning

Данная статья — это не рейтинг эффективности автоанализаторов. Я применяю их к собственным контрактам, намеренно синтезируя ошибки, и изучаю реакции. Такое исследование не может являться основанием для определения "лучше-хуже", для этого имеет смысл провести слепое исследование на большой выборке контрактов, которое, учитывая капризный характер такого рода ПО, провести крайне сложно. Вполне возможна ситуация, когда небольшая ошибка в контракте может отключить большой кусок логики анализатора, а простейший эвристический признак может добавить анализатору огромное число очков за счет нахождения широко распространенного бага, который конкуренты просто не успели добавить. Также могут сыграть роль ошибки в подготовке и компиляции контрактов. Все рассматриваемое ПО является довольно молодым, и дорабатывается постоянно, поэтому не стоит воспринимать критические замечания как непоправимые проблемы.

Цель статьи — дать читателю понимание того, как работают методы анализа кода в разных анализаторах и умение их правильно использовать, а не "определиться с выбором". Разумный выбор — использовать сразу несколько инструментов, делая акцент на наиболее подходящем для анализируемого контракта.

Настройка и подготовка к запуску

Mythril использует сразу несколько видов анализа, вот пара хороших статей о нем: самая главная, эта или эта. Перед продолжением имеет смысл их прочитать.

Для начала соберем свой собственный Docker образ Mythril (мало ли что мы захотим в нем поменять?):

git clone https://github.com/ConsenSys/mythril-classic.git
cd mythril-classic
docker build -t myth .

Теперь попробуем запустить его на нашем contracts/flattened.sol (я использую тот же контракт, который рассматривался во введении), в котором присутствуют два основных контракта, Ownable от Zeppelin и наш Booking. У нас по прежнему проблема с версией компилятора, я ее исправил тем же способом, что и в предыдущей статье, добавив в Dockerfile строки, которые заменят версию компилятора:

COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin

После пересборки образа, можно попробовать запустить анализ контракта. Сразу давайте использовать флаги -v4 и --verbose-report, чтобы увидеть все предупреждения. Поехали:

docker run -v $(pwd):/tmp            -w /tmp myth:latest            -v4            --verbose-report            -x contracts/flattened.sol

Здесь мы работаем с flattened контрактом без зависимостей. Чтобы проанализировать отдельный контракт Booking.sol и чтобы Mythril подхватил все зависимости, можно использовать примерно такую конструкцию:

docker run -v $(pwd):/tmp            -w /tmp myth:latest            --solc-args="--allow-paths /tmp/node_modules/zeppelin-solidity/  zeppelin-solidity=/tmp/node_modules/zeppelin-solidity"            -v4            --verbose-report            -x contracts/Booking.sol

Я предпочитаю работать с flattened вариантом, т.к. мы будем многое модифицировать в коде. Но у Mythril есть еще и крайне удобный режим --truffle, который просто протестирует все, что скомпилирует truffle, проверяя весь проект на предмет уязвимостей. Также важной фичей является возможность указать через двоеточие название контракта, который надо анализировать, иначе Mythril будет анализировать все встретившиеся контракты. Мы верим, что Ownable от OpenZeppelin — это безопасный контракт, и анализировать собираемся только Booking, поэтому финальная строка для запуска:

docker run -v $(pwd):/tmp -w /tmp myth:latest -x contracts/flattened.sol:Booking -v4 --verbose-report

Запуск и деплой контракта

Вышеуказанной строкой запускаем анализатор, смотрим вывод, и получаем среди прочего вот такую строку:

mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout)
The analysis was completed successfully. No issues were detected.

Оказывается, наш контракт не был создан и "задеплоен" в эмулятор. Именно поэтому я рекомендую для всех видов анализа использовать флаг -v4, чтобы видеть все сообщения и не пропустить ни одного важного. Давайте разбираться, что не так. Решение этой практической проблемы довольно важно для понимания того, как правильно использовать Mythril.

Итак, читаем про Mythril: It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. Если вы не сильно знакомы с этими терминами, рекомендую wiki про concolic testing тут, а вот хорошая презентация про taint checking для x86. Если кратко: Mythril эмулирует исполнение контракта, фиксирует ветви, по которым может пойти исполнение и пытается достичь "сломанного" состояния контракта, перебирая различные комбинации параметров и пытаясь обойти все возможные пути. Вот примерная схема действий из статьи выше:

1. Определить набор входных переменных для алгоритма. Это будут symbolic-переменные, а все остальные будут считаться просто конкретными значениями.
2. Запомнить эти переменные и каждую операцию, меняющую одну из этих переменных, записывать в trace файл. Также записывать все ошибки, и по дороге отмечать ветви кода, по которым проходит исполнение.
3. Выбрать стартовый набор значений переменных.
4. Нативно исполнить код контракта и сохранить trace-файл.
5. Выполнить symbolic execution поверх сохраненного trace, генерируя новые symbolic переменные, отмечая каждую новую ветвь, по которой может пойти исполнение, и планируя её будущий анализ.
6. Исключить текущую ветвь из непроанализированных, чтобы в следующий раз исполнение пошло по следующей непроанализированной ветви. Если таких не осталось, выходим.
7. Провести анализ ветви: во всех местах, где исполнение ветвится, определить набор input-ов, чтобы попасть в нужную ветвь, зафиксировать их и новую ветвь исполнения. Если такие input-ы найти не удалось, вернуться к п.6 и анализировать следующую ветвь.
8. Вернуться к п.4

Если сильно упростить, то Mythril, встретив ветвление в коде, может понять, при каких наборах переменных можно попасть и в одну и в другую ветвь. В каждой ветви Mythril знает, ведет ли она к assert, transfer, selfdestruct и другим важным для безопасности опкодам. Поэтому Mythril анализирует, какие наборы параметров и транзакций могут привести исполнение к нарушению безопасности. А способ, которым Mythril отсекает ветви, которые никогда не получат управление и анализирует control flow, и есть его основная фишка. Более подробно про кишки Mythril и хождение по ветвям написано тут.

Благодаря детерминистичности исполнения смарт-контрактов, одна и та же последовательность инструкций всегда ведет строго к одному набору изменений в state, вне зависимости от платформы, архитектуры и окружения. Также, функции в смарт-контрактах довольно короткие, а ресурсы — крайне ограничены, поэтому анализаторы типа Mythril, совмещающие symbolic и native execution, для смарт-контрактов могут крайне эффективно работать.

В процессе работы Mythril оперирует понятием "state" — это код контракта, его окружение, указатель на текущую команду, storage контракта и состояние стека. Вот из документации:

The machine state ? is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc ? P256, the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents ?m are a series of zeroes of size 256.

Граф переходов между state-ами является основным объектом исследования. В случае успешного запуска анализа, информация об этом графе выводится в лог анализа. Также, Mythril умеет строить этот граф в удобочитаемом виде при помощи опции --graph.

Теперь более-менее понимая, что будет делать Mythril, продолжим разбираться, почему контракт не анализируется и откуда взялось [WARNING]: No contract was created during the execution of contract creation. Для начала я покрутил параметр --create-timeout и --max-depth (как было рекомендовано) и, не получив результата, подумал, что виноват конструктор — что-то в нем не работает. Вот его код:

function Booking(
    string _description,
    string _fileUrl,
    bytes32 _fileHash,
    uint256 _price,
    uint256 _cancellationFee,
    uint256 _rentDateStart,
    uint256 _rentDateEnd,
    uint256 _noCancelPeriod,
    uint256 _acceptObjectPeriod
) public payable {
    require(_price > 0);
    require(_price > _cancellationFee);
    require(_rentDateStart > getCurrentTime());
    require(_rentDateEnd > _rentDateStart);

    require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd);
    require(_rentDateStart > _noCancelPeriod);

    m_description = _description;
    m_fileUrl = _fileUrl;
    m_fileHash = _fileHash;
    m_price = _price;
    m_cancellationFee = _cancellationFee;
    m_rentDateStart = _rentDateStart;
    m_rentDateEnd = _rentDateEnd;
    m_noCancelPeriod = _noCancelPeriod;
    m_acceptObjectPeriod = _acceptObjectPeriod;
}

Вспомним алгоритм действий Mythril. Для запуска trace необходимо вызвать конструктор контракта, ведь все последующее исполнение будет зависеть от того, с какими параметрами был вызван конструктор. К примеру, если вызвать конструктор с _price == 0, конструктор выдаст исключение на require(_price > 0). Даже если Mythril переберет множество значений _price, конструктор все равно будет ломаться, если, например _price <= _cancellationFee. В этом контракте с десяток параметров, связанных жесткими ограничениями, и Mythril, конечно, не может угадывать валидные комбинации параметров. Он пробует пройти на следующую ветвь исполнения, перебирая параметры конструктора, но шансов угадать у него практически нет — слишком много комбинаций параметров. Поэтому выкладка контракта не отрабатывает — все пути упираются в какой нибудь из require(...), и мы получаем вышеуказанную проблему.

Теперь у нас есть два пути: первый — отключить все require в конструкторе, закомментировав их. Тогда Mythril сможет вызвать конструктор с любым набором параметров и все отработает. Но это означает, что исследуя контракт с такими параметрами, Mythril найдет ошибки, которые возможны при неправильных значениях, переданных в конструктор. Проще говоря, если Mythril найдет баг, который возникает, если создатель контракта укажет _cancellationFee в миллиард раз больше, чем цена аренды _mprice, то толку от такого бага никакого — подобный контракт никогда не будет задеплоен, а ресурсы на поиск ошибок будут потрачены. Мы подразумеваем, что контракт всё-таки задеплоен с более-менее целостными параметрами, поэтому для дальнейшего анализа имеет смысл указать более реальные параметры конструктора, чтобы Mythril не искал ошибки, которые никогда не возникнут, если правильно задеплоить контракт.

Я провел много часов, пытаясь точно понять, на каком же месте деплой ломается, включая и отключая разные части конструктора. Вдобавок к моим бедам, в конструкторе используется getCurrentTime(), возвращающая текущее время, и неясно, как этот вызов обрабатывает Mythril. Я не буду описывать здесь эти приключения, т.к. скорее всего при регулярном использовании эти тонкости станут известны аудитору. Поэтому я выбрал второй путь: ограничить входные данные, и просто убрал все параметры из конструктора, даже getCurrentTime(), попросту захардкодив нужные параметры прямо в конструкторе (в идеале эти параметры стоит получить у заказчика):

   function Booking(                                                                                
    ) public payable {                                                                                                        
        m_description = "My very long booking text about hotel and beautiful sea view!";
        m_fileUrl = "https://ether-airbnb.bam/some-url/";
        m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7;
        m_price =           1000000000000000000; // 1 ETH
        m_cancellationFee = 100000000000000000; // 0.1 ETH
        m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day
        m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days
        m_acceptObjectPeriod = 3600 * 8; // 8 hours
        m_noCancelPeriod = 3600 * 24; // 1 day

        require(m_price > 0);
        require(m_price > m_cancellationFee);
        require(m_rentDateStart > 1550664800);
        require(m_rentDateEnd > m_rentDateStart);
        require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd);
        require(m_rentDateStart > m_noCancelPeriod);
    }                      

Плюс, чтобы все запустилось, надо еще выставить параметр max-depth. У меня заработало с этим конструктором при --max-depth=34 на AWS инстансе t2.medium. При этом, на моем ноутбуке, который помощней, все запускается без всяких max-depth. Судя по использованию этого параметра, он необходим для построения ветвей для анализа, а его дефолтное значение — infinity (код). Поэтому крутите-вертите этот параметр, но добейтесь того, чтобы нужный контракт был проанализирован. Понять это можно по сообщениям типа:

mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states
mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............

Первая строка как раз описывает граф, который будет анализироваться, остальные строки читайте сами. Для анализа различных ветвей, по которым может пойти исполнение, требуются серьезные вычислительные ресурсы, поэтому при анализе объемных контрактов придется подождать даже на быстром компьютере.

Поиск ошибок

Теперь будем искать ошибки и добавлять собственные. Mythril ищет ветви, в которых происходит отправка эфира, selfdestruct, assert, и другие действия, важные с точки зрения безопасности. Eсли где-то в коде контракта встречается одна из вышеописанных инструкций, Mythril изучает пути, по которым можно прийти к этой ветви и, более того, выводит последовательность транзакций, ведущую к данной ветви!

Для начала посмотрим что выдал Mythril на многострадальный Booking контракт. Первое предупреждение:

==== Dependence on predictable environment variable ====
SWC ID: 116
Severity: Low
Contract: Booking
Function name: fallback
PC address: 566
Estimated Gas Usage: 17908 - 61696
Sending of Ether depends on a predictable variable.
The contract sends Ether depending on the values of the following variables:
- block.timestamp
Note that the values of variables like coinbase, gaslimit, block number and timestamp are predictable and/or can be manipulated by a malicious miner. Don't use them for random number generation or to make critical decisions.
--------------------
In file: contracts/flattened.sol:142

msg.sender.transfer(msg.value-m_price)

а возникает она из-за

require(m_rentDateStart > getCurrentTime());

в fallback-функции.

Обратите внимание на то, что Mythril понял, что в getCurrentTime() прячется block.timestamp. Несмотря на то, что по смыслу контракта это не ошибка, то, что Mythril связывает block.timestamp с выдачей эфира — это отлично! В данном случае программист должен понимать, что решение принимается на основе значения, которое может контролировать майнер. И, если в будущем в этом месте контракта возникнет аукцион или иной торг за услугу, нужно учитывать возможность front-running атаки.

Посмотрим, увидит ли Mythril зависимость от block.timestamp, если мы спрячем переменную во вложенный вызов, вот так:

function getCurrentTime() public view returns (uint256) {
-     return now;
+     return getCurrentTimeInner();              
}                     

+ function getCurrentTimeInner() internal returns (uint256) {
+     return now;
+ }

И да! Mythril продолжает видеть связь между block.timestamp и transfer-ом эфира, это крайне важно для аудитора. Связь между переменной, контролируемой атакующим, и принятием решения после нескольких изменений состояния контракта, может быть очень сильно замаскирована логикой, и Mythril позволяет ее отследить. Хотя полагаться на то, что за вас отследят все возможные связи между всеми возможными переменными не стоит: если продолжить издеваться над функцией getCurrentTime() и сделать тройную глубину вложенности, предупреждение исчезнет. Каждый вызов функции для Mythril требует создания новых ветвлений state, поэтому анализ очень глубоких уровней вложенности потребует огромных ресурсов.

Есть конечно, довольно серьезная вероятность, что я просто неверно пользуюсь параметрами анализа или отсечка происходит где-то в глубинах анализатора. Как я уже говорил, продукт в активной разработке, я прямо в момент написания статьи вижу в репозитории коммиты с упоминанием max-depth, так что не воспринимайте всерьез текущие проблемы, мы уже нашли достаточно доказательств того, что Mythril может очень эффективно искать неявные связи между переменными.

Сначала добавим в контракт функцию, отдающую эфир кому попало, но только после того, как клиент послал эфир в контракт. Мы разрешили кому угодно забрать 1/5 эфира, но только когда контракт находится в состоянии State.PAID (т.е. только после того, как клиент оплатил эфиром снимаемый номер). Вот эта функция:

function collectTaxes() external onlyState(State.PAID) {
    msg.sender.transfer(address(this).balance / 5);
}

Mythril нашел проблему:

==== Unprotected Ether Withdrawal ====
SWC ID: 105                 
Severity: High               
Contract: Booking
Function name: collectTaxes()
PC address: 2492
Estimated Gas Usage: 2135 - 2746
Anyone can withdraw ETH from the contract account.
Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent a equivalent amount of ETH to it. This is likely to be a vulnerability.
--------------------
In file: contracts/flattened.sol:149

msg.sender.transfer(address(this).balance / 5)

--------------------
--------------------
Transaction Sequence:

{
    "2": {
        "calldata": "0x",
        "call_value": "0xde0b6b3a7640000",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    },
    "3": {
        "calldata": "0x01b613a5",
        "call_value": "0x0",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    }
}

Отлично, т.е. Mythril даже вывел две транзакции, которые приводят к тому, что из контракта можно забрать эфир. А теперь изменим требование State.PAID на State.RENT, вот так:

- function collectTaxes() external onlyState(State.PAID){
+ function collectTaxes() external onlyState(State.RENT) {

Теперь collectTaxes() можно вызвать, только когда контракт находится в состоянии State.RENT, а в этот момент на балансе ничего нет, т.к. контракт уже выслал весь эфир owner-у. И важно здесь то, что Mythril на этот раз уже НЕ выводит ошибку ==== Unprotected Ether Withdrawal ====! При условии onlyState(State.RENT) до ветви кода, которая высылает эфир из контракта с ненулевым балансом, анализатор не добрался. Mythril перебирал разные варианты параметров, но в State.RENT можно попасть, только отправив весь эфир арендодателю. Поэтому добраться до этой ветви кода, имея ненулевой баланс, невозможно, и Mythril совершенно правильно не тревожит аудитора!

Точно так же Mythril будет находить selfdestruct и assert, показывая аудитору, какие действия могут привести к уничтожению контракта или к поломке в важной функции. Эти примеры я не буду приводить, просто попробуйте сделать функцию, похожую на приведенную выше, только вызывающую selfdestruct, и покрутите ее логику.

Также, не забывайте, что одна из частей Mythril — это symbolic execution, а этот подход, сам по себе, без эмуляции исполнения, может определять множество уязвимостей. Например, можно считать уязвимостью "Integer overflow" любое использование "+", "-" и других арифметических операторов, если один из операндов хоть как-то контролируется атакующим. Но повторю еще раз, самая мощная возможность Mythril — это соединение symbolic и native execution и определение значений параметров, ведущих к ветвлению логики.

Заключение

Конечно, чтобы показать весь спектр потенциальных проблем, которые способен обнаруживать Mythril потребуется не одна, а несколько статей. Ко всем прочему, он умеет делать это все в реальном блокчейне, находя по сигнатурам нужные контракты и уязвимости, строить красивые графы вызовов, форматировать отчеты. Также, Mythril позволяет писать собственные сценарии тестирования, предоставляя python-based интерфейс к контракту и позволяющие с произвольной степенью гибкости протестировать отдельные функции, зафиксировать значения параметров, или вообще реализовать собственную стратегию работы с дизассемблированным кодом.

Mythril все-таки довольно молодой софт, это вам не IDA Pro, и документации, кроме нескольких статей, крайне мало. Значение многих параметров приходится лишь вычитывать в коде Mythril, начав с cli.py. Надеюсь, что полное и глубокое описание работы каждого параметра появится в документации.

Помимо этого, когда контракт более-менее большой, вывод кучи ошибок занимает много места, а хотелось бы иметь возможность получать и сжатую информацию о найденной ошибке, т.к. при работе с Mythril надо обязательно смотреть трассу анализа, видеть, какие контракты насколько удалось протестировать и иметь возможность принудительно отключить конкретные ошибки, которые аудитор расценивает как false-positive.

Ну а в целом, Mythril — отличный и крайне мощный инструмент для анализа смарт-контрактов и на данный момент должен быть в арсенале любого аудитора. Он позволяет как минимум обратить внимание на критические части кода и обнаружить скрытые связи между переменными.

Подводя итог, рекомендации по использованию Mythril такие:

1. Максимально сужайте стартовые условия исследуемого контракта. Если при анализе Mythril будет тратить много ресурсов на ветви, которые никогда не будут реализованы на практике, он потеряет возможность находить действительно важные баги, поэтому нужно все время стараться сужать область потенциальных ветвлений.
2. Следите за тем, запустился ли анализ контракта, не пропускайте сообщений типа mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout), иначе можете ошибочно посчитать, что багов нет.
3. Вы можете произвольно отключать ветви в коде контракта, давая Mythril меньше вариативности в выборе ветвей и экономя ресурсы. Постарайтесь обойтись без ограничений на max-depth, чтобы не "обрубать" анализ, но при этом будьте внимательны, чтобы не замаскировать ошибку.
4. Внимательно относитесь к каждому предупреждению, даже легкие замечания иногда стоят того, чтобы хотя бы добавить комментарий в код контракта, облегчая задачу другим разработчикам.

В следующей статье мы займемся анализатором Manticore, а вот все оглавление статей, которые готовы или планируются к написанию:

Часть 1. Введение. Компиляция, flattening, версии Solidity
Часть 2. Slither
Часть 3. Mythril (эта статья)
Часть 4. Manticore (в процессе написания)
Часть 5. Echidna (в процессе написания)