Технологические компании и университеты объединяют усилия во имя улучшения безопасности умных контрактов

Microsoft-harvard-smart-contracts-1024x512-08-25-2016

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

Эфириум-сообщество по-прежнему лихорадит от атаки на ДАО около двух месяцев назад.

Атака была проведена через содержащиеся уязвимости в умных контрактах. Это также напомнило всем нам, что безопасность должна быть приоритетом номер один.

Исследователям из Майкрософт, Гарвардского университета и Inra (французского национального научно-исследовательского института) потребовалось время, чтобы проанализировать язык и процесс верификации умных контрактов. Группа ученых опубликовала свои результаты в техническом документе.

В статье говориться о том, что еще очень многое предстоит сделать в области написания умных контрактов. Оказалось, что далеко не все выкладывают исходный код контракта на Solidity, что делает доступным для исследования лишь код контракта уже на Виртуальной Машине Эфириума. По результатам проведенных исследований исходный код на Solidity есть лишь у 396 из 112 802 контрактов доступных на сайте etherscan.io.

«Мы смогли преобразовывать и проверить соответствие типов в коде 46 контрактов из 396, собранных с сайта https://etherscan.io. Из них лишь немногие оказались надежными. Это явный признак того, что широкомасштабный анализ опубликованных контрактов, вероятнее всего, выявит часто встречающиеся уязвимости; мы оставим такой анализ на будущее», — говорится в докладе.

Для обеспечения правильного преобразования и верификации между обоими языками программирования в документе представлена рабочая среда F*- «функциональный язык программирования, нацеленный на проверку правильности программы».

Данное решение предоставит конкретные инструменты для декомпиляции байт-кода EVM (переименован в EVM*) и анализа Solidity (Solidity*). Эти инструменты предлагают три различных метода верификации:

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

 2. В случае с кодом EVM, мы можем использовать EVM*, чтобы декомпилировать его и проанализировать низкоуровневые свойства, такие как ограничения на газ, расходуемый на запросы (вызовы).

3. В случае, когда есть программа на Solidity и предположительно функционально эквивалентный байт-код EVM, мы можем проверить их эквивалентность, преобразовав каждый в F*. Таким образом, мы можем проверить правильность вывода компилятора Solidity в каждом конкретном случае с использованием реляционных рассуждений.

Это демонстрирует ориентированность методов на обеспечение самой безопасной и достоверной технологии.

Источник: ethnews Автор: Даниэль Миган



Рубрики:DAO, DApps, Анализ, Теория, Ethereum, смарт-контракты, эфир

Метки: ,

1 reply

Trackbacks

  1. Драма с хард-форком — возможности для ETC — EthereumClassic

Добавить комментарий

Заполните поля или щелкните по значку, чтобы оставить свой комментарий:

Логотип WordPress.com

Для комментария используется ваша учётная запись WordPress.com. Выход / Изменить )

Фотография Twitter

Для комментария используется ваша учётная запись Twitter. Выход / Изменить )

Фотография Facebook

Для комментария используется ваша учётная запись Facebook. Выход / Изменить )

Google+ photo

Для комментария используется ваша учётная запись Google+. Выход / Изменить )

Connecting to %s