The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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 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.
@misc{syeda2017reasoning,
title = {Reasoning about Translation Lookaside Buffers},
author = {Hira Syeda and Gerwin Klein},
year = {2017},
journal = {EPiC series in computing},
volume = {46},
pages = {490--470},
doi = {10.29007/c2f1},
}
This record lives at https://refs.drheap.org/syeda2017reasoning/ and will keep
doing so. It used to be called syeda2018reasoning, and those addresses still resolve to this one.