Building Programming Interface Specifications in the Open System of Componentwise Verification of the Linux Kernel

Nowadays static verification is one of the most promising methods for finding bugs in programs. To apply successfully existing tools for the Linux kernel one needs to perform componentwise verification. Such verification needs an environment model that reflects a real environment of components rather accurately. Development of the complete environment model for Linux kernel components is a very time-consuming task since there are too many programming interfaces in the kernel and they are not stable. The given paper suggests a new approach for building programming interface specifications. This approach allows one to apply static verification tools efficiently (with small number of false alarms but without missed bugs) for checking rules of programming interfaces usage under conditions of the incomplete environment model, if component developers obey a specific coding style. Two implementations of the suggested approach were developed. The first one extended the BLAST static verification tool while the second one utilized C Instrumentation Framework – an aspect-oriented programming implementation for the C programming language. The latter allowed to use various static verification tools, like BLAST, CPAchecker, CBMC, etc., for checking specifications. In practice that implementation helped to reduce the number of false alarms on more than 70% for some rules of programming interfaces usage. The paper shows that to avoid left false alarms one needs to develop more precise environment models and to use more accurate static verification tools. Besides the Linux kernel the suggested approach can be applied for componentwise verification in projects where developers obey the specific coding style.

Linux kernel, kernel component, device driver, rule of programming interfaces usage, specification, environment model, static verification, aspect-oriented programming, C programming language

1. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an Open Framework for C Verification Tools Benchmarking. In Proc. Perspectives of Systems Informatics (PSI), LNCS, vol 7162, pp. 82-91, 2012. doi: 10.1007/978-3-642-29709-0_17

2. 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).

3. Open verification system Linux Driver Verification. http://linuxtesting.ru/ldv.

4. Fagan M.E. Design and Code Inspections to Reduce Errors in Program Development. IBM Systems Journal, vol. 38, issue 2/3, pp. 258-287, 1999. doi: 10.1147/sj.382.0258

5. Novikov E. One Approach to Aspect-Oriented Programming Implementation for the C programming language. In Proc. 5th Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE), pp. 74-81, 2011.

6. Boehm B., Basili V. Software Defect Reduction Top 10 List. Computer, vol. 34, issue 1, pp. 135-137, 2001. doi: 10.1109/2.962984

7. C Instrumentation Framework: aspect-oriented programming implementation for the C programming language. http://forge.ispras.ru/projects/cif.

8. Raymond E.S. The Cathedral and the Bazaar: Musings on Linux and Open Source by an Accidental Revolutionary. O'Reilly Media, 1999.

9. Novikov E.M., Khoroshilov А.V. Ispol'zovanie aspektno-orientirovannogo programmirovaniya dlya vypolneniya zaprosov po iskhodnomu kodu programm [Using Aspect-Oriented Programming for Querying Source Code]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 23, pp. 371-386, 2012 (in Russian).

10. Chamberlain D., Cross D., Wardley A. Perl Template Toolkit. O'Reilly Media, 2003.

11. Larson P. Testing Linux with the Linux Test Project. In Proc. Ottawa Linux Symposium, 2002.

12. Gunton N. Creating Modular Web Pages With EmbPerl. 2001, http://www.perl.com/pub/2001/03/embperl.html.

13. Novell System Test Kit for Linux. https://www.suse.com/partners/ihv/pdf/SystemTestKit-7.1-Linux-10_22_12.pdf.

14. Oracle Linux Tests. https://oss.oracle.com/projects/olt/dist/documentation/OLT_TestCoverage.pdf.

15. TSyvarev А.V., Martirosyan V.А. Testirovanie drajverov fajlovykh sistem v OS Linux [Testing of Linux File System Drivers].Trudy ISP RАN [The Proceedings of ISP RAS], vol. 23, pp. 413-426, 2012 (in Russian).

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

17. Coverity Scan: 2011 Open Source Integrity Report. http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf.

18. Stuart H. Hunting bugs with Coccinelle. University of Copenhagen, Masters Thesis, 2008.

19. Sparse - a Semantic Parser for C. https://sparse.wiki.kernel.org/index.php/Main_Page.

20. Shved P., Mandrykin M., Mutilin V. Predicate Analysis with Blast 2.7. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 525–527, 2012. doi: 10.1007/978-3-642-28756-5_39

21. Shved P., Mandrykin M., Mutilin V. Predicate Analysis with Blast 2.7. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 525–527, 2012. doi: 10.1007/978-3-642-28756-5_39

22. Löwe S., Wendler P. CPAchecker with Adjustable Predicate Analysis. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 528–530, 2012. doi: 10.1007/978-3-642-28756-5_40

23. Sinz C., Merz F., Falke S. LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 542–544, 2012. doi: 10.1007/978-3-642-28756-5_44

24. Beyer D. Competition on Software Verification. In Proc. 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

25. Results of the 2013 2nd International Competition on Software Verification. http://sv-comp.sosy-lab.org/2013/results/index.php.

26. Engler D., Musuvathi M. Static analysis versus model checking for bug finding. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 2937, pp. 191-210, 2004. doi: 10.1007/978-3-540-24622-0_17

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

28. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The Static Driver Verifier Research Platform. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 119–122, 2010. 10.1007/978-3-642-14295-6_11

29. Post H., Küchlin W. Integrated static analysis for Linux device driver verification. In Proc. Integrated Formal Methods (IFM), LNCS, vol. 4591, pp. 518-537, 2007. doi: 10.1007/978-3-540-73210-5_27

30. 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).

31. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an Open Framework for C Verification Tools Benchmarking. In Proc. Perspectives of Systems Informatics (PSI), LNCS, vol 7162, pp. 82-91, 2012. doi: 10.1007/978-3-642-29709-0_17

32. Open verification system Linux Driver Verification. http://linuxtesting.ru/ldv.

33. Novikov E. One Approach to Aspect-Oriented Programming Implementation for the C programming language. In Proc. 5th Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE), pp. 74-81, 2011.

34. C Instrumentation Framework: aspect-oriented programming implementation for the C programming language. http://forge.ispras.ru/projects/cif.

35. Novikov E.M., Khoroshilov А.V. Ispol'zovanie aspektno-orientirovannogo programmirovaniya dlya vypolneniya zaprosov po iskhodnomu kodu programm [Using Aspect-Oriented Programming for Querying Source Code]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 23, pp. 371-386, 2012 (in Russian).

36. Chamberlain D., Cross D., Wardley A. Perl Template Toolkit. O'Reilly Media, 2003.

37. Gunton N. Creating Modular Web Pages With EmbPerl. 2001, http://www.perl.com/pub/2001/03/embperl.html.