Внедрение формата верификации для безопасности умных контрактов на Эфириум

Внедрение формата верификации для безопасности умных контрактов на Эфириум



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



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



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



Хотя «формат верификации» может показаться чем-то сложным, его можно объяснить в нескольких словах — применительно к Эфириуму, это выглядит следующим образом. Разработчики используют новый язык программирования, solidity, для того, чтобы писать на нём умные контракты. Затем написанный код преобразуется в байт-код для использования виртуальной машиной Эфириума (ethereum virtual machine, EVM) и распространяется между узлами сети для выполнения. Здесь «формат верификации» становится более объективным способом гарантировать, что когда различные компоненты сети получат эти инструкции, то выполнят их таким образом, как задумано пользователями.



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



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



«Сообщество Эфириума находится в уникальном положении, так как после краха DAO мы поняли, что необходим строгий подход к умным контрактам. Мы не можем писать их так же, как и веб-приложения.», рассказал Пассмор



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



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



Учебный тренажёр



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



Язык Solidity, созданный для платформы Эфириум, часто критиковали за непроверенность функций и сложность написания на нём кода. В основном, это связано с тем, что язык очень новый. Вышеуказанные проблемы только усилились из-за проблем с компилятором языка, отсутствием публичных библиотек и крахом DAO, а ведь этот проект исследовался известными участниками сообщества разработчиков Solidity.



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



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



«Такое может произойти, и инструмент для верификации формата в данном случае автоматически это обнаружит.» объяснил он.



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



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



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



«Многие банки, с которыми мы работали, интересовались Эфириумом, но они волновались по поводу проверки корректности умных контрактов», сказал он.



Ethereum Foundation привлекли к задаче Йоичи Хирая, известного специалиста из фирмы FireEye, это компания, которая предоставляет услуги компьютерной безопасности. Выступая на конференции, Хирая расказал о том, что разочарован в задаче, которая описана для него слишком широко.



«Я изучил Эфириум, я изучил EVM, 32 страницы спецификаций pages и так и не понял, что же нужно делать», сказал он.



Эфириум, напротив, уверяет, что это «практически не проблема» для разработчиков, которые собираются наилучшим образом перевести написанный код на Solidity в байт код.



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



Это не серебряная пуля



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



«Мы можем теперь узнать, что случилось с DAO, и сделать, чтобы такого больше не было, но мы также должны смотреть вперёд», объяснил он.



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



«Даже при том, что многие никогда не имели с этим дела, формат верификации — то, в чём мы действительно нуждаемся. Пока мы только учимся, но это не только необходимо, но ещё и интересно», сделал вывод Пассмор



Источник