Инструментальная поддержка процесса дедуктивной верификации модулей ядра Linux.

Авторы

Денис Ефремов, Никита Комаров

Аннотация

Ошибки в критически важных системах могут быть дорогими. Если такие системы должны обеспечить конфиденциальность при работе с критически важными данными, такими как государственная тайна или частные производственные секреты, стоимость ошибки может с трудом поддаваться оценке. Чтобы убедиться в отсутствии ошибок для таких систем, следует использовать методы формальной верификации. В статье рассматривается формальная верификация такой системы - модуля безопасности для ядра Linux; описывается выбранный набор инструментов и процесс верификации, а также некоторые необходимые вспомогательные инструменты, разработанные авторами.

Полный текст статьи в формате pdf (на английском)

Ключевые слова

верификация; формальная верификация; дедуктивная верификация; статическая верификация; ядро linux; верификация драйверов

Издание

Труды SYRCoSE 2014.

DOI: 10.15514/SYRCOSE-2014-8-6

Научная группа

Технологии программирования

Все публикации за 2014 год

Все публикации