В рамках формальной верификации Ethereum стремится к определенности смарт-контрактов

Осенью в мире блокчейна появится новое модное словечко — формальная верификация.

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

Как свидетельствуют многочисленные выступления, посвященные этой теме на Devcon2, идея о том, что новые гарантии могут быть даны программистам Ethereum , широко поддерживается сообществом разработчиков. Эта концепция уже предлагается как способ внушить доверие всему, от самого протокола Ethereum до его экспериментального блокчейна Proof-of-Stake.

То, что это произошло, возможно, неудивительно, учитывая внезапный крах The DAO этим летом — крупнейшего на сегодняшний день смарт-контракта, запущенного на децентрализованной платформе разработки приложений.

Но покаофициальная проверка Это может показаться сложным, но эту концепцию, пожалуй, можно кратко изложить применительно к Ethereum : в настоящее время программисты используют совершенно новый язык (Solidity) для написания смарт-контрактов, записывая команды, которые затем транслируются в байт-код для использования виртуальной машиной Ethereum (EVM) и распространяются по узлам сети для выполнения.

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

Грант Пассмор, соучредитель Aesthetic Integration, — ONE из предпринимателей, который видит возможность помочь в этом начинании, используя Devcon2 для запуска Imandra Contracts, официальной платформы проверки смарт-контрактов на основе блокчейна.

На мероприятии он высказал идею о том, что Ethereum может стать «раем» для формальной верификации (широко цитируемая точка соприкосновения в переговорах), учитывая цели его сообщества и значительную ответственность, которую оно хочет возложить на код.

Пассмор сказал CoinDesk:

«Сообщество Ethereum находится в уникальном положении, поскольку после The DAO мы понимаем, что необходима строгая инженерия. T подходить к написанию смарт-контракта как к веб-приложению».

В других местах такие докладчики, как Филип Дайан из Корнелла, говорили об интересе к методологии в более широком плане, сообщая аудитории, что, по его мнению, формальная верификация может помочь Ethereum решить ключевые проблемы.

«Это станет ONE частью общей картины. Я с нетерпением жду возможности использовать Ethereum , чтобы задать стандарт и показать людям, как это делается», — сказал он.

Учебные колеса

Учитывая недавнее внимание, которое финансовые компании уделяют изучениюязыки смарт-контрактов, возможно, именно концепция применения формальной верификации к Solidity была наиболее частой темой обсуждения.

Разработанный для платформы Ethereum , Solidity подвергся критике за то, что он в значительной степени не протестирован и сложен в написании, в основном потому, что он настолько новый. Такие проблемы, возможно, были усилены из-за проблемыс компилятором языка, отсутствием публичных библиотек и крахом DAO, который был проверен видными членами сообщества разработчиков.

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

Райтвайсснер рассказал CoinDesk , что разработчики смарт-контрактов ONE смогут использовать формальные инструменты проверки, например, чтобы определить, есть ли непредвиденные ошибки в их работе. Он указал, что такой инструмент можно использовать для определения того, не превышает ли результат при сложении двух балансов поле, выделенное компилятором.

«Это может произойти, и формальный инструмент проверки автоматически это обнаружит. Вы можете обнаружить это на ранней стадии и отреагировать на это внутри смарт-контракта», — пояснил он.

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

Испытательный полигон

На конференции также активно обсуждалась тема о том, что Ethereum можно использовать для проверки того, как формальная верификация может применяться в Финансы в более широком смысле.

Например, Пассмор заявил, что Aesthetic Integration работает над применением формальной верификации в работе с финансовыми учреждениями с 2014 года, и что до сих пор клиенты стремились использовать ее в ограниченных областях, таких как темные пулы, где трейдерам требуется уверенность в честности.

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

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

Развитие формальной верификации также привлекло Ёити Хираи по схожим причинам. Инженер по формальной верификации, который сейчас работает в Ethereum Foundation, его интерес к этой концепции начался как исследователь и на его предыдущей работе в компании FireEye, лидере по кибербезопасности.

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

«Я нашел Ethereum, увидел EVM, желтую книгу, спецификацию, там было всего 32 страницы, и я подумал, что смогу перевести ее и написать доказательства о смарт-контрактах», — сказал он.

Ethereum, напротив, предлагает то, что он назвал «меньшей спецификацией» и «решаемой проблемой» для инженеров по определению того, как лучше всего перевести Solidity в байт-код.

«Я полагаю, что появится еще много исследователей, занимающихся формальной верификацией», — сказал он.

Нет серебряной пули

Тем не менее, несмотря на энтузиазм, предпринимаются шаги, чтобы предостеречь от того, насколько далеко может зайти формальная верификация. Разработчик Алекс Берегсаси, работающий над обновлениями EVM, говорил о необходимости набора решений, которые помогут разработчикам гарантировать, что код смарт-контракта работает так, как задумано.

Пассмор также отметил, что трудно сказать, могла ли его новая система обнаружить проблемы с DAO, поскольку формальные инструменты проверки по-прежнему требуют Human участия.

«Вы можете закодировать проблемы, которые возникли с The DAO, и проверить, T ли их у вас, но вы должны знать, на что обращать внимание», — пояснил он.

Ограничения были признаны Райтвайсснером и Пассмором, которые предостерегли разработчиков от того, чтобы они считали формальную проверку «волшебной палочкой».

Однако Райтвайсснер считает, что методология будет ONE по мере ее более широкого использования, поскольку разработчики постепенно будут совершенствоваться в выявлении проблем и создании репозиториев, в которых знания о распространенных проблемах могут быть доступны.

Пассмор полагает, что таким образом сообщество Ethereum успешно «проповедует» эту концепцию, что, по его мнению, в конечном итоге будет способствовать развитию исследований в области блокчейна.

Пассмор заключил:

«Хотя многие никогда с этим не сталкивались, формальная верификация — это то, что нам нужно. Это кривая обучения, но ее нужно принять, и это волнительно».

Изображения предоставлены Питом Риццо для CoinDesk