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

[vaysar]

Microsoft объявила о разработке формальной схемы проверки подлинности контракта  Ethereum с открытым исходным кодом для языка программирования Solidity .

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

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

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

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

Этот процесс обычно требует специализированных разработчиков и длительных периодов времени, поэтому он предназначен только для наиболее важных частей продукта. Умные контракты имеют определенные свойства, которые облегчают их формальную проверку. Как объясняет главный научный сотрудник Microsoft Шувенду Лахири,

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

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

Это предоставляет разработчикам более эффективный путь к производству. Солидность является наиболее популярным языком для программирования умных контрактов в Ethereum, поэтому автоматизированный инструмент формальной проверки должен упростить разработчикам безопасность их приложений.
Источник: https://cryptoslate.com/microsoft-verisol-smart-contract-verification-ethereum/