Сборники трудов ИСП РАН


Верификация драйверов операционной системы Linux.

Д. Бейер, А.К. Петренко.

Аннотация

Верификация драйверов ОС Linux – это широкая область для применения различных методов верификации, в частности, методов проверки свойств безопасности и надежности программ, а также функциональной верификации. Драйверы Linux – это индустриальное программное обеспечение, на стабильность которого полагаются ИТ-инфраструктуры. В силу этого к надежности и корректности их работы предъявляют жесткие требования, в свою очередь, это означает, что если инженер-верификатор обнаружил ошибку в драйвере, он может рассчитывать на быструю реакцию сообщества разработчиков в плане подтверждения и исправления этой ошибки. Драйверы Linux – сложное низкоуровневое системное программное обеспечение, и его характеристики требуют применения различных техник анализа программ: использования SMT-решателей, методов верификации моделей (model checking) и других методов верификации. Точность и эффективность этих методов за последнее время значительно повысилась, и поэтому сложная задача верификации драйверов ОС Linux становится реальной по мере использования этих достижений в инструментах верификации.

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

Ядро операционной системы, Linux, инструменты верификции, анализ программ, верификация моделей, анализ указателей, анализ структур данных, свойства безопасности, ограничиваемая проверка моделей, символьная верификация, анализ с явными значениями, условная

Издание

Труды Института системного программирования РАН, том 23, 2012, стр. 405-412.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-23-23

Полный текст статьи в формате pdf Вернуться к содержанию тома