Конфигурируемая система статической верификации модулей ядра операционных системстатья
Статья опубликована в журнале из списка RSCI Web of Science
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из перечня ВАК
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 2 ноября 2015 г.
Аннотация:Ядро операционной системы (ОС) представляет собой критичную в отношении надежности
и производительности программную систему. Качество ядра современных ОС уже находится
на достаточно высоком уровне. Иначе обстоит дело с модулями ядра, например, драйверами
устройств, которые по ряду причин имеют существенно более низкий уровень качества.
Одними из наиболее критичных и распространенных ошибок в модулях ядра являются
нарушения правил корректного использования программного интерфейса ядра ОС. Выявить
все такие нарушения в модулях или доказать их корректность потенциально можно с
помощью инструментов статической верификации, которым для проведения анализа
необходимо предоставить контрактные спецификации, описывающие формальным образом
обязательства ядра и модулей по отношению друг к другу. В статье рассматриваются
существующие методы и системы статической верификации модулей ядра различных ОС.
Предлагается новый метод статической верификации модулей ядра ОС Linux, который
позволяет конфигурировать процесс проверки на каждом из его этапов. Показывается, каким
образом данный метод может быть адаптирован для проверки компонентов ядра других ОС.
Описывается архитектура конфигурируемой системы статической верификации модулей
ядра ОС Linux, реализующей предложенный метод, и демонстрируются результаты ее
практического применения. В заключении рассматриваются направления дальнейшего
развития.