Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Formal Reasoning Under Cached Address Translation

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

Operating system (OS) kernels achieve isolation between user-level processes using hardware features such as multi-level page tables and translation lookaside buffers (TLBs). The TLB caches address translation, and therefore correctly controlling the TLB is a fundamental security property of OS kernels—yet all large-scale formal OS verification projects we are aware of leave the correct functionality of TLB as an assumption. In this paper, we present a verified sound abstraction of a detailed concrete model of the memory management unit (MMU) of the ARMv7-A architecture. This MMU abstraction revamps our previous address space specific MMU abstraction to include new software-visible TLB features such as caching of globally-mapped and partial translation entries in a two-stage TLB. We use this abstraction as the underlying model to develop a logic for reasoning about low-level programs in the presence of cached address translation. We extract invariants and necessary conditions for correct TLB operation that mirrors the informal reasoning of OS engineers. We systematically show how these invariants adapt to global and partial translation entries. We show that our program logic reduces to a standard logic for user-level reasoning, reduces to side-condition checks for kernel-level reasoning, and can handle typical OS kernel tasks such as context switching.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. ARM also provides locked down entries that will not be evicted automatically. These could be modelled easily here by excluding them from the eviction set.

  2. This is the technique attacked by Meltdown [17]. Since hardware manufacturers are in the process of fixing this flaw, we present the more interesting setting instead of the less complex and slower scenario with a separate kernel address space.

References

  1. Achermann, R., Humbel, L., Cock, D., Roscoe, T.: Physical addressing on real hardware in Isabelle/HOL. In: Proceedings of the 9th International Conference on Interactive Theorem Proving, pp. 1–19 (2018)

  2. Alkassar, E., Cohen, E., Kovalev, M., Paul, W.J.: Verification of TLB virtualization implemented in C. In: Proceedings of Verified Software: Theories, Tools and Experiments 2012, vol. 7152 of Lecture Notes in Computer Science, Philadelphia, pp. 209–224, PA, USA (Jan 2012)

  3. ARM Ltd.: ARM Architecture Reference Manual, ARM v7-A and ARM v7-R, April 2008. ARM DDI 0406B

  4. ARM Ltd.: ARM Cortex-A15 MPCore Processor Technical Reference Manual, June 2013. ARM DDI 0438I

  5. Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Cache-leakage resilient OS isolation in an idealized model of virtualization. In: Proceedings of the 25th IEEE Computer Security Foundations Symposium, pp. 186–197 (2012)

  6. Daum, M., Billing, N., Klein, G.: Concerned with the unprivileged: user programs in kernel refinement. Form. Asp. Comput. 26(6), 1205–1229 (2014)

    Article  MathSciNet  Google Scholar 

  7. Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: AFIPS Conference Proceedings. 1979 National Computer Conference, pp. 329–334, New York, NY, USA, June 1979

  8. Fox, A., Myreen, M.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Proceedings of the 1st International Conference on Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pp. 243–258, Edinburgh, UK (July 2010)

  9. Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X. (Newman), Weng, S.-C., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 595–608 (2015)

  10. Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sjöberg, V., Costanzo, D.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: USENIX Symposium on Operating Systems Design and Implementation, pp. 653–669, Savannah, GA, USA (Nov 2016)

  11. Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2:1–2:70 (2014)

    Article  Google Scholar 

  12. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA (Oct 2009)

  13. Kolanski, R.: A logic for virtual memory. In: Systems Software Verification, pp. 61–77, Sydney, Australia (July 2008)

  14. Kolanski, R.: Verification of Programs in Virtual Memory Using Separation Logic. PhD thesis, UNSW, Sydney, Australia, (July 2011). Available from publications page at http://ts.data61.csiro.au/

  15. Kolanski, R., Klein, G.: Types, maps and separation logic. In: International Conference on Theorem Proving in Higher Order Logics, pp. 276–292, Munich, Germany (Aug 2009)

  16. Kovalev, M.: TLB Virtualization in the Context of Hypervisor Verification. PhD thesis, Saarland University, Saarbrücken, Germany (2013)

  17. Lipp, M., Schwartz, M., Gruss, D., Prescher, T., Haas, W., Fogh, A., Horn, J., Mangard, S., Kocher, P., Genkin, D., Yarom, Y., Hamburg, M.: Meltdown: reading kernel memory from user space. In: USENIX Security Symposium, Baltimore, MD, USA (Aug 2018)

  18. Lutsyk, P.: Correctness of Multi-core Processors with Operating System Support. PhD thesis, Saarland University, Saarbrücken, Germany (2018)

  19. Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in Higher-Order Logic. In: Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, volume 1479 of Lecture Notes in Computer Science, pp. 349–366, Canberra, Australia (Sept 1998)

  20. Nemati, H., Dam, M., Guanciale, R., Do, V., Vahidi, A.: Trustworthy memory isolation of Linux on embedded devices. In: Trust and Trustworthy Computing, pp. 125–142 (Aug 2015)

  21. Nemati, H., Guanciale, R., Dam, M.: Trustworthy virtualization of the ARMv7 memory subsystem. In: Proceedings of the 41st International Conference on Current Trends in Theory and Practice of Computer Science, vol. 8939 of Lecture Notes in Computer Science, pp. 578–589, Pec pod Sněžkou, Czech Republic (Jan 2015)

  22. Neumann, P.G., Boyer, R.S., Feiertag, R.J., Levitt, K.N., Robinson, L.: A Provably Secure Operating System: The System, Its Applications, and Proofs, 2nd Edn. Technical Report CSL-116, Computer Science Laboratory, SRI International, Menlo Park, CA, USA (May 1980)

  23. Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, vol. 2283 of Lecture Notes in Computer Science (2002)

  24. Slind, K., Norrish, M.: A brief overview of HOL4. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, pp. 28–32 (Feb 2008)

  25. Syeda, H.T., Klein, G.: Reasoning about translation lookaside buffers. In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol. 46 of EPiC Series in Computing, pp. 490–508 (2017)

  26. Syeda, H.T., Klein, G.: Program verification in the presence of cached address translation. In: Proceedings of the 9th International Conference on Interactive Theorem Proving, volume 10895 of Lecture Notes in Computer Science, pp. 542–559, Oxford, UK (July 2018)

  27. Syeda, H.T., Klein, G.: Isabelle/HOL program logic for cached address translation. https://github.com/SEL4PROJ/tlb/tree/jar19 (April 2019)

Download references

Author information

Authors and Affiliations

  1. Data61, CSIRO, Canberra, Australia

    Hira Taqdees Syeda & Gerwin Klein

  2. School of Computer Science and Engineering, UNSW, Sydney, Australia

    Hira Taqdees Syeda & Gerwin Klein

Authors
  1. Hira Taqdees Syeda
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gerwin Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hira Taqdees Syeda.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Syeda, H.T., Klein, G. Formal Reasoning Under Cached Address Translation. J Autom Reasoning 64, 911–945 (2020). https://doi.org/10.1007/s10817-019-09539-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-019-09539-7

Keywords

Search

Navigation