Deductive Verification of Unmodified Linux Kernel Library Functions

  • Denis EfremovEmail author
  • Mikhail Mandrykin
  • Alexey Khoroshilov
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


This paper presents results from the development and evaluation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conventional memory and string operations. The formal contract of the functions was extracted from their source code and was represented in the form of preconditions and postconditions. The correctness of 23 functions was completely proved using AstraVer toolset, although success for 11 functions was achieved using 2 new specification language constructs. Another 2 functions were proved after a minor modification of their source code, while the final one cannot be completely proved using the existing memory model. The benchmark can be used for the testing and evaluation of deductive verification tools and as a starting point for verifying other parts of the Linux kernel.


Formal verification Deductive verification Linux kernel 


  1. 1.
    Baudin, P., et al.: ACSL: ANSI/ISO C specification language. Technical report 1.12, CEALIST and INRIA, March 2017Google Scholar
  2. 2.
    Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015). Scholar
  3. 3.
    Moy, Y.: Automatic Modular Static Safety Checking for C Programs. Ph.D. thesis, Université Paris-Sud, January 2009.
  4. 4.
    Mandrykin, M.U., Khoroshilov, A.V.: Region analysis for deductive verification of c programs. Program. Comput. Softw. 42(5), 257–278 (2016). Scholar
  5. 5.
    Carvalho, N., da 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, Cham (2014). Scholar
  6. 6.
    Torlakcik, M.: Contracts in OpenBSD. dissertation report, University College Dublin (2010)Google Scholar
  7. 7.
    Verker: Verification of linux kernel library functions (2017).
  8. 8.
    Burghardt, J., Clausecker, R., Gerlach, J., Pohl, H.: ACSL by example. Technical report, Fraunhofer Institute for Open Communication Systems (2017)Google Scholar
  9. 9.
    Cok, D.R., Blissard, I., Robbins, J.: C library annotations in ACSL for frama-C: experience report. GrammaTech, Inc, Technical report, March 2017Google Scholar
  10. 10.
    Hubert, T., Marché, C.: Separation analysis for deductive verification. In: Heap Analysis and Verification (HAV 2007), Braga, Portugal, pp. 81–93, March 2007.
  11. 11.
    ISO/IEC 9899: 2011: C11 standard for C programming language. Standard, JTC and ISO (2011).
  12. 12.
    Moy, Y.: Union and cast in deductive verification. In: Proceedings of the C/C++ Verification Workshop. Technical report ICIS-R07015, pp. 1–16. Radboud University Nijmegen, July 2007.
  13. 13.
    Mandrykin, M.U., Khoroshilov, A.V.: High-level memory model with low-level pointer cast support for jessie intermediate language. Program. Comput. Softw. 41(4), 197–207 (2015). Scholar
  14. 14.
    Leino, K.R.M., Moskal, M.: Usable auto-active verification (2010)Google Scholar
  15. 15.
    Dross, C., Moy, Y.: Auto-active proof of red-black trees in SPARK. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 68–83. Springer, Cham (2017). Scholar
  16. 16.
    Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010). Scholar
  17. 17.
    Verker: Verification of linux kernel library functions, lemma functions branch (2017).
  18. 18.
    Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC 2013, pp. 1230–1235. ACM, New York (2013).
  19. 19.
    Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Denis Efremov
    • 1
    • 2
    Email author
  • Mikhail Mandrykin
    • 2
  • Alexey Khoroshilov
    • 1
    • 2
    • 3
    • 4
  1. 1.National Research University Higher School of EconomicsMoscowRussia
  2. 2.Ivannikov Institute for System Programming of the RASMoscowRussia
  3. 3.Moscow Institute of Physics and TechnologyMoscowRussia
  4. 4.Lomonosov Moscow State UniversityMoscowRussia

Personalised recommendations