Minimizing the number of static verifier traces to reduce time for finding bugs in Linux kernel modules.

Authors

V. Mordan, E. Novikov.

Abstract

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.

Full text of the paper in pdf

Keywords

Linux kernel module; correctness rule; static verifier trace; equivalence class

Edition

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

Research Group

Software Engineering

All publications during 2014

All publications