Linux Driver Verification

Linux driver verification is a large application area for software verification methods, in particular, for functional, safety, and security verification. Linux driver software is industrial production code — IT infrastructures rely on its stability, and thus, there are strong requirements for correctness and reliability. Linux driver software is complex, low-level systems code, and its characteristics make it necessary to bring to bear techniques from program analysis, SMT solvers, model checking, and other areas of software verification. These areas have recently made a significant progress in terms of precision and performance, and the complex task of verifying Linux driver software can be successful if the conceptual state-of-the-art becomes available in tool implementations.

The paper is based on experience of the research groups led by authors in verification of industrial software. It is important to develop verification tools that are efficient and effective enough to successfully check software components that are as complex as device drivers. In this area verifiers/researchers and Linux society find mutual benefits in cooperation because: for the society it is important to get such crucial software verified; for the verification community it is important to get realistic verification tasks in order to tune and further develop the technology. The paper provides an overview of the state-of-the-art and pointed out research directions in which further progress is essential. In particularly the paper considers most promising verification techniques and tools, including predicate abstraction, counter example generation, explicit-state verification, termination and concurrency analysis. One of main topic of Linux driver verification research is combination of verification techniques.

1. T. Ball, S. K. Rajamani. The Slam Project: Debugging System Software via Static Analysis. Proc. POPL, pp. 1–3. ACM (2002).

2. G. Basler, A. Donaldson, A. Kaiser, D. Kröning, M. Tautschnig, T. Wahl. SATABS: A Bit-Precise Verifier for C Programs. C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 552–555. Springer, Heidelberg (2012).

3. D. Beyer. Competition on Software Verification. C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012).

4. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, R. Sebastiani. Software Model Checking via Large-block Encoding. Proc. FMCAD, pp. 25–32. IEEE (2009).

5. D. Beyer, T. A. Henzinger, R. Jhala, R. Majumdar. The Software Model Checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5-6), 505–525 (2007).

6. D. Beyer, T. A. Henzinger, M. E. Keremoglu, P. Wendler. Conditional Model Checking: A Technique to Pass Information Between Verifiers. Proc. FSE. ACM (2012).

7. D. Beyer, T. A. Henzinger, G. Theoduloz. Program Analysis with Dynamic Precision Adjustment. Proc. ASE, pp. 29–38. IEEE (2008).

8. D. Beyer, M. E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. G. Gopalakrishnan, S. Qadeer (eds.). CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011).

9. D. Beyer, M. E. Keremoglu, P. Wendler. Predicate Abstraction with Adjustable-Block Encoding. Proc. FMCAD, pp. 189–197. FMCAD (2010).

10. A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs.. W. R. Cleaveland (ed.). TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999).

11. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM 50(5), 752–794 (2003).

12. E. Clarke, D. Kröning, N. Sharygina, K. Yorav. SatAbs: SAT-Based Predicate Abstraction for ANSI-C. N. Halbwachs, L. D. Zuck (eds.). TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005).

13. B. Cook, A. Podelski, A. Rybalchenko. Terminator: Beyond Safety. T. Ball, T., R. B. Jones (eds.). CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006).

14. L. Cordeiro, J. Morse, D. Nicole, B. Fischer. Context-Bounded Model Checking with ESBMC 1.17. C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 534–537. Springer, Heidelberg (2012).

15. P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival. Combination of Abstractions in the ASTREE Static Analyze. M. Okada, I. Satoh (eds.). ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008).

16. K. Dudka, P. Müller, P. Peringer, T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 545–548. Springer, Heidelberg (2012).

17. A. Galloway, G. Lüttgen, J. T. Mühlberg, R. I. Siminiceanu. Model-Checking the Linux Virtual File System. N. D. Jones, M. Müller-Olm (eds.). VMCAI 2009. LNCS, vol. 5403, pp. 74–88. Springer, Heidelberg (2009).

