Trustworthy Systems

Formal reasoning under cached address translation

Authors

Hira Taqdees Syeda and Gerwin Klein

DATA61

UNSW Sydney

Abstract

Operating system (OS) kernels achieve isolation between user-level processes using hardware features such as multi-level page tables and translation lookaside buffers (TLB). 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 the memory management unit of the ARMv7-A architecture including a two-stage TLB with address space identifiers and global entries. 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 mirror the informal reasoning of OS engineers. 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.

BibTeX Entry

  @article{Syeda_Klein_20,
    author           = {Syeda, Hira Taqdees and Klein, Gerwin},
    date             = {2020-6-1},
    doi              = {https://doi.org/10.1007/s10817-019-09539-7},
    issn             = {0168-7433},
    issue            = {6},
    journal          = {Journal of Automated Reasoning},
    keywords         = {{TLB}, operating systems, cached adress translation, program verification, {Isabelle}/{HOL}, {ARM}},
    month            = jun,
    pages            = {911-945},
    publisher        = {Springer},
    title            = {Formal Reasoning under Cached Address Translation},
    volume           = {64},
    year             = {2020}
  }

Download