• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
ФИО студента
Название работы
Руководитель
Факультет
Программа
Оценка
Год защиты
Волков Григорий Дмитриевич
Реализация поддержки лемма-функций и абстрактных аксиоматик в Frama-C
2018
Дедуктивная верификация позволяет статически доказать соответствие программного кода его контрактной спецификации. Это значительно помогает в предотвращении логических ошибок в критических программных системах. В ИСП РАН для дедуктивной верификации модулей безопасности ядра Linux используется платформа статического анализа Frama-C с плагином AstraVer. Для улучшения эффективности работ по верификации таких крупных проектов, в данной работе представлены модификации инструмента Frama-C, расширяющие его возможности.



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

Для полноценного использования метода доказательства лемм в виде функций требуется расширить инструмент Frama-C поддержкой лемма-функций.

Также в дедуктивной верификации часто бывает нужно параметризовать (типами, логическими функциями / предикатами) набор логических утверждений. Это позволяет доказывать и использовать утверждения в логике высших порядков (утверждения, использующие кванторы на функции). Например, так можно определить набор свойств для абстракного (неопределенного) типа данных, а затем подставлять разные конкретные типы данных и получать для них тот же набор свойств.

Для поддержки этой возможности требуется расширить инструмент Frama-C поддержкой абстрактных аксиоматик (включения аксиоматик).

Данная работа описывает реализацию поддержки лемма-функций и абстрактных аксиоматик в инструменте верификации Frama-C.

Выпускные квалификационные работы (ВКР) в НИУ ВШЭ выполняют все студенты в соответствии с университетским Положением и Правилами, определенными каждой образовательной программой.

Аннотации всех ВКР в обязательном порядке публикуются в свободном доступе на корпоративном портале НИУ ВШЭ.

Полный текст ВКР размещается в свободном доступе на портале НИУ ВШЭ только при наличии согласия студента – автора (правообладателя) работы либо, в случае выполнения работы коллективом студентов, при наличии согласия всех соавторов (правообладателей) работы. ВКР после размещения на портале НИУ ВШЭ приобретает статус электронной публикации.

ВКР являются объектами авторских прав, на их использование распространяются ограничения, предусмотренные законодательством Российской Федерации об интеллектуальной собственности.

В случае использования ВКР, в том числе путем цитирования, указание имени автора и источника заимствования обязательно.

Расширенный поиск ВКР