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 ГБ свободного места на диске.

Схема работы

klever

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

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

Перейти к списку всех технологий