В данной статье мы делаем поверхностный обзор подходов, обеспечивающих безопасность смарт-контрактов. Разбираем устройство и принцип работы инструмента формальной верификации SMTChecker (встроен в компилятор solc), а также верифицируем с его помощью учебные контракты: находим баги и уязвимости, и доказываем их отсутствие. Читать далее
Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования. Формальная верификация — это доказательство с использованием…
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье мы продолжим обсуждать методы и инструменты формальной верификации смарт-контрактов и их практическое применение для предотвращения уязвимостей. Мы подробно поговорим о методе дедуктивной верификации, а точнее, о фреймворке для тестирования и верификации смарт-контрактов — ConCert. Под кат
Больше года я работал над книгой «Создание смарт-контрактов Solidity для блокчейна Ethereum. Практическое руководство», и вот теперь эта работа завершена, а книга издана и доступна в Литресе. Надеюсь, моя книга поможет быстро приступить к созданию смарт-контактов Solidity и распределенных