Дедуктивная верификация модулей ядра
Проект Linux Deductive Verification нацелен на развитие свободных инструментов дедуктивной верификации, поддерживающих верификацию кода ядра Linux. Основной прикладной целью проекта является доказательство корректности реализации специализированного модуля управления доступом, разработанного для операционной системы специального назначения Astra Linux Special Edition.
В рамках проекта мы развиваем цепочку инструментов дедуктивной верификации Astraver Toolset, базирующуюся на трёх открытых компонентах: Frama-C + Jessie plugin + Why3. Эти инструменты были нами улучшены с целью исправления ошибок и реализации поддержки верификации кода модулей ядра Linux. Наиболее существенные изменения были внесены в инструмент Jessie, тогда как исправления в Frama-C и Why3 достаточно локальны. Некоторые из наших изменений уже приняли в оригинальные проекты Jessie и Why3, тогда как оставшиеся изменения доступны в наших публичных репозиториях.
Более подробное описание наших доработок и инструкции опубликованы в анонсах выпуска новых версий наших инструментов:
Для знакомства с принципами дедуктивной верификации программ рекомендуем воспользоваться нашими методическими материалами, подготовленными для курса "Формальная спецификация и верификация программ", читаемому на факультете ВМК МГУ им. М.В.Ломоносова.
В развитие настоящего проекта, ИСП РАН в партнерстве с АО «НПО РусБИТех» и ФГУП «ГосНИИАС» стартовал новый проект, поддержанный Министерством науки и высшего образования РФ. Основными целями нового проекта является разработка новых технологий верификации программного обеспечения, обеспечивающих высокую надежность и информационную безопасность вычислительных систем ответственного назначения, включая операционные системы, встроенные системы управления, системы обработки данных и роботизированные системы, используемые в критических областях (космосе и авиации, атомной энергетике, медицине). Подробнее смотрите на специализированном сайте проекта.