Институт системного программирования им. В.П. Иванникова РАН

Klever: система верификации моделей промышленного ПО

Klever – система верификации моделей, которые генерируются автоматически на основе исходного кода промышленного программного обеспечения, разрабатываемого на языке программирования Си. Klever позволяет специфицировать различные требования по безопасности и надёжности, а также проверять их выполнение автоматически с заданным уровнем точности.

Особенности и преимущества

Klever базируется на результатах передовых научных исследований в области автоматического построения и верификации моделей программ. В основе системы верификации лежат методы для покомпонентной верификации, моделирования окружения и спецификации требований, что делает возможным применение формальных методов к исходному коду промышленного программного обеспечения размером в сотни тысяч и миллионы строк кода на языке программирования Си. Klever является проектом с открытым исходным кодом (https://forge.ispras.ru/projects/klever).

Klever – это:

• Высокоточный консервативный анализ исходного кода промышленного программного обеспечения, позволяющий выявлять все возможные ошибки искомых видов и доказывать корректность программ при явно заданных предположениях.
• Масштабируемость. Покомпонентная верификация программ позволяет применять к большому объёму исходного кода наиболее точные методы анализа, такие как верификация моделей и символьное выполнение.
• Возможность адаптации под конкретные нужды заказчиков. Разработка спецификаций моделей окружения целевых программ, а также спецификаций для обнаружения нарушений, специфичных для программ требований, в дополнение к проверке общих правил безопасного программирования на языке Си.
• Детализированное представление выявленных ошибок. При обнаружении ошибок система верификации выдаёт подробные трассы ошибок, включающие конкретные значения переменных и аргументов вызываемых функций.
• Удобный многопользовательский веб-интерфейс для подготовки и запуска верификации, а также для выполнения экспертной оценки результатов верификации.

Для кого предназначен Klever?

• Компании, разрабатывающие программное обеспечение с высоким уровнем надёжности и безопасности.
• Сертификационные лаборатории.

Опыт внедрения

В основном система верификации Klever применяется для тщательной проверки ядер и драйверов различных операционных систем. Для демонстрации возможностей системы Klever были выполнены работы по верификации драйверов устройств ядра Linux. В результате удалось обнаружить более 400 ошибок следующих типов: выход за границу буфера, разыменование нулевого указателя, использование неинициализированной памяти, повторное или некорректное освобождение памяти, утечка памяти, состояние гонки, взаимная блокировка, некорректный вызов функции в зависимости от контекста, некорректная инициализация структур данных ядра Linux и т.д. Данные ошибки были признаны разработчиками ядра Linux.

Системные требования

Ubuntu 18.04/20.04, не менее 4-х процессорных ядер x86-64, 16 ГБ оперативной памяти и 100 ГБ свободного места на диске.

Схема работы

Разработчик/участник

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