Skip to main content
SpringerLink
Log in
Book cover

International Andrei Ershov Memorial Conference on Perspectives of System Informatics

PSI 2017: Perspectives of System Informatics pp 256–275Cite as

A Memory Model for Deductively Verifying Linux Kernel Modules

  • Conference paper
  • First Online:

  • 1594 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10742))

Abstract

Several previous evaluations of memory models for SMT-based deductive verification tools have shown that the choice of memory model may significantly affect both the number of automatically discharged verification conditions and the capabilities of the verification tool. One of the most efficient memory models for deductive verification of low-level C code is based on region analysis and component-as-array modeling. However, originally this model doesn’t support many C language idioms widely used in low-level system code including the Linux kernel. The paper suggests a modification of this model that extends it with full support for arbitrarily nested structures, unions and arrays, arbitrary pointer arithmetic and general pointer type casts. The extension for nested structures and arrays requires no additional annotation overhead. The support for pointer arithmetic, unions and pointer type casts generally requires user annotations. The proposed model fully preserves the performance of the original memory model for earlier supported code. Preliminary practical evaluation on an industrial security kernel module showed a small specification overhead required for code where the proposed model is not fully automatic.

The research was supported by RFBR grant 15-01-03934.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, Washington, DC, USA, pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  2. Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711–728. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_47

    Google Scholar 

  3. Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773–789. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_54

    Chapter  Google Scholar 

  4. Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439–458. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_23

    Chapter  Google Scholar 

  5. Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 171–182. ACM, New York (2008)

    Google Scholar 

  6. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4

    Chapter  Google Scholar 

  7. Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_15

    Chapter  Google Scholar 

  8. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2

    Chapter  Google Scholar 

  9. Böhme, S., Moskal, M.: Heaps and data structures: a challenge for automated provers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 177–191. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_15

    Chapter  Google Scholar 

  10. Moy, Y.: Automatic modular static safety checking for C programs. Ph.D. thesis, Université Paris-Sud, January 2009

    Google Scholar 

  11. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16

    Chapter  Google Scholar 

  12. Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. Electron. Notes Theor. Comput. Sci. 254, 85–103 (2009)

    Article  Google Scholar 

  13. Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7(23–50), 3 (1972)

    MATH  Google Scholar 

  14. Bornat, R.: Proving pointer programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000). https://doi.org/10.1007/10722010_8

    Chapter  Google Scholar 

  15. Hubert, T., Marché, C.: Separation analysis for deductive verification. In: Heap Analysis and Verification (HAV 2007), Braga, Portugal, pp. 81–93, March 2007

    Google Scholar 

  16. Dijkstra, E.W., Schölten, C.S.: The strongest postcondition. In: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, New York (1990). https://doi.org/10.1007/978-1-4612-3228-5_12

  17. Moy, Y.: Union and cast in deductive verification. In: Proceedings of the C/C++ Verification Workshop, vol. Technical Report ICIS-R07015, pp. 1–16. Radboud University Nijmegen, July 2007

    Google Scholar 

  18. Baudin, P., Cuoq, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. Version 1.11 – Aluminium-20160501, September 2016

    Google Scholar 

  19. Plotkin, G.D.: A structural approach to operational semantics (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for System Programming of the Russian Academy of Sciences, Moscow, Russia

    Mikhail Mandrykin & Alexey Khoroshilov

  2. The Faculty of Computational Mathematics and Cybernetics of Lomonosov Moscow State University, Moscow, Russia

    Alexey Khoroshilov

  3. Moscow Institute of Physics and Technology, Dolgoprudny, Russia

    Alexey Khoroshilov

  4. National Research University Higher School of Economics, Moscow, Russia

    Alexey Khoroshilov

Authors
  1. Mikhail Mandrykin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexey Khoroshilov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mikhail Mandrykin .

Editor information

Editors and Affiliations

  1. Ivannikov Institute for System Programming of RAS, Moscow, Russia

    Alexander K. Petrenko

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Mandrykin, M., Khoroshilov, A. (2018). A Memory Model for Deductively Verifying Linux Kernel Modules. In: Petrenko, A., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science(), vol 10742. Springer, Cham. https://doi.org/10.1007/978-3-319-74313-4_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-74313-4_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-74312-7

  • Online ISBN: 978-3-319-74313-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation