Skip to main content

TS

Reasoning about translation lookaside buffers

Authors

Hira Syeda and Gerwin Klein

Data61
CSIRO

UNSW

Abstract

The main security mechanism for enforcing memory isolation in operating systems is provided by page tables. The hardware-implemented Translation Lookaside Buffer (TLB) caches these, and therefore the TLB and its consistency with memory are security critical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified kernels currently leave the TLB as an assumption.

In this paper, we present a formal model of the Memory Management Unit (MMU) for the ARM architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks.

BibTeX Entry

  @inproceedings{Syeda_Klein_17,
    author           = {Syeda, Hira and Klein, Gerwin},
    month            = may,
    year             = {2017},
    keywords         = {ts, proofeng},
    title            = {Reasoning about Translation Lookaside Buffers},
    booktitle        = {Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence
                        and Reasoning},
    pages            = {490--508},
    address          = {Maun, Botswana}
  }

Download