21 июня: К вопросу построения инструмента формальной верификации смарт-контрактов

Шишкин Евгений Сергеевич

Шишкин Евгений Сергеевич

Шишкин Евгений Сергеевич — ведущий исследователь, научный отдел компании ИнфоТеКС. Научные интересы: дедуктивные методы формальной верификации, методы формальной спецификации, построение специализированных доменных логик, спецификация и верификация распределенных и реагирующих систем, функциональное программирование.

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

На семинаре планируется рассмотреть задачу построения надежных смарт-контрактов с использованием сплава различных технологий формальной верификации. Под надежностью понимается отсутствие функциональных и нефункциональных ошибок в программе смарт-контракта. Мы не стремимся дать готовое решение, а, скорее, сформулировать проблему и побудить сообщество к её совместному решению.

В основном докладе планируется затронуть такие темы:

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

Помимо доклада планируется провести дискуссию со специалистами ИСП РАН и, возможно, приглашенными экспертами по программированию и аудиту смарт-контрактов для выработки общего взгляда на проблему и пути решения.

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

Доклад состоится 21 июня 2018 года в 17:00 в Институте системного программирования РАН имени В.П. Иванникова. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

*

Можно использовать следующие HTML-теги и атрибуты: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>