Дедуктивная верификация модулей ядра

Проект Linux Deductive Verification нацелен на развитие свободных инструментов дедуктивной верификации, поддерживающих верификацию кода ядра Linux. Основной прикладной целью проекта является доказательство корректности реализации специализированного модуля управления доступом, разработанного для операционной системы специального назначения Astra Linux Special Edition.

В рамках проекта мы развиваем цепочку инструментов дедуктивной верификации Astraver Toolset, базирующуюся на трёх открытых компонентах: Frama-C + Jessie plugin + Why3. Эти инструменты были нами улучшены с целью исправления ошибок и реализации поддержки верификации кода модулей ядра Linux. Наиболее существенные изменения были внесены в инструмент Jessie, тогда как исправления в Frama-C и Why3 достаточно локальны. Некоторые из наших изменений уже приняли в оригинальные проекты Jessie и Why3, тогда как оставшиеся изменения доступны в наших публичных репозиториях.

Более подробное описание наших доработок и инструкции опубликованы в анонсах выпуска новых версий наших инструментов:

Для знакомства с принципами дедуктивной верификации программ рекомендуем воспользоваться нашими методическими материалами, подготовленными для курса "Формальная спецификация и верификация программ", читаемому на факультете ВМК МГУ им. М.В.Ломоносова.