The University of New South Wales

Program verification in the presence of cached address translation


Hira Syeda and Gerwin Klein


UNSW Sydney


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

    pages            = {542-559},
    publisher        = {Lecture Notes in Computer Science},
    doi              = {\_32},
    month            = jul,
    booktitle        = {International Conference on Interactive Theorem Proving},
    paperurl         = {},
    year             = {2018},
    volume           = {10895},
    title            = {Program Verification in the Presence of Cached Address Translation},
    author           = {Syeda, Hira and Klein, Gerwin},
    address          = {Oxford, UK},
    date             = {2018-7-20}