В своём блоге корпорация Microsoft анонсировала разработку открытой формальной схемы верификации смарт-контрактов эфириума на языке программирования Solidity.

Инструмент будет называться VeriSol (Verifier for Solidity) — он позволит разработчикам писать спецификации для смарт-контрактов, которые затем можно будет протестировать с использованием математической логики. В блоге Microsoft говорится, что команда VeriSol будет использовать верификатор для формальной проверки спецификаций смарт-контрактов, которыми руководствуются члены консорциума эфириума в Azure и Azure Blockchain Service.

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

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

VeriSol будет дополнять набор инструментов разработки Microsoft Azure Blockchain.

Напомним, что недавно Microsoft заявила о том, что будет использовать блокчейн биткоина для создания системы надежной цифровой идентификации, а в Microsoft Excel была добавлена опция с символом биткоина.