Minimizing the number of static verifier traces to reduce time for finding bugs in Linux kernel modules.
Minimizing the number of static verifier traces to reduce time for finding bugs in Linux kernel modules.
Авторы
Аннотация
Static verifiers usually stop after they find a first bug in a program under analysis. This slows down the process of finding and fixing of bugs of the same kind in a given Linux kernel module. In order to solve this problem we used the static verifier CPAchecker with option to continue analysis after finding of a first bug. Besides we extended LDV Tools – a toolset for verification of Linux kernel modules – for finding several bugs in a given module against a specified rule specification. But first experiments revealed a new problem – the verifier produced too many similar traces. The given paper introduces a formal definition of equivalent traces and presents different comparison algorithms and a semi-automated approach, which makes possible to find several bugs in a given Linux kernel module against a specified rule specification at once.
Ключевые слова
Издание
Proceedings of the 8th Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE 2014), editors A. Kamkin, A. Petrenko, A. Terekhov, Saint Petersburg, Russia, May 29-31. ISP RAS, Moscow, 2014.
DOI: 10.15514/SYRCOSE-2014-8-5
2311-7230
Научная группа
Все публикации за 2014 год
Все публикации