Формальная верификация смарт-контрактов во фреймворке ConCert
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье мы продолжим обсуждать методы и инструменты формальной верификации смарт-контрактов и их практическое применение для предотвращения уязвимостей. Мы подробно поговорим...
Что такое формальная верификация
Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования. Формальная верификация — это доказательство с использованием математических методов корректности...
Формальная верификация в информационной безопасности. Как пройти сертификацию во ФСТЭК
В связи с выходом приказа ФСТЭК России № 76 от 02.06.2020 «Об утверждении Требований по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий» создание и доказательство безопасности формальных...
Создание системы формальной верификации смарт-контрактов. Часть 1: символьная виртуальная машина на php и python
Формальная верификация подобна атомной бомбе в мире информационной безопасности: это средство, которое позволяет найти в программе все баги либо же доказать, что их нет. Разумеется, со своими преимуществами, недостатками и ограничениями. Раньше я описывал основы формальной верификации на примере...
[Из песочницы] Формальная верификация на примере задачи о волке, козе и капусте
На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров. Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую...