Klever: система автоматической статической верификации Си-программ

Klever: система автоматической статической верификации Си-программ

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

Klever ‒ это проект с открытым исходным кодом (https://forge.ispras.ru/projects/klever).

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

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

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

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

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

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

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

Данные ошибки были признаны разработчиками ядра Linux.

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

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

Схема работы

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

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