Minimizing the Number of Static Verifier Traces to Reduce Time for Finding Bugs in Linux Kernel Modules
Vitaly Mordan, Evgeny Novikov · Proceedings of the Spring/Summer young researchers' colloquium on software engineering · 2014
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.