Advertisement

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)

Abstract

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.

Keywords

Formal verification Deductive verification Linux kernel 

References

  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).  https://doi.org/10.1007/s00165-014-0326-7MathSciNetCrossRefGoogle Scholar
  3. 3.
    Moy, Y.: Automatic Modular Static Safety Checking for C Programs. Ph.D. thesis, Université Paris-Sud, January 2009. http://www.lri.fr/~marche/moy09phd.pdf
  4. 4.
    Mandrykin, M.U., Khoroshilov, A.V.: Region analysis for deductive verification of c programs. Program. Comput. Softw. 42(5), 257–278 (2016).  https://doi.org/10.1134/S0361768816050042MathSciNetCrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-06200-6_29CrossRefGoogle Scholar
  6. 6.
    Torlakcik, M.: Contracts in OpenBSD. M.sc. dissertation report, University College Dublin (2010)Google Scholar
  7. 7.
    Verker: Verification of linux kernel library functions (2017). https://forge.ispras.ru/projects/verker
  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. http://www.lri.fr/~marche/hubert07hav.pdf
  11. 11.
    ISO/IEC 9899: 2011: C11 standard for C programming language. Standard, JTC and ISO (2011). http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
  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. http://www.lri.fr/~moy/Publis/moy07ccpp.pdf
  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).  https://doi.org/10.1134/S0361768815040040MathSciNetCrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-57288-8_5CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-17164-2_21CrossRefGoogle Scholar
  17. 17.
    Verker: Verification of linux kernel library functions, lemma functions branch (2017). https://forge.ispras.ru/projects/verker/repository?rev=lemma_functions
  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). http://doi.acm.org/10.1145/2480362.2480593
  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).  https://doi.org/10.1007/978-3-642-37036-6_8CrossRefGoogle 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