Децентрализованные протоколы, такие как Bitcoin и Ethereum, позволяют надежно выполнять интеллектуальные контракты-компьютерные протоколы, которые регулируют обмен активами между пользователями.
Основополагающие протоколы, используемые для обновления (в которых определяется состояние каждого контракта) и гарантируется, что даже без доверенных посредников исполнение контрактов является правильным с точки зрения правил контракта. Однако может случиться так, что правила сами по себе не корректны в отношении поведения, ожидаемого пользователями. Действительно, все успешно проведенные до сих пор атаки на "умные" контракты, которые разграбили или заморозили миллионы долларов США в Этерее, используют некоторое несоответствие между намеченным и фактическим поведением контракта.
Для противодействия этих атак исследовательское сообщество недавно приступило к формализации "умных" контрактов и их защитных свойств, а также к разработке автоматизированных средств проверки на основе этих моделей. По сути, большинство исследований направлено на Ethereum, самую распространенную (и атакованную) платформу для "умных" контрактов. По этой причине защитные свойства рассматриваемых инструментов ориентированы на специфику Solidity, языка высокого уровня для "умных" контрактов в Ethereum. Например, некоторые шаблоны уязвимостей, проверенные этими инструментами, представляют собой, неправильно обработанные исключения, особая реализация которых в Solidity привела к атакам, подобно атакам в DAO.
Лишь немногие инструменты проверяют общие свойства безопасности "умных" контрактов, что было бы значимо и за пределами Ethereum. Среди этих работ проверяется ликвидность, которое удерживается, когда контракт допускает отслеживание того, где его баланс уменьшается (таким образом, средства, хранящиеся в контракте, не остаются замороженными). Это было сделано недавней атакой на Ethereum, которая заморозила ∼ 160M USD в рамках контракта, воспользовавшись ошибкой в библиотеке. Будучи способным классифицировать данный конкретный контракт как неликвидный, любой контракт, в котором противник может заблокировать часть средств и погасить их в более поздний момент, будет классифицироваться как ликвидный. Более сильные представления о ликвидности могут исключить такие небезопасные контракты, например, путем проверки того, что средства никогда не будут заморожены по всем возможным стратегиям противника. Изучение ликвидности в более общих условиях было бы важным по различным причинам.
Во-первых, учет противников позволил бы выявить больше проблем безопасности, чем те, которые проверяются существующими инструментами верификации.
Во-вторых, к грядущим технологиям блокчейн можно применить платформенно-диагностические понятия ликвидности,
В-третьих, изучение ликвидности в более простых условиях, чем Ethereum, может упростить задачу верификации, что невозможно в Turing-мощных языках типа поддерживаемых Ethereum.
Рассмотрим особый случай, когда контракты выражаются в формате BitML, DSL высокого уровня для "умных" контрактов, которые компилируются в Bitcoin. В таких условиях разрабатываем методику верификации ликвидности "умных" контрактов.
Можем суммировать наши основные вклады следующим образом:
1. Формализуем понятие ликвидности и иллюстрируем несколько значимых вариантов. Понятие ликвидности учитывается как контракт, так и стратегию, которой следует участник для выполнения контрактных действий. Примерно такая стратегия является ликвидной, если следовать ей, чтобы не допустить замораживания средств в рамках контракта, даже в присутствии противников.
2. Представляю вашему вниманию абстракцию семантики конечного состояния, а также звуковой и полной w.r.t. конкретной (бесконечно-состоятельной) семантики, приведенную в виде набора наблюдаемых контрактов.
3. Разрабатывается методика верификации ликвидности в BitML. Она позволяет определить, является ли стратегия ликвидной для данного контракта, а также синтезировать ликвидную стратегию, когда она существует.
Конечная государственная абстракция является универсальной: проверка ликвидности является лишь одним из возможных вариантов ее применения.
Изучаются вопросы безопасности, связанные с контрактами Ethereum smart. Несколько статей посвящены EVM, байт-коду языка, который является целью компиляции Solidity. Среди них представляет операционную семантику упрощенной версии EVM, а также разрабатывает Oyente, инструмент для выявления некоторых паттернов уязвимости EVM контрактов посредством символического исполнения.
Безопасность проверки шаблонов уязвимостей путем анализа графиков зависимостей, полученных из кода EVM. Как уже упоминалось выше, данный инструмент также касается той или иной формы ликвидности, которая, по сути, предполагает наличие сотрудничающего противника. EtherTrust представляет собой структуру для статической проверки контрактов EVM, которая может установить отсутствие уязвимостей. Этот инструмент основан на детальной формализации EVM, которая проверяется в соответствии с официальным набором тестов Ethereum.
В работе представлена исполняемая семантика EVM, указанная в K-фреймворке. Инструмент преобразует Solidity и EVM код в F∗ и использует свои инструменты проверки для обнаружения уязвимостей контрактов. Далее, инструмент проверяет эквивалентность между программой Solidity и предполагаемой компиляцией ее в EVM. Работа проверяет код EVM с помощью ассистента Isabelle/HOL, доказывая, что только его владелец может уменьшить остаток средств при обращении к конкретному контракту.
Умные контракты в Bitcoin имеют совершенно иной вид по сравнению с Ethereum, поскольку они обычно выражаются в виде криптографических протоколов, а не в виде программ. Несмотря на ограниченную экспрессивность скриптов в транзакциях Bitcoin, было предложено несколько видов контрактов на Bitcoin: от лотерей до общих многопартийных расчетов, от условных платежей и т.д. Все эти работы направлены на то, чтобы доказать надежность фиксированного контракта, в отличие от вышеупомянутых работ в Ethereum, где цель состоит в проверке произвольных контрактов. Насколько нам известно, только пара работ посвящена этой цели для Bitcoin.
Инструмент для анализа Bitcoin-скриптов, позволяющий определить, при каких условиях может быть погашена вложенная транзакция. Рабочие модели заключают контракты как временные автоматы, а затем используют Uppaal Model Checker для проверки их свойств.
Моделируемые контракты не могут быть напрямую переведены на Bitcoin, в то время как в нашем подходе мы можем использовать компилятор Bitcoin для перевода контрактов на стандартные транзакции Bitcoin. Отметим также, что рассматриваемые свойства являются специфическими для моделируемого контракта, в то время заинтересованные в проверке общих свойств контрактов, таких как ликвидность.
Благодаря этому, можно сделать вывод о том, что разработали теорию ликвидности для "умных" контрактов, а также методику верификации, которая является надежной и полной для контрактов, выраженных в BitML. Конечная государственная абстракция может применяться, помимо ликвидности, для верификации других свойств "умных" контрактов. Например, помогает решить, позволяет ли стратегия участнику всегда расторгать контракт в течение определенного срока.
Кроме того, можно сделать вывод о том, что контракт расторгается раньше определенного срока или сделать вывод о том, что он расторгается в кратчайшие сроки и т.д. Хотя теория сфокусирована на BitML, различные понятия ликвидности, которые предложили, могут быть применены к более выразительным языкам для "умных" контрактов, например, Solidity (язык высокого уровня, используемый в Ethereum).
Насколько известно, единственной проверенной до сих пор формой ликвидности в Ethereum является вариант "бесстратегический многопартийный", который требует только наличия кооперативной стратегии размораживания средств (это свойство анализируется, например, инструментом Securify). Поскольку контракты Ethereum являются мощными в Туринге, проверка их ликвидности невозможна надежным и полным образом, вместо этого, снижение экспрессивности BitML делает ликвидность распознаваемой в этой ситуации.