Microsoft объявляет о проверке смарт-контракта Ethereum VeriSol

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

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

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

Формальная проверка смарт-контракта Ethereum обеспечит безопасность.

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

Этот процесс обычно занимает много времени и требует специализированных разработчиков, поэтому он зарезервирован только для наиболее важных частей продукта. Смарт-контракты имеют определенные свойства, которые облегчают их формальную проверку. Как объясняет главный научный сотрудник Microsoft Шувенду Лахири (Shuvendu Lahiri) :
«Небольшое количество кода и семантика последовательного выполнения смарт-контрактов делают их пригодными для масштабируемой проверки, а открытая операционная среда существенно снижает необходимость вручную моделировать среду, в которой работает смарт-контракт».

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

Solidity является наиболее популярным языком для программирования смарт-контрактов в сети  Ethereum, поэтому автоматизированный инструмент формальной проверки должен обеспечить разработчикам безопасность их приложений.