Видеоролик о технологиях ИСП РАН
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 ГБ свободного места на диске.
Схема работы
Разработчик/участник
Перейти к списку всех технологий