Skip to main content


Program verification in the presence of cached address translation


Hira Syeda and Gerwin Klein



Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables and translation lookaside buffers (TLBs). Controlling the TLB correctly is a fundamental security property — yet all large-scale formal OS verification projects leave the TLB as an assumption. We present a logic for reasoning about low- level programs in the presence of TLB address translation. We extract invariants and necessary conditions for correct TLB operation that mirror the informal reasoning of OS engineers. 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 and page table manipulations.

BibTeX Entry

    publisher        = {Springer's LNCS series},
    doi              = {\_32},
    booktitle        = {Interactive Theorem Proving, ITP},
    author           = {Syeda, Hira and Klein, Gerwin},
    month            = jul,
    volume           = {10895},
    year             = {2018},
    date             = {2018-7-20},
    title            = {Program Verification in the Presence of Cached Address Translation},
    pages            = {542-559},
    address          = {Oxford, UK}


Served by Apache on Linux on seL4.