Formal Verification of Linux Kernel Library Functions
https://doi.org/10.15514/ISPRAS-2017-29(6)-3
Abstract
The paper presents result of a study on deductive verification of 26 Linux kernel library functions with AstraVer toolset. The code includes primarily string-manipulating functions and is verified against contract specifications formalizing its functional correctness properties. The paper presents a brief review of the related earlier studies, discusses their results and indicates both the previous issues that were successfully solved in this study and the ones that remain and still prevent successful verification. The paper also presents several specification practices that were applied in the study, including some common specification patterns. The authors have successfully and fully proved functional correctness of 25 functions. The paper includes results of benchmarking 5 state-of-the-art SMT solvers on the resulting verification conditions.
About the Authors
D. V. Efremov
NRU Higher School of Economics
Russian Federation
Russian Federation
M. U. Mandrykin
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. MISRA C: 2012. Guidelines for the Use of the C Language in Critical Systems, ISBN 978-1-906400-10-1 (paperback), ISBN 978-1-906400-11-8 (PDF), March 2013.
2. AstraVer Toolset: deductive verification of Linux kernel modules and security policy models. ISP RAS. Available at: http://linuxtesting.org/astraver, accessed 15.10.2017.S
3. Mandrykin M. U., Khoroshilov A. V. High-level memory model with low-level pointer cast support for Jessie intermediate language. Programming and Computer Software, 2015, vol. 41, no. 4, pp. 197-207. DOI: 10.1134/S0361768815040040
4. Mandrykin M. U., Khoroshilov A. V. Region analysis for deductive verification of C programs. Programming and Computer Software, 2016, vol. 42, no. 5, pp. 257-278. DOI: 10.1134/S0361768816050042
5. Carvalho N., Silva Sousa C., Pinto J.S., Tomb A. Formal verification of kLIBC with the WP frama-C plug-in. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 343-358. Springer, Heidelberg (2014).
6. Torlakcik M. Contracts in OpenBSD. MSc thesis. University College Dublin. April, 2010.
7. Efremov D., Mandrykin M. VerKer: Verification of Linux Kernel Library Functions. Available at: http://forge.ispras.ru/projects/verker, accessed 15.10.2017.
8. Cuoq P., Kirchner F., Kosmatov N., Prevosto V., Signoles J., Yakobowski B. Frama-C: A Software Analysis Perspective. Proceedings of the 10th International Conference on Software Engineering and Formal Methods. SEFM'12. Thessaloniki, Greece. 2012. Lecture Notes in Computer Science, vol. 7504, pp. 233-247. Springer-Verlag. Berlin, Heidelberg. 2012.
9. Baudin P., Cuoq P., Filliâtre J., Marché C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. Version 1.12. CEA LIST and INRIA. May, 2017. Available at: https://frama-c.com/download/acsl_1.12.pdf, accessed 15.10.2017.
10. Moy Y. Automatic Modular Static Safety Checking for C Programs. PhD thesis. Université Paris-Sud. January, 2009.
11. Filliâtre J., Paskevich A. Why3: Where Programs Meet Provers. Proceedings of the 22Nd European Conference on Programming Languages and Systems. ESOP'13. Rome, Italy. LNCS, vol. 7792, pp. 125-128. Springer-Verlag.
12. Burghardt J., Clausecker R., Gerlach J., Pohl H. ACSL By Example: Towards a Verified C Standard Library. Version 15.1.1. Available at: https://github.com/fraunhoferfokus/acsl-by-example/raw/master/ACSL-by-Example.pdf, accessed 15.10.2017.
13. Cok D., Blissard I., Robbins J. C Library annotations in ACSL for Frama-C: experience report. GrammaTech, Inc. March, 2017. Available at: http://annotationsforall.org/resources/links/GT-libc-experience-report.pdf, accessed 15.10.2017.
14. Hatcliff J., Leavens G. T., Leino K. R. M., Müller P., Parkinson M. Behavioral interface specification languages. ACM Comput. Surv. vol. 44, issue 3, article 16, 58 pages. June 2012.
15. ISO/IEC 9899: 2011: C11 standard for C programming language. JTC and ISO. April 7, 2016.
16. Hubert T., Marché C. Separation Analysis for Deductive Verification. Heap Analysis and Verification (HAV'07). Braga, Portugal, March 2007, pp. 81-93.
17. Moy Y. Union and Cast in Deductive Verification. Proceedings of the C/C++ Verification Workshop. Technical Report ICIS-R07015, pp. 1-16. Radboud University Nijmegen. July, 2007.
18. Signoles J. E-ACSL Executable ANSI/ISO C Specification Language. Version 1.12. CEA LIST. May, 2017. Available at: https://frama-c.com/download/e-acsl/e-acsl.pdf, accessed 15.10.2017.
19. Marché C. [Frama-c-discuss] Frama-C/WP and CVC4 (version 1.5). Available at: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2017-August/005338.html, accessed 15.10.2017.
Review
For citations:
Efremov D.V., Mandrykin M.U. Formal Verification of Linux Kernel Library Functions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(6):49-76. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(6)-3
Email this article 