Trustworthy Systems

Reasoning about translation lookaside buffers


Hira Syeda and Gerwin Klein


UNSW Sydney


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 crit- ical 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 ker- nels 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

    month            = may,
    date             = {2017-5-4},
    publisher        = {EasyChair Publications},
    volume           = {46},
    booktitle        = {Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence
                        and Reasoning},
    year             = {2017},
    address          = {Maun, Botswana},
    author           = {Syeda, Hira and Klein, Gerwin},
    title            = {Reasoning about Translation Lookaside Buffers},
    pages            = {490--508}