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

user warning: Got error 28 from storage engine query: SELECT t.*,v.weight AS v_weight_unused FROM term_node r INNER JOIN term_data t ON r.tid = t.tid INNER JOIN vocabulary v ON t.vid = v.vid WHERE r.vid = 246 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.33/modules/taxonomy/taxonomy.module on line 640.

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

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

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

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