Microsoft выпускает официальный инструмент проверки с открытым исходным кодом для смарт-контрактов Solidity

За время своего существования блокчейн, с защитой от несанкционированного доступа и технологией распределенного регистра, уже вызвал много шума и рассматривается как пробивной, влияющий на подходы в таких разнообразных областях, как финансовые услуги, цепочки поставок и управление. Сказать, что его будущее ярко, может быть преуменьшением. По словам Gartner, технология позволит увеличить добавленную стоимость бизнеса до 360 миллиардов долларов к 2026 году.

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

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

Группа Microsoft Azure Blockchain, которая предоставляет продукты и услуги для создания, развертывания и управления комплексными приложениями на основе цепочек для корпоративных клиентов, серьезно относится к этим угрозам. Смарт-контракты играют неотъемлемую роль в их блокчейн-предложениях — от администрирования управления членами консорциума в службе Azure Blockchain до реализации проверенных решений с помощью инструментальной среды Azure Blockchain. Группа также предлагает комплект разработки Azure Blockchain для быстрого развертывания смарт-контрактов из кода Visual Studio, Logic Apps и Microsoft Flow.
С целью укрепления смарт-контрактов в Azure Blockchain команда нашла партнера среди исследователей в Microsoft Research, работающих над передовыми методами обеспечения правильности программных продуктов. Результатом сотрудничества стал VeriSol, совершенно новый инструмент формальной проверки с открытым исходным кодом, разработанный исследователями. С VeriSol — сокращенно от Verifier for Solidity — разработчики могут начать выражать желаемое поведение смарт-контрактов, написанных на подмножестве популярного языка Solidity, а затем использовать механизм математической логики для строгой проверки этих спецификаций на соответствие реализации. Недавно он был включен в непрерывный интеграционный конвейер Azure Blockchain для разработки смарт-контрактов.

«VeriSol позволяет нам выполнять итерации быстрее благодаря автоматической и непрерывной проверке, а также позволяет быстрее обнаруживать ошибки, не беспокоясь о возможном влиянии на клиентов», — говорит Коди Борн (Cody Born), старший инженер-программист в группе Azure Blockchain.

Формальная проверка и смарт-контракты — идеальная пара

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

«Использование формальной верификации для производственного программного обеспечения требует от специалистов, обладающих высокой степенью специализации, формальных языков и инструментов, что обуславливает огромные затраты на обучение групп разработчиков и зачастую инвестиции в несколько человеко-лет, чтобы разбить сложную задачу верификации на те, которые могут механически разряжаться с помощью инструментов проверки», — объясняет главный исследователь Microsoft Шувенду Лахири, один из нескольких исследователей VeriSol. «Такие инвестиции ограничивают использование и успех формальной проверки очень небольшим количеством критически важных для безопасности аппаратных и программных компонентов».

Но смарт-контракты обладают рядом характеристик, которые делают их отличным кандидатом для автоматической формальной проверки для основных разработчиков смарт-контрактов.

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

Итак, Лахири, старший научный сотрудник Microsoft и эксперт по безопасности Шуо Чен, и техасский университет в Остине Юэпенг Ван, стажер Microsoft на момент работы, и приглашенный исследователь Исил Диллиг отправились в путешествие летом 2018 года, чтобы помочь Azure Blockchain — и, в конечном счете, его клиентам — создать более надежные и качественные смарт-контракты.

С VeriSol Борн и его коллеги-разработчики, в том числе Microsoft Software Engineer Xinxing Liu, могут начать определять и доказывать безопасность своей работы способами, которые раньше были невозможны. По словам Борна, более традиционное тестирование опирается на способность разработчиков точно предвидеть, как будет использоваться продукт. Это упражнение включает в себя упущение из рассмотрения некоторых ключевых случаев, поскольку люди могут думать только о стольких различных логических тестовых случаях. Но формальная проверка автоматически определяет различные способы, которыми код может потенциально нарушить данный инвариант, включая те случаи, которые разработчики не могут предсказать.

Смарт-контракты в Azure Blockchain

Даже в своей зарождающейся жизни VeriSol применялся к разнообразным смарт-контрактам в экосистеме Azure Blockchain.

В одном приложении группа VeriSol использовала верификатор для формализации и проверки спецификаций смарт-контрактов, которыми руководствуются члены консорциума в Ethereum на Azure и Azure Blockchain Service. Смарт-контракты по управлению предназначены для эффективного управления членством в условиях консорциума, где, в отличие от общедоступных блокчейнов, регистр ограничен группой участников, которые осведомлены о личности других участников. Формальная проверка таких контрактов на управление может помочь обеспечить управление членством — например, как члены принимаются и исключаются, и как они голосуют по предложениям и другим вопросам, например, — осуществляется так, как Microsoft указала для своих клиентов.

В другом исследовании группа применила VeriSol к смарт-контрактам, реализующим проверенные на практике приложения для рабочих процессов в Azure Blockchain Workbench. Приложение рабочего процесса состоит из высокоуровневой политики рабочего процесса, описываемой как конечный автомат, где переходы основаны на контроле доступа на основе ролей, и смарт-контракта Solidity, который реализует конечный автомат вместе с бизнес-логикой в ​​блокчейне. По словам Лахири, для обеспечения надежности и безопасности приложения крайне важно, чтобы программа Solidity правильно реализовала политику рабочих процессов. VeriSol использовался для проверки «семантического соответствия» таких приложений, то есть того, что конечные автоматы, реализованные в смарт-контракте и указанные в политике рабочего процесса, никогда не синхронизируются во время развертывания.

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

Попутно VeriSol автоматически выявлял тонкие ошибки, которые были исправлены в процессе разработки, и помогал выполнять полную проверку правильности большинства свойств и инвариантов с высоким уровнем автоматизации.

Стоя на плече гигантов

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

VeriSol основан на десятилетии работы по проверке, уже предпринятой Microsoft и ее исследователями в рамках большей приверженности компании безопасности, удобству для пользователей и высококачественным, современным продуктам и услугам. Эта работа включает в себя такие компоненты проверки, как Z3, Corral и Boogie. Эти компоненты, все с открытым исходным кодом, представляют собой проверенные методы, без которых VeriSol был бы невозможен.

Однако, этому путешествию еще далеко до завершения.

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

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

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

Перевод материала: https://www.microsoft.com/en-us/research/blog/researchers-work-to-secure-azure-blockchain-smart-contracts-with-formal-verification/?ocid=msr_blog_verisol_tw