В июне 2016 года нарастало волнение по поводу того, что «The DAO», построенный на блокчейне Ethereum, вот-вот станет первым в мире полностью цифровым децентрализованным инвестиционным фондом.

Но через несколько недель он стал образцом хакерских атак DeFi после того, как злоумышленники украли у него эфира на сумму 50 миллионов долларов.

Чтобы взломать The DAO, злоумышленник воспользовался так называемой уязвимостью повторного входа, уязвимостью параллелизма, при которой один метод конкретного смарт-контракта вызывается, пока другой метод все еще выполняется, и DAO является лишь частью долгосрочной разработки смарт-контракт. Первый страдает от таких ошибок.

Среди выдающихся преемников — Uniswap/Lendf.Me, у которой в 2020 году было украдено 25 миллионов долларов, CREAM, у которой в 2021 году было украдено 18 миллионов долларов, и Fei, у которой в 2022 году было украдено 80 миллионов долларов.

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

Более того, эти взаимодействия зачастую трудно протестировать автоматически и систематически.

TLA+: Истребитель

Введите временную логику действий (TLA+), язык для определения и проверки сложных систем. TLA+ не только находит ошибки, но и проверяет их существование.

Как это возможно, спросите вы? TLA+ поставляется с набором инструментов для облегченной формальной проверки в форме так называемой проверки модели. Посредством проверки модели он исчерпывающе исследует все возможные параллельные взаимодействия модели кода — те самые области, которые сложно протестировать — и находит ошибки.

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

Чтобы проиллюстрировать это некоторыми вымышленными цифрами: если стандартные отраслевые методы, такие как тестирование и проверки безопасности, устраняют 80% ошибок, а «тяжелая» формальная проверка устраняет 99%, то использование TLA+ устраняет 90% с помощью всего лишь одного небольшого количества тяжелых проверок.

TLA+ и Интернет-компьютеры

Наша команда инженеров использует TLA+ для анализа всех аспектов интернет-вычислений, включая критически важные для безопасности смарт-контракты, которые выполняются на платформе. Хотя компьютеры Ethereum и Интернета имеют разные модели выполнения, ошибки повторного входа могут возникать в смарт-контрактах на обоих блокчейнах.

Фактически, благодаря своей высокой пропускной способности компьютеры в Интернете допускают несколько одновременных вызовов одного смарт-контракта, что требует от авторов смарт-контрактов быть более осторожными, чтобы исключить нежелательные одновременные взаимодействия. Поскольку безопасность имеет решающее значение для успеха компьютеров в Интернете, TLA+ используется во многих смарт-контрактах для обнаружения ошибок на этапе разработки.

Контейнер анализа TLA+ (смарт-контракты для компьютеров в Интернете) недавно был проведен для недавно выпущенного биткойна Chain-Key (ckBTC), результатами которого я поделюсь ниже.

Смарт-контракт ckBTC

Чтобы поговорить об анализе TLA+ ckBTC, давайте начнем с общего обзора ckBTC. ckBTC — это собственный токен интернет-компьютера, надежно обеспеченный биткойнами (BTC) в соотношении 1:1.

Реестр ckBTC — это контейнерный смарт-контракт в компьютерной цепочке блоков Интернета, который отслеживает, сколько ckBTC принадлежит каждому конечному пользователю. Этот же реестр позволяет конечным пользователям передавать свои ckBTC другим конечным пользователям быстрее и дешевле, чем передача BTC в сети Биткойн.

Чтобы конвертировать ckBTC в BTC и обратно, конечные пользователи взаимодействуют с другим смарт-контрактом — минтером ckBTC.

На высоком уровне операция конвертации BTC в ckBTC выглядит следующим образом:

Шаги для получения ckBTC:

1. Конечный пользователь сначала переводит некоторое количество BTC на определенный пользователем адрес депозита в биткойнах. Все адреса депозита полностью контролируются кодом смарт-контейнера ckBTC minter благодаря подписи ECDSA с цепным ключом, которая создает новый UTXO, принадлежащий депозиту. адрес;

2. Конечный пользователь уведомляет монетный двор ckBTC о новом депонированном UTXO, прося монетный двор обновить баланс пользователя;

