Microsoft выпускает инструмент для проверки смарт-контрактов Ethereum

В подтверждение своих намерений помочь развитию блокчейнов Microsoft выпустила новый инструмент под названием VeriSol, который проверяет и анализирует умные контракты, разработанные на языке программирования Solidity. 3 июня команда Microsoft Azure Blockchain опубликовала сообщение в блоге под названием «Исследователи работают над обеспечением интеллектуальных контрактов Azure Blockchain с формальной проверкой».
With new open-source formal verification tool VeriSol, Microsoft researchers are helping developers author safer and higher-quality smart contracts in @Azure Blockchain offerings: https://t.co/dzL84z1p3F
— Microsoft Research (@MSFTResearch) June 3, 2019
В сообщении блога говорится, что команда служб разработки блокчейнов в Azure серьезно отнеслась к потенциальным проблемам безопасности в смарт-контрактах и с этой целью разработала формальный инструмент проверки, который проверяет правильность программ или, другими словами,
“Разработчики могут начать выражать желаемое поведение умных контрактов, написанных на подмножестве популярного языка Solidity, а затем использовать математическую логику для строгой проверки этих спецификаций на соответствие реализации”.
[irp]
Главный исследователь Microsoft, Шувенду Лахири, сказал, что инструмент поможет устранить затраты ресурсов, связанные с проверкой,
“Использование формальной верификации в производственном программном обеспечении требует от специалистов, обладающих высокой степенью специализации формальных языков и инструментов, что обуславливает огромные затраты на обучение для команд разработчиков и зачастую несколько человеко-лет инвестиций, чтобы разбить сложную задачу верификации на те, которые могут быть разряжены механически с помощью инструментов проверки.”
Группа заявляет, что этот инструмент уже был успешно применен к смарт-контрактам в Azure. В одном случае этот инструмент использовался для формализации и проверки спецификаций интеллектуальных контрактов, которые управляют консорциумом Ethereum в Azure и службе Azure Blockchain.
Microsoft увлечена блокчейном
Microsoft проявляет большой интерес к пространству блокчейнов. Помимо запуска рабочей среды Azure, он также выпустил набор инструментов для разработчиков Azure для миллионов разработчиков Ethereum и создает децентрализованную службу идентификации ION.
Исследовательская группа также заявила, что VeriSol не является концом ее планов блокчейна — она также направлена на обеспечение формальной проверки для основной разработки умных контрактов посредством открытого сотрудничества.
“По словам Лахири, мы планируем расширить возможности не только разработчиков и клиентов Azure Blockchain, но и внести вклад в создание более полной экосистемы блокчейнов, которая поможет людям полностью реализовать потенциал технологии, не подвергаясь дорогостоящим ошибкам в интеллектуальных контрактах.”