Внедрение на Ethereum формата верификации с целью обезопасить умные контракты
10.10.2016
В сфере блокчейн в последнее время стало часто встречаться слово «формат верификации». Данное словосочетание, которое, к слову, употребляется при описании математического инструментария для проверки кода программ, до недавнего времени использовалось не столь часто. Но если учесть дискуссии, которые вели разработчики платформы Ethereum на конференции Devcon-2, состоявшейся на днях, можно говорить о том, что вопрос, касающийся безопасности блокчейн, включая интеллектуальные контракты, ставится во главу угла.
На упомянутой конференции много говорилось и о том, что разработчикам Ethereum следует предоставить широкое поле для деятельности, нежели их существующие на сегодняшний день полномочия. Например, была предложена идея, «обязанность» которой – внушить к Эфириуму доверие посредством экспериментально приведенного доказательства его доли в сети blockchain.
Столь оригинальные мысли вовсе не были неожиданностью, если принять во внимание летний крах DAO, который оправился после случившегося и сейчас стал крупнейшим умным проектом, благодаря которому функционирует система децентрализованного финансирования разработок.
Упомянутый формат верификации вовсе не так сложен, каким кажется с первого взгляда. Он объясняется достаточно просто и относительно Ethereum выглядит таким образом: Специалисты пишут программы умных контрактов на новом языке Solidity. После этого прописанный код конвертируется в байт, чтобы его могла использовать EVM, то есть виртуальная машина платформы Эфириум. Данный байт распространяется среди сетевых узлов для соответствующего выполнения. И тут формат верификации предлагает объективные гарантии того, что инструкции, полученные разными сетевыми элементами, будут выполнены именно так, как этого ожидают пользователи.
Грант Пассмор, один из создателей Aesthetic Integration и первых бизнесменов, приложивших немало усилий для развития данного направления, на мероприятии Devcon-2 прорекламировал технологию Imandra Contracts, призванную проверять интеллектуальные контракты в сети блокчейн посредством верификационного формата.
Пассмор заявил, что Эфириум способен стать «райским местом» для такого новшества, и рассказал, какую помощь данная инновация окажет всему сообществу, если коду будут доверены формальные проверки.
Сообщество Ethereum, по словам предпринимателя, попало в нестандартную ситуацию, поскольку после проблем с DAO стала очевидной необходимость строгого и внимательного подхода к интеллектуальным контрактам. Прописывать их по аналогии с веб-приложениями нельзя.
Другие докладчики, в частности, Филипп Дэйлен, прибывший из Корнуэлла, рассуждали на эту тему намного глобальнее. Например, Дэйлен отметил, что Эфириум с помощью формальной проверки сумеет решить все важные задачи, что перед ним поставлены. По словам Дэйлена, он планирует использовать платформу для установления стандартов, чтобы продемонстрировать всем, как все это должно быть создано.
Не зря автор Solidity Кристиан Рейтвейсснер посчитал, что интеграция формата верификации целесообразна, поскольку это позволит специалистам Эфириума находить ошибки намного быстрее и качественнее.
Разработчик сообщил, что создатели смарт-контрактов все равно станут пользоваться форматом верификации, в частности тогда, когда в системах будут возникать ошибки. По словам Кристиана, такая ситуация возможна, а инструментарий для форматной верификации автоматически найдет проблему.
Райтвейсснер утверждает, что разработчики языка Solidity провели исследование и изучили возможности использования форматной верификации в рабочем процессе.
Проект Ethereum Foundation вовлек в свою работу Йоичи Хирая, крупного эксперта из компании FireEye. Эта фирма занимается предоставлением перечня услуг, связанных с компьютерной безопасностью. Хирая также выступил на мероприятии и сообщил о своем разочаровании в поставленной перед ним задаче, поскольку та для его фирмы слишком широка и требует неимоверных трудозатрат.
По словам Пассмора, теперь можно понять, что произошло с DAO, и постараться предотвратить подобные инциденты в будущем, однако, уверенности в том, что это получится, пока нет. И все же верификационный формат, несмотря на свою новизну, имеет все шансы получить распространение ввиду своей очевидной необходимости.
Назад
На упомянутой конференции много говорилось и о том, что разработчикам Ethereum следует предоставить широкое поле для деятельности, нежели их существующие на сегодняшний день полномочия. Например, была предложена идея, «обязанность» которой – внушить к Эфириуму доверие посредством экспериментально приведенного доказательства его доли в сети blockchain.
Столь оригинальные мысли вовсе не были неожиданностью, если принять во внимание летний крах DAO, который оправился после случившегося и сейчас стал крупнейшим умным проектом, благодаря которому функционирует система децентрализованного финансирования разработок.
Упомянутый формат верификации вовсе не так сложен, каким кажется с первого взгляда. Он объясняется достаточно просто и относительно Ethereum выглядит таким образом: Специалисты пишут программы умных контрактов на новом языке Solidity. После этого прописанный код конвертируется в байт, чтобы его могла использовать EVM, то есть виртуальная машина платформы Эфириум. Данный байт распространяется среди сетевых узлов для соответствующего выполнения. И тут формат верификации предлагает объективные гарантии того, что инструкции, полученные разными сетевыми элементами, будут выполнены именно так, как этого ожидают пользователи.
Грант Пассмор, один из создателей Aesthetic Integration и первых бизнесменов, приложивших немало усилий для развития данного направления, на мероприятии Devcon-2 прорекламировал технологию Imandra Contracts, призванную проверять интеллектуальные контракты в сети блокчейн посредством верификационного формата.
Пассмор заявил, что Эфириум способен стать «райским местом» для такого новшества, и рассказал, какую помощь данная инновация окажет всему сообществу, если коду будут доверены формальные проверки.
Сообщество Ethereum, по словам предпринимателя, попало в нестандартную ситуацию, поскольку после проблем с DAO стала очевидной необходимость строгого и внимательного подхода к интеллектуальным контрактам. Прописывать их по аналогии с веб-приложениями нельзя.
Другие докладчики, в частности, Филипп Дэйлен, прибывший из Корнуэлла, рассуждали на эту тему намного глобальнее. Например, Дэйлен отметил, что Эфириум с помощью формальной проверки сумеет решить все важные задачи, что перед ним поставлены. По словам Дэйлена, он планирует использовать платформу для установления стандартов, чтобы продемонстрировать всем, как все это должно быть создано.
Тренажер для обучения
Многие финансовые компании проявляли интерес к умным контрактам и изучали их. Это дает право говорить о связи формата верификации с программным языком Solidity. Данный язык, который был создан для Эфириума, нередко подвергался критике за непроверенный функционал и сложности, возникающие при написании на нем кода. Как правило, это издержки новизны. Указанные трудности лишь усугубились из-за краха DAO, проблем с языковым компилятором, а также по причине отсутствия соответствующих библиотек. А между тем, данные разработки тщательно анализировались известными создателями языка Solidity.Не зря автор Solidity Кристиан Рейтвейсснер посчитал, что интеграция формата верификации целесообразна, поскольку это позволит специалистам Эфириума находить ошибки намного быстрее и качественнее.
Разработчик сообщил, что создатели смарт-контрактов все равно станут пользоваться форматом верификации, в частности тогда, когда в системах будут возникать ошибки. По словам Кристиана, такая ситуация возможна, а инструментарий для форматной верификации автоматически найдет проблему.
Райтвейсснер утверждает, что разработчики языка Solidity провели исследование и изучили возможности использования форматной верификации в рабочем процессе.
Полигон для испытаний
Платформа Эфириум и формат верификации постоянно упоминались на конференции. В частности, Пассмор заявил, что Aesthetic Integration уже пару лет проводит работы по интегрированию верификационного формата, и в настоящее время он уже используется. Правда, только в ряде областей со своей уникальной спецификой, таких как организация трейдерских пулов. А в отношении умных контрактов, Пассмор высказал предположение, что в пуле Эфириума инновация будет принята скорее, нежели в прочих сообществах. По мнению Пассмора, это, вероятнее всего, поскольку множество финансовых организаций, с которыми приходилось сотрудничать Aesthetic Integration, выражали заинтересованность платформой Эфириум, однако, беспокоились о качестве проверки интеллектуальных контрактов.Проект Ethereum Foundation вовлек в свою работу Йоичи Хирая, крупного эксперта из компании FireEye. Эта фирма занимается предоставлением перечня услуг, связанных с компьютерной безопасностью. Хирая также выступил на мероприятии и сообщил о своем разочаровании в поставленной перед ним задаче, поскольку та для его фирмы слишком широка и требует неимоверных трудозатрат.
До реализации идеи еще далеко
Энтузиазм, который охватил всех приверженцев идеи верификации формата, к сожалению, не приблизит реализацию данной концепции. Слишком многое еще предстоит сделать, чтобы воплотить ее в реальность. Алекс Берегази, специалист, занимающийся обновлениями технологии EVM, считает, что для этого придется создать огромное количество кодов программ. Впрочем, Пассмор также отметил, что на данном этапе трудно гарантировать, что проблемы, с которыми в свое время столкнулся DAO, не повторятся.По словам Пассмора, теперь можно понять, что произошло с DAO, и постараться предотвратить подобные инциденты в будущем, однако, уверенности в том, что это получится, пока нет. И все же верификационный формат, несмотря на свою новизну, имеет все шансы получить распространение ввиду своей очевидной необходимости.
Назад