Configurable Toolset for Static Verification of Operating Systems Kernel Modules

An operating system (OS) kernel is a critical software regarding to reliability and efficiency. Quality of a modern OSs kernel is high enough. Another situation is with kernel modules, e.g. device drivers, which due to various reasons have a significantly lower level of quality. One of the most critical and widespread bugs in kernel modules are violations of rules of correct usage of a kernel API. One can identify all such the violations in modules or prove their correctness with help of static verification tools which needs contract specifications describing formally obligations of a kernel and modules with respect to each other. The paper considers existing methods and toolsets for static verification of kernel modules of different OSs. It suggests a new method for static verification of Linux kernel modules that allows to configure checking at each of its stages. The paper shows how this method can be adapted for checking kernel components of other OSs. It describes an architecture of a configurable toolset for static verification of Linux kernel modules, which implements the proposed method, and demonstrates results of its practical application. Directions of further development are considered in conclusion

operating system kernel, kernel module, software quality, static verification, contract specification, environment model, specification of rule of correct usage of API

1. Chou A., Yang J., Chelf B., Hallem S., Engler D. An empirical study of operating system errors. Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), pp. 73-88, 2001. doi: 10.1145/502034.502042

2. Swift M., Bershad B., Levy H. Improving the reliability of commodity operating systems. Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP), pp. 73-88, 2003. doi: 10.1145/502034.502042

3. Palix N., Thomas G., Saha S., Calves C., Lawall J., Muller G. Faults in Linux: ten years later. Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 305-318, 2011. doi: 10.1145/1950365.1950401

4. Mutilin V.S., Novikov E.M., Khoroshilov А.V. Аnaliz tipovykh oshibok v drajverakh operatsionnoj sistemy Linux [Analysis of typical faults in Linux operating system drivers]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 22, pp. 349-374, 2012 (in Russian).

5. Ball T., Bounimova E., Cook B., Levin V., Lichtenberg J., McGarvey C., Ondrusek B., Rajamani S. K., Ustuner A. Thorough static analysis of device drivers. Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), pp. 73-85, 2006. doi: 10.1145/1218063.1217943

6. Glass R.L. Facts and fallacies of software engineering. Addison-Wesley Professional, 2002.

7. Engler D., Chelf B., Chou A., Hallem S. Checking system rules using system-specific, programmer-written compiler extensions. Proceedings of the 4th conference on Symposium on Operating System Design & Implementation (OSDI), vol. 4, pp. 1-16, 2000.

8. Аvetisyan А., Belevantsev А., Borodin А., Nesov V. Ispol'zovanie staticheskogo analiza dlya poiska uyazvimostej i kriticheskikh oshibok v iskhodnom kode programm [Using static analysis for finding security vulnerabilities and critical errors in source code]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 21, pp. 23-38, 2011 (in Russian).

9. Lawall J. L., Brunel J., Palix N., Rydhof H. R., Stuart H., Muller G. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 43—52, 2009. doi: 10.1109/DSN.2009.5270354

10. Mandrykin M.U., Mutilin V.S., Khoroshilov А.V. Vvedenie v metod CEGAR — utochnenie abstraktsii po kontrprimeram [Introduction to CEGAR — Counter-Example Guided Abstraction Refinement]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 24, pp. 219-292, 2013 (in Russian).

11. Engler D., Musuvathi M. Static analysis versus model checking for bug finding. Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 2937, pp. 191-210, 2004. doi: 10.1007/978-3-540-24622-0_17

12. Beyer D. Competition on Software Verification. Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 504-524, 2012. doi: 10.1007/978-3-642-28756-5_38

13. Beyer D. Second Competition on Software Verification. Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7795, pp. 594-609, 2013. doi: 10.1007/978-3-642-36742-7_43

14. Mandrykin M.U., Mutilin V.S., Novikov E.M., Khoroshilov А.V. Obzor instrumentov staticheskoj verifikatsii Si programm v primenenii k drajveram ustrojstv operatsionnoj sistemy Linux [Static verification tools for C programs and Linux device drivers: A survey]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 22, pp. 293-326, 2012 (in Russian).

15. Corbet J., Kroah-Hartman G., McPherson A. Linux kernel development. How Fast it is Going, Who is Doing It, What They are Doing, and Who is Sponsoring It. http://go.linuxfoundation.org/who-writes-linux-2012, 2012.

16. Ball T., Levin V., Rajamani S.K. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, pp. 68-76, 2011. doi: 10.1145/1965724.1965743

17. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static driver verification with under 4% false alarms. Proceedings of the 10th International Conference on Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 35-42, 2010.

18. Ball T., Rajamani S.K. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.

19. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The Static Driver Verifier Research Platform. Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 119–122, 2010. doi: 10.1007/978-3-642-14295-6_11

20. Witkowski T., Blanc N., Kroening D., Weissenbacher G. Model checking concurrent Linux device drivers. Proceedings of the 22nd IEEE/ACM international conference on Automated Software Engineering (ASE), pp. 501-504, 2007. doi: 10.1145/1321631.1321719

21. Post H., Küchlin W. Integrated static analysis for Linux device driver verification. Proceedings of the 6th International Conference on Integrated Formal Methods (IFM), LNCS, vol. 4591, pp. 518-537, 2007. doi: 10.1007/978-3-540-73210-5_27

22. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2988, pp. 168-176, 2004. doi: 10.1007/978-3-540-24730-2_15

23. Clarke E., Kroening D., Sharygina N., Yorav K. SATABS: SAT-based predicate abstraction for ANSI-C. Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3440, pp. 570–574, 2005. doi: 10.1007/978-3-540-31980-1_40

24. Mutilin V.S. Verifikatsiya drajverov operatsionnoj sistemy Linux pri pomoshhi predikatnykh abstraktsij [Linux drivers verification with help of predicate abstractions]. Dissertatsiya na soiskanie uchenoj stepeni kandidata fiziko-matematicheskikh nauk, ISP RАN [PhD thesis, ISP RAS], 2012 (in Russian).

25. Zakharov I.S., Mutilin V.S., Novikov E.M., Khoroshilov А.V. Modelirovanie okruzheniya drajverov ustrojstv operatsionnoj sistemy Linux [Environment modeling of Linux operating system device drivers]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 25, pp. 85-112, 2013 (in Russian).

26. Novikov E.M. Razvitie metoda kontraktnykh spetsifikatsij dlya verifikatsii modulej yadra operatsionnoj sistemy Linux. [Development of contract specifications method for verification of Linux kernel modules]. Dissertatsiya na soiskanie uchenoj stepeni kandidata fiziko-matematicheskikh nauk, ISP RАN [PhD thesis, ISP RAS], 2013 (in Russian).

27. Necula G. C., McPeak S., Rahul S.P., Weimer W. CIL: Intermediate language and tools for analysis and transformation of C programs. Proceedings of the 11th International Conference on Conference on Compiler Construction, LNCS, vol. 2304, pp. 213-228, 2002. doi: 10.1007/3-540-45937-5_16

28. Mutilin V.S., Novikov E.M., Strakh А.V., Khoroshilov А.V., Shved P.E. Аrkhitektura Linux Driver Verification [Linux Driver Verification architecture]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 20, pp. 163-187, 2011 (in Russian).

29. Khoroshilov A., Mutilin V., Novikov E., Zakharov I. Modeling environment for static verification of Linux kernel modules. Proceedings of the 11th International Andrei Ershov Memorial Conference (PSI), 2014.

30. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z

31. Beyer D., Keremoglu M.E. CPAchecker: A tool for configurable software verification. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184–190, 2011. doi: 10.1007/978-3-642-22110-1_16

32. Albarghouthi A., Li Y., Gurfinkel A., Chechik M. UFO: A framework for abstraction and interpolation-based software verification. Proceedings of the 24th International Conference on Computer Aided Verification, LNCS, vol. 7358, pp. 672-678, 2012. doi: 10.1007/978-3-642-31424-7_48

33. Novikov E.M. Uproshhenie analiza trass oshibok instrumentov staticheskogo analiza koda. [Simplification of static verifier traces analysis]. Аktual'nye Problemy Programmnoj Inzhenerii [Аctual Problems of Software Engineering], pp. 215-221, 2011 (in Russian).

34. List of bugs found in Linux kernel modules with help of configurable toolset for static verification Linux Driver Verification Tools. http://linuxtesting.org/results/ldv.

35. Mandrykin M.U., Mutilin V.S., Novikov E.M., Khoroshilov A.V., Shved P.E. Using Linux device drivers for static verification tools benchmarking. Programming and Computer Software, vol. 38, n. 5, стр. 245-256, 2012.

36. Beyer D. Petrenko A. Linux Driver Verification. Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, LNCS, vol. 7610, pp. 1-6, 2012. doi: 10.1007/s10009-007-0044-z