3. Смарт-контракт минтера затем использует интеграцию Биткойн с интернет-компьютерами для получения всех UTXO, принадлежащих контролируемому минтером, но индивидуальному для пользователя адресу депозита. Затем минтер выбирает новые UTXO из сети Биткойн, отправляя им перекрестные проверки. свой внутренний бухгалтерский список обработанных им UTXO;

4. Наконец, минтер дает указание реестру чеканить новые ckBTC для всех новых UTXO в соотношении 1:1, а после завершения добавляет вновь обнаруженные UTXO в список обработанных UTXO.

Отказ от ответственности: в приведенном выше процессе для простоты отсутствует процесс KYT (Знай свою транзакцию).

Смарт-контракт ckBTC соответствует TLA+

Представленная выше общая картина на самом деле скрывает незначительную проблему параллелизма, и хорошая новость заключается в том, что мы можем обнаружить проблему с помощью инструментария TLA+.

Но прежде чем TLA+ сможет что-либо обнаружить, мы должны сначала предоставить ему две вещи:

• Создайте модель нашей системы, используя язык TLA+.

• Укажите свойства TLA+, которые мы ожидаем от системы.

Эта модель представляет собой упрощенную, но все же полностью определенную версию системы, которая в нашем случае включает в себя смарт-контракт минтера, а также все другие соответствующие части системы, а именно контракт реестра и сеть Биткойн.

Для каждого компонента мы моделируем его состояние и то, как соответствующие действия, которые может предпринять конечный пользователь (например, перевести BTC или ckBTC, внести BTC или вызвать различные действия, предоставляемые минтером), изменяют состояние.

Все эти элементы в модели несколько упрощены: части, на которых фокусируется анализ (например, код минтера), моделируются более подробно, тогда как другие части (например, сеть Биткойн) моделируются менее подробно, фактически модель TLA+. аналогично подробному проектному заданию системы.

Интуитивно понятно, что главная функция, которую мы хотим реализовать, — это обеспечить полную поддержку нашего ckBTC. Другими словами, ни один конечный пользователь не должен иметь возможность «вдвойне потратить» свои внесенные BTC, чтобы получить больше ckBTC, чем они внесли.

Но чтобы проанализировать такое свойство, нам нужно сделать это интуитивное представление очень точным, формально выразив его на языке TLA+. Наше формальное определение заключается в том, что общее количество ckBTC (т. е. сумма всех балансов ckBTC конечных пользователей, хранящихся в реестре ckBTC) не превышает общее количество BTC, контролируемое контейнером для монет (т. е. стоимость всех UTXO, принадлежащие депозитному адресу).

Обнаружение и решение проблем

После того как мы создали модель и свойства, набор инструментов TLA+ может проанализировать модель. Чтобы запустить анализ, мы сначала определяем настройки для запуска анализа. Например, наша настройка ckBTC включает только двух разных конечных пользователей и небольшую часть общего количества биткойнов (например, 5 сатоши).

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

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

Например, анализ может показать, что мы можем нарушить наше свойство «нет незащищенных ckBTC» в сценарии, подобном показанному ниже:

здесь:

• Конечные пользователи вносят BTC, как и раньше;

• Однако теперь конечный пользователь дает указание минтеру ckBTC обновить баланс дважды в быстрой последовательности, и на интернет-компьютере эти обновления могут одновременно взаимодействовать с другими смарт-контрактами;

• Два обновления, работающие одновременно, запрашивают у сети Биткойн все UTXO, депонированные конечным пользователем, и оба получают в ответ один и тот же UTXO, депонированный на шаге 1. Поскольку UTXO еще не находится в «обработанном» списке, оба обновления считают, что UTXO является новым;

• Оба обновления предписывают реестру отчеканить соответствующее количество ckBTC на шаге 4.

Таким образом, в конце шага 4 мы находимся в состоянии, когда предложение ckBTC в два раза превышает сумму UTXO на депозитных адресах, что нарушает наше свойство «нет неподдерживаемых ckBTC».

Обратите внимание, что эта ошибка возникает только потому, что обновления баланса конечного пользователя выполняются одновременно — на самом деле это повторная ошибка в том же стиле, что и та, которая привела к сбою The DAO.

Одним из способов решения этой проблемы является предотвращение параллельного запуска обновлений баланса для одного и того же конечного пользователя. Мы можем сделать это, заставив минтер хранить конечного пользователя в «заблокированном» списке пользователей при запуске обновления баланса и хранить его там. на время действия списка обновлений для достижения этой цели.

Если конечный пользователь попытается инициировать другое параллельное обновление баланса, обновление сначала проверит и найдет этого конкретного конечного пользователя в списке заблокированных пользователей, а затем прервется.

Обратите внимание, что здесь мы немного упрощаем атаку: блокировка на самом деле является довольно распространенным шаблоном для смарт-контрактов IC, и минтеры ckBTC использовали его с самого начала. Однако неправильно выполненная блокировка открывает дверь для вышеупомянутых атак, которые TLA+ способен обнаружить.

Кроме того, мы обнаружили некоторые крайние случаи, которые нарушали «нет неподдерживаемого ckBTC» и другие важные свойства, и как только мы применили все исправления, TLA+ смогла проверить и подтвердить, что в нашей определенной настройке больше не было нарушений свойств.

Стоит ли использовать TLA+ для своих смарт-контрактов?

Абсолютно! Ладно-ладно, может быть, мне следует дать более детальный ответ, который наша команда исследований и разработок использует для критически важных смарт-контрактов на компьютерах в Интернете, когда речь идет о нетривиальном параллелизме.

Например, анализ TLA+ выявил тонкие ошибки параллелизма в управлении компьютерами в Интернете и контейнерах бухгалтерской книги, которые были пропущены в предыдущих ручных проверках безопасности и могли привести к серьезным проблемам, случаям и пунктам — TLA+ сыграл важную роль в раскрытии таких сложных проблем. Абсолютный взрыв.

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

Не стоит пугаться самого языка TLA+, несмотря на устрашающее название, доступ к его мощным функциям довольно прост. Фактически, шпаргалка TLA+, описывающая почти все функции TLA+, примерно умещается на странице:

• mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html

Более того, усилия, необходимые для построения модели, сопоставимы со стандартными ручными проверками безопасности. Например, минтеру ckBTC одному человеку потребуется в общей сложности около 3 недель, чтобы понять дизайн, создать исходную модель и свойства.

Полученная модель TLA+ намного проще реализации, как потому, что она проще кода, так и из-за высокоуровневой природы TLA+. Модель минтера ckBTC требует около 250 строк кода по сравнению с тысячами строк реализации Rust. Возможно, это удивительно, но одной из самых сложных задач с точки зрения усилий является определение требуемых свойств, поскольку в интуитивно понятных спецификациях часто обнаруживаются пробелы.

После создания модели анализ (проверка модели) завершается автоматически. Анализ может занять много времени — например, для ckBTC на его выполнение потребовалось более 20 часов. Наконец, еще одним преимуществом TLA является то, что моделирование и анализ можно выполнять на этапе проектирования до реализации кода, что помогает избежать крупных рефакторингов из-за ошибок проектирования в дальнейшем.

Где TLA+ бесполезен

С другой стороны, TLA+ менее полезен для сложных последовательных программ, в отличие от параллельных программ, а также он плохо справляется со сложными криптографическими протоколами, для которых есть другие инструменты (например, Tamarin), которые более полезны.

Наконец, существует проблема синхронизации модели TLA+ и фактической реализации, поскольку код реализации со временем развивается и может перестать соответствовать модели, что может быть трудно уловить без поддержки инструментов.

На самом деле, наша команда исследований и разработок пытается решить эту проблему — надеюсь, мы скоро сможем поделиться с вами некоторыми инструментами!

Я надеюсь, что этот обзор пробудил у вас интерес к использованию TLA+ для ваших собственных важных смарт-контрактов, и если это так, следите за обновлениями — скоро появится следующий пост с более подробным руководством о том, как использовать TLA+ для смарт-контрактов. и Attached — это реальная модель TLA+, разработанная нашей командой исследований и разработок.

IC-контент, который вам важен

Технологический прогресс | Информация о проекте Глобальные события |

Собирайте и следите за IC Binance Channel

Будьте в курсе самой последней информации