ИСПОЛЬЗОВАНИЕ ДРАЙВЕРОВ УСТРОЙСТВ ОПЕРАЦИОННОЙ СИСТЕМЫ LINUX ДЛЯ СРАВНЕНИЯ ИНСТРУМЕНТОВ СТАТИЧЕСКОЙ ВЕРИФИКАЦИИ

摘要

Система верификации Linux Driver Verification предназначена для статического анализа исходного кода драйверов устройств операционной системы Linux. В настоящей статье описывается архитектура системы верификации, включая средства интеграции сторонних инструментов статической верификации Си программ. Рассматриваются характеристики исходного кода драйверов Linux, интересные с точки зрения алгоритмов верификации, приводятся примеры проведения сравнительного анализа различных инструментов верификации, а также различных версий и конфигураций одного инструмента.