18. S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, A. Rybalchenko. HSF(C): A Software Verifier Based on Horn Clauses. C. Flanagan, B. Koenig (eds.). TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg (2012).

19. A. Gupta, C. Popeea, A. Rybalchenko. Threader: A Constraint-Based Verifier for Multi-threaded Programs. G. Gopalakrishnan, S. Qadeer (eds.). CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011).

20. T. A. Henzinger, R. Jhala, R. Majumdar, K. L. McMillan. Abstractions from Proofs. Proc. POPL, pp. 232–244. ACM (2004).

21. T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Lazy Abstraction. Proc. POPL, pp. 58–70. ACM (2002).

22. A. Khoroshilov, V. Mutilin, E. Novikov, P. Shved, A. Strakh. Towards an Open Framework for C Verification Tools Benchmarking // E. Clarke, I. Virbitskaite, A. Voronkov (eds.). PSI 2011. LNCS, vol. 7162, pp. 179–192. Springer, Heidelberg (2012).

23. A. Khoroshilov, V. Mutilin, A. Petrenko, V. Zakharov. Establishing Linux Driver Verification Process // A. Pnueli, I. Virbitskaite, A. Voronkov (eds.). PSI 2009. LNCS, vol. 5947, pp. 165–176. Springer, Heidelberg (2010) .

24. J. T. Mühlberg, G. Lüttgen. Blasting Linux Code // L. Brim, B. R. Haverkort, M. Leucker, J. van de Pol (eds.). FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 211–226. Springer, Heidelberg (2007).

25. W. Penninckx, J. T. Mühlberg, J. Smans, B. Jacobs, F. Piessens. Sound Formal Verification of Linux’s USB BP Keyboard Driver. A. E. Goodloe, S. Person (eds.). NFM 2012. LNCS, vol. 7226, pp. 210–215. Springer, Heidelberg (2012).

26. A. Podelski, A. Rybalchenko. Transition Predicate Abstraction and Fair Termination. Proc. POPL, pp. 132–144. ACM (2005).

27. H. Post, C. Sinz, W. Küchlin. Towards Automatic Software Model Checking of Thousands of Linux Modules — A Case Study with Avinux. Softw. Test., Verif. Reliab. 19(2), 155–172 (2009).

28. P. Shved, M. Mandrykin, V. Mutilin. Predicate Analysis with BLAST 2.7 // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 525–527. Springer, Heidelberg (2012).

29. P.E.Shved, V.S.Mutilin, M.U.Mandrykin. Opyt razvitiya instrumenta staticheskoj verifikatsii BLAST [An Expirience in Static Verification Tool BLAST Improving]. Programming and Computer Software, No. 3, 2012, pp. 24-35 (in Russian).

30. V.S.Mutilin, M.U.Mandrykin, E.M.Novikov, A.V.Khoroshilov, P.E.Shved. Ispol'zovanie drajverov ustrojstv operatsionnoj sistemy Linux dlya sravneniya instrumentov staticheskoj verifikatsii [Usage of Linux Drivers for Comparison of Static Verification Tools]. Programming and Computer Software, No. 5, 2012, pp. 54-71(in Russian).

31. V.S.Mutilin, E.M.Novikov, A.V.Strakh et al. Аrkhitektura Linux Driver Verification [Linux Driver Verification Architecture]. Trudy ISP RАN [The Proceedings of ISP RAS], 2011, vol. 20, pp. 163-187 (in Russian).

32. C. Sinz, F. Merz, S. Falke. LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation // C. Flanagan, B. König (eds.). TACAS 2012. LNCS, vol. 7214, pp. 542–544. Springer, Heidelberg (2012).

33. A. von Rhein, S. Apel, F. Raimondi. Introducing Binary Decision Diagrams in the Explicit-State Verification of Java Code // Proc. Java Pathfinder Workshop (2011).

34. T. Witkowski, N. Blanc, D. Kröning, G. Weissenbacher. Model Checking Concurrent Linux Device Drivers // Proc. ASE, ACM (2007), pp. 501–504.