Static verification for memory safety of Linux kernel drivers
https://doi.org/10.15514/ISPRAS-2016-30(6)-8
Abstract
Memory errors in Linux kernel drivers are a kind of serious bugs that can lead to dangerous consequences but such errors are hard to detect. This article describes static verification that aims at finding all errors under certain assumptions. Static verification of industrial projects such as the Linux kernel requires additional effort. Limitations of current tools for static verification disallow to analyze the Linux kernel as a whole, so we use a simplified automatically generated environment model. This model introduces inaccuracy, but provides ability for verification. In addition, we allow absent definitions for some functions which results in incomplete ANSI C programs. The current work proposes an approach to reveal issues with memory usage in such incomplete programs. Our static verification technique is based on Symbolic Memory Graphs (SMG) with extensions aiming to reduce a false alarm rate. We introduced an on-demand memory conception for simplification of kernel API models and implemented this conception in static verification tool CPAchecker. Also, we changed precision of a CPAchecker memory model from bytes to bits and supported structure alignment similar to the GCC compiler. We implemented the predicate extension for SMG to improve accuracy of the analysis. We verified of Linux kernel 4.11.6 and 4.16.10 with help of the Klever verification framework with CPAchecker as a verification engine. Manual analysis of warnings produced by Klever revealed 78 real bugs in drivers. We have made patches to fix 33 of them.
About the Author
A. A. Vasilyev
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. [1]. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser, Comprehensive formal verification of an os microkernel. ACM Transactions on Computer Systems, vol. 32, no. 1, 2014, pp. 2:1–2:70.
2. [2]. T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner, Thorough static analysis of device drivers. SIGOPS Operating Systems Review, vol. 40, no. 4, 2006, pp. 73–85.
3. [3]. D. Engler and M. Musuvathi. Static analysis versus software model checking for bug finding. Lecture Notes in Computer Science, vol. 2937, 2004, pp. 191–210.
4. [4]. Saturn. Precise and Scalable Software Analysis. Available at: http://saturn.stanford.edu/, accessed 01.12.2018.
5. [5]. T. Witkowski, N. Blanc, D. Kroening, and G. Weissenbacher. Model checking concurrent Linux device drivers. In Proceedings of the 22nd IEEE/ACM Int. Conference on Automated Software Engineering, 2007, pp. 501–504.
6. [6]. N. Palix, G. Thomas, S. Saha, C. Calvès, J. Lawall, and G. Muller. Faults in Linux: Ten years later. In Proceedings of the 16th Int. Conference on Architectural Support for Programming Languages and Operating Systems, 2011, pp. 305–318.
7. [7]. Linux driver verification project. Available at: http://linuxtesting.org/ldv, accessed 01.12.2018.
8. [8]. V. Mutilin, E. Novikov, and A. Khoroshilov. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN/Proc. ISP RAS, vol. 22, 2012, pp. 349–374 (in Russian). DOI: 10.15514/ISPRAS-2012-22-19.
9. [9]. A. Khoroshilov, V. Mutilin, A. Petrenko, and V. Zakharov. Establishing Linux driver verification process, Lecture Notes in Computer Science, vol. 5947, pp. 165–176, 2010.
10. [10]. I. Zakharov, M. Mandrykin, V. Mutilin, E. Novikov, A. Petrenko, and A. Khoroshilov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, vol. 41, no. 1, 2015, pp. 49–64.
11. [11]. Klever verification framework. Available at: https://forge.ispras.ru/projects/klever, accessed 01.12.2018.
12. [12]. I.S. Zakharov, V.S. Mutilin, and A.V. Khoroshilov. Pattern-based environment modeling for static verification of linux kernel modules. Programming and Computer Software, vol. 41, no. 3, 2015, pp. 183–195.
13. [13]. A. Khoroshilov, V. Mutilin, E. Novikov, and I. Zakharov. Modeling environment for static verification of linux kernel modules. Lecture Notes in Computer Science, vol. 8974, 2015, pp. 400–414.
14. [14]. E. Novikov and I. Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402–416.
15. [15]. D. Beyer and M. Keremoglu. CPAchecker: A tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184–190.
16. [16]. K. Dudka, P. Peringer, and T. Vojnar. Byte-precise verification of low-level list manipulation. Lecture Notes in Computer Science, vol. 7935, 2013, pp. 215–237.
17. [17]. R. Wilhelm, S. Sagiv, and T. W. Reps. Shape analysis. Lecture Notes in Computer Science, vol. 1781, 2000, pp. 1–17.
18. [18]. D. Beyer, T. A. Henzinger, and G. Théoduloz. Configurable software verification: concretizing the convergence of model checking and program analysis. Lecture Notes in Computer Science, vol. 4590, 2007, pp. 504–518. [Online]. Available: http://portal.acm.org/citation.cfm?id=1770351.1770419
Review
For citations:
Vasilyev A.A. Static verification for memory safety of Linux kernel drivers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(6):143-160. https://doi.org/10.15514/ISPRAS-2016-30(6)-8
Email this article 