Proceedings of ISP RAS


Static Verification Tools for C Programs and Linux Device Drivers: A Survey.

Khoroshilov A.V., Mandrykin M.U., Mutilin V.S., Novikov E.M.

Abstract

The survey considers methods and techniques used in modern static verification tools for C programs. It describes two main approaches Counter Example Guided Abstraction Refinement (CEGAR) and Bounded Model Checking (BMC) and techniques used to efficiently implement them such as Predicate Abstraction, Abstract Reachability Tree, Lazy Abstraction, Configurable Program Analysis, Explicit Analysis, Interpolation, and Shape Analysis. The paper also discusses current capabilities of the tools such as supported C programming language constructs, scalability, properties being checked, and trustworthiness of analysis results.

We provide description of such static verification tools, as BLAST, CPAchecker, HSF(C), SATABS, SLAM, WOLVERINE, YOGI, CBMC, ESBMC, LLBMC, FSHELL and PREDATOR. This description shows techniques implemented in these tools and their current capabilities. The paper presents results of the 1st International Competition on Software Verification in category DeviceDrivers64 which contains verification tasks based on device drivers from Linux kernel 3.0.

Specifics of device drivers verification are discussed and existing driver verification systems are described including Microsoft SDV for Windows operating system and DDVerify, Avinux and Linux Driver Verification for Linux. The paper concludes that BMC-based tools work well for programs of limited size and control flow complexity. Regarding verification of device drivers that means these tools are able to quickly find violations of properties being checked if paths to these violations are quite short, but they mostly fail to prove correctness and to find complicated bugs. CEGARbased tools demonstrate better scalability, while they have problems with handling address arithmetic and complex memory structures. For future improvements in static verification of

C programs and Linux device drivers we propose composition of various techniques and modularization of analysis.

Keywords

verification, static analysis, device drivers, Linux operating system.

Edition

Proceedings of the Institute for System Programming, vol. 22, 2012, pp. 293-326.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-17

Full text of the paper in pdf (in Russian) Back to the contents of the volume