Для обеспечения качества модулей ядра Linux используются различные подходы. Однако по тем или иным причинам они не позволяют выявить все ошибки. В докладе будет представлен метод статической верификации модулей ядра Linux, который нацелен на выявление всех возможных нарушений проверяемых правил. Также будет рассмотрен инструментарий, который реализует данный метод, представлены результаты его практического применения и продемонстрированы возможности его использования.
Евгений Новиков
Младший научный сотрудник, Институт системного программирования РАН
2010 – окончил факультет управления и прикладной математики (Московский физико-технический Институт, Москва, Россия).
2013 – кандидат физико-математических наук “Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux” (Институт системного программирования РАН, Москва, Россия).
С 2009 – старший лаборант/стажер-исследователь/младший научный сотрудник (Институт системного программирования РАН, Москва, Россия).
Евгений участвовал в совместном проекте Института системного программирования РАН и Linux Foundation по развитию инфраструктуры стандарта LSB в течении 2-х лет. Затем он стал одним из основных разработчиков в проекте по верификации драйверов Linux.
Comment