Технологический гигант решил помочь Виталику Бутерину с исправлением ошибок в его детище. Новая формальная схема проверки смарт-контрактов поможет бороться с неточностями языка Solidity.
Название VeriSol намекает на сочетание слов «Verified» и «Solidity». Технология позволяет разработчикам писать спецификации к контрактам используя язык-посредник, который затем может быть протестирован с использованием машинерии математической логики.
Команда VeriSol использует подтверждающий софт чтобы формализовать и проверить спецификации контрактов, которые контролируют членов консорциума в Ethereum, работающем на базе Azure и Azure Blockchain Service.
Что собой представляет VeriSol на данный момент?
Сейчас система является прототипом, однако команда нацелена на покрытие большинства методов использования корпоративных приложений смарт контрактов. Схема является продуктом партнерства между Microsoft Azure Blockchain и команд из отдела «Microsoft Research».
Формальная проверка смарт-контрактов дает больше безопасности. В течение долгого времени, безопасность таких контрактов оставляла желать лучшего. Криптовалютное воровство и взломы сервисов, бирж, онлайн и оффлайн кошельков с кражами миллионов долларов в токенах ETH – тому подтверждение.
Процесс в общем требует специализированных разработчиков и длительные периоды времени на исполнение, так что сила зарезервирована только для самых важных частей продукта. В смарт-контрактах есть свойства, позволяющие проще проводить формальную верификацию. Шувенду Лахири из Microsoft поясняет:
«Маленький размер кода и семантика периодичного исполнения в смарт-контрактах делает их податливыми к масштабируемой верификации, а открытое операционное пространство значительно сокращает необходимость в ручном моделировании окружения, в котором работает контракт».
Компания будет предлагать Kit и Workbench – продукты для разработки кода блокчейнов при помощи имеющихся шаблонов, с интеграцией в сервисы Azure вроде управления ключами или идентификационными данными. Инструменты формальной верификации вроде VeriSol позволяют разработчикам проверять свою работу и лучше находить ошибки.
Почему понадобился подобный инструмент?
Язык программирования Solidity, на котором написан Ethereum – это уникальное явление в мире языков программирова. Он не только был придумал всего лишь несколько лет назад, так еще и имеет свойство, из-за которого была взломана добрая половина всех смарт-контрактов Ethereum. Это – многовариантность исполнения.
Дело в том, что компьютерный код не всегда работает согласно четкой, двоичной логике. Если бы код всегда работал так, как описывают его работу разработчики, то неполадок не существовало бы. Но многие устройства упорно продолжают «глючить» – ваш телефон, планшет, компьютер, и не важно, Linux, Mac или Windows, неисправности есть везде. Как это происходит, неужели техника «живая» и может думать?
Нет, просто срабатывает многовариативность. Смарт-контракты Ethereum «глючат» точно так, как ваш телефон, который, то показывает виджет «Часы», то не показывает, как будто «по собственному желанию». Язык Solidity – один из немногих, где многовариантность исполнения кода развита и поддерживается всеми силами. Вы можете создать смарт-контракт на этом языке, думать, что он делает одно, а потом окажется, что контракт умеет делать еще что-то другое. При чем, если вы в таком контракте случайно потеряете деньги, то их уже не вернуть, так что игры с необработанным смарт-контрактом опасны.
Именно для того, чтобы как следует протестировать все варианты исполнения кода конкретного контракта, и представлен инструмент VeriSol. Сможет ли он справляться с поставленной задачей – покажет время. Однако не стоит считать, что этот инструмент полностью решит проблемы сети.
Фото: shutterstock.